有限時相論理に関するリソース

Question

有限時相論理に関するリソースを探しています。過去のTLについて言及しているリソースをいくつか見つけましたが、それを詳細に説明しているリソースや論文は見つかりませんでした。ここの誰かが私を正しい方向に向けてくれることを期待していました。

主なユースケースは、テストケースの生成を行い、TLのバリアントを使用して、いくつかの提案が成立するかどうかを確認するツールです。これは、生成/検索できる深さ（および幅）に制約があることを意味することは明らかです。現在の実装では、基本的にすることができますnext、globallyとuntil。ただし、使用にeventuallyは問題があります。ランダム生成が目的の状態に達しない場合はどうなるでしょうか。

だから私は2つの質問があると思います：

• 過去の時相論理はここで役立ちますか？それらについての詳細はどこにありますか？
• 有限数の状態で機能する他の時相論理はありますか？

好奇心旺盛な方のために、私が話しているプロジェクトは https://docs.quickstrom.io/（私は著者ではありませんが、アイデアに興味があります）。使用される仕様言語の詳細については、こちらをご覧ください。https://github.com/quickstrom/quickstrom/blob/main/docs/source/topics/specification-language.rst

Answer 1

質問1。過去の時相論理はここで役立ちますか？それらについての詳細はどこにありますか？

表現力の面では、いいえ。[1]の定理により、すべての線形時相論理式（過去の演算子を含む）は、開始点を使用して時間構造のプロパティを定義することにのみ関心がある場合、将来の式と同等です。

[1] Dov M. Gabbay、Amir Pnueli、Saharon Shelah、およびJonathanStavi。公平性の時間的分析について、POPL 1980：163-173、1980。

質問2。有限数の状態で機能する他の時相論理はありますか？

はい、たとえば、モジュロ時相論理[2]は、モジュロを数えることができる時相演算子を利用します $q$ または[3、4]で提案された拡張。

[2] A. Baziramwabo、P。McKenzie、D.Thérien：Modular Temporal Logic、LICS 1999、344-351。

[3]Z.Ésik、Distinguished Generatorsを使用したモノイドの有限単語および輪積に関する拡張時相論理、言語理論の開発2002、LNCS 2450、Springer（2003）43-58。

[4] P. Wolper、時相論理はより表現力があります、Information and Control 56（1983）、72–99。