次のような状況をモデル化するための適切な形式 (つまり時相論理) を探しています。
- 時間内に個別のイベントでイベントが発生する可能性があります (以下に詳述する条件に従います)。
- 状態あります。この状態は一定数の変数では表現できません。ただし、各エントリが有限数の変数で構成される線形リスト/配列で表現することは可能です。
- イベントが発生する前に、状態は修正されます。
- いつでも、イベントが可能です。それらは固定された構造を持っています (いくつかの変数があります)。発生する可能性のあるイベントは、現在の状態によって制限されます。
- イベントは、状態の即時変更を引き起こします。
- イベントによって、状態が継続的に変化することもあります。たとえば、(上記の配列のエントリの 1 つの) 変数は、その値を 0 から 1 に一定時間 (すぐに、または指定された遅延の後に) 変更します。
- また、「ある条件 C が成立するイベント E の後の最も早い時点」という形式で離散的な時点を指定し、そのような時点で連続的な状態変化を開始することも可能である必要があります。
このようなものをモデル化するための既存の時相論理はありますか?
次のように、希望する条件を表現することも可能である必要があります。
- 特定の時点の参照: 配列のすべてのエントリの特定の変数の合計は、特定のしきい値を超えることはできません。
- 時間の経過に伴う変化の参照: すべての可能な時間間隔について、特定の変数の値 (再び、前述の配列の各エントリから) [現実的には、各エントリに対して計算された算術式ではなく] は、指定されたしきい値よりも速く変化してはなりません。
考えられるすべてのシナリオについて、すべての条件が満たされているかどうかをチェックできるモデル チェッカーが存在する必要があります。そうでない場合は、考えられるシナリオを 1 つ出力し、どの条件が満たされていないかを通知する必要があります。つまり、可能性のあるシナリオを説明する条件と、それらのシナリオで満たされなければならない条件を区別する必要があり、単に「不可能」とだけ言うのではありません。