同期的および非同期的ハイパープロパティのための論理の統一

本論文では、線形時間設定におけるパワフルなハイパー論理フレームワークであるGeneralized HyperLTL with Stuttering and Contexts (GHyperLTLS+C)を導入し、調査する。GHyperLTLS+Cは、既知の非同期的HyperLTL拡張と、同期および非同期完全記憶意味論の下でのKLTLの拡張を統一する。また、GHyperLTLS+Cの意味のある断片であるSimple GHyperLTLS+Cを特定し、その決定可能な模型検査問題を示す。Simple GHyperLTLS+Cは、HyperLTLおよび非同期的HyperLTL拡張の既知の断片よりも表現力が高く、単一トレース上で強力な非正則トレース特性を表現できる唯一のハイパー論理である。