Metric temporal logic とは

メトリック・テンポラル・ロジック(MTL)は、時間ロジックの特殊なケースです。これは時間的オペレータが、until、next、sinceおよびpreviousオペレータのような時間制約のあるバージョンに置き換えられる時間的論理の拡張です。インターリーブと仮想クロックの両方の抽象を想定したリニアタイムロジックです。これは、ポイントベースの弱単調整数時間セマンティクスで定義されます。 MTLの場合、充足可能性問題の正確な複雑さは、区間ベースまたはポイントベースの同期(すなわち、厳密に単調)または非同期(すなわち、弱単調)の解釈EXPSPACE-completeとは無関係であり、
MTLは、リアルタイムシステムのための顕著な仕様形式として記述されています。無限の時間をかけた言葉の上の完全なMTLの決定可能性の問題は開いたままです。