非同期TeamLTLとHyperLTLの表現力に関する一考察

線形時間論理（LTL）は、反応系の形式的仕様を記述するためにシステム検証に使用されます。しかし、情報フローセキュリティにおける非推論などの関連する特性はLTLで表現できません。このような特性のクラスは、最近注目を集めているハイパープロパティとして知られています。ハイパープロパティを捉える研究には、トレース量子化子を用いてLTLを拡張するハイパーロジックと、トレースの集合に対して真実を拡張するチーム意味論を使用するロジックの2つの主要な流れがあります。本論文では、集合ベースのチーム意味論（TeamLTL）に基づく非同期LTLとHyperLTLとの関係を探ります。特に、チームLTLをブール和で拡張し、Until演算子の左辺やGlobal演算子内では否定が発生しないTeamLTLの拡張の断片について考慮します。ブール和で拡張されたTeamLTLは、1つの全称量子子に制限されたHyperLTLの正のブール閉包と同等に表現可能であり、ブール否定で拡張されたTeamLTLの左下閉じた断片は、1つの全称量子子に制限されたHyperLTLのブール閉包と表現的に同等であることを示します。