離散事象システムにおけるオパシティのためのモジュラスーパバイザ制御

摘要

本稿では，形式言語に基づく枠組みにおいて，離散事象システムのオパシティを保証するスーパバイザ制御について考察する．特に，システムのシークレット動作が複数の言語で与えられる場合において，すべての言語のオパシティを保証する最大許容スーパバイザのモジュラ設計を考える．まず，そのような最大許容スーパバイザは一般にモジュラ設計法では構成できないことを示す．しかし，可観測な不可制御事象に関するある仮定のもとでは，最大許容スーパバイザのモジュラ設計が可能となることを明らかにする．