時間制限付き命題時相論理

コンピュータサイエンスの一分野であるモデル検査において、時間指定命題時相論理( TPTL ) は命題線形時相論理( LTL ) の拡張であり、変数を導入して 2 つのイベント間の時間を測定します。たとえば、 LTL では各イベントpの後に最終的にイベントqが続くことを記述できますが、 TPTL ではさらにq の発生 に時間制限を与えることができます。

TPTL の未来フラグメントは線形時相論理と同様に定義され、さらにクロック変数を導入して定数と比較することができます。正式には、クロックのセットが与えられた場合、MTL は次のように構築されます。 ${\displaystyle X}$

• 命題変数 APの有限集合、
• 論理演算子¬と∨、そして
• 時間的 様相 演算子U、
• クロック比較、、数値、および<、≤、=、≥、> などの比較演算子。${\displaystyle x\simc}$${\displaystyle x\in X}$${\displaystyle c}$${\displaystyle \sim}$
• クロックのセットを持つ TPTL 式用のフリーズ量化演算子。${\displaystyle x.\phi}$${\displaystyle \phi}$${\displaystyle X\cup \{x\}}$

さらに、間隔の場合、は の略語とみなされ、他のすべての種類の間隔についても同様です。 ${\displaystyle I=(a,b)}$${\displaystyle x\in I}$${\displaystyle x>a\land x<b}$

TPTL+Past ^[1]の論理はTLSの未来フラグメントとして構築されており、

• 時間的様相演算子S。

次の演算子Nは MTL 構文の一部とはみなされないことに注意してください。代わりに、他の演算子から定義されます。

閉じた式とは、空の時計の集合上の式である。^[2]

を、直感的に時間の集合を表すものとしましょう。 を、各瞬間にAPからの命題の集合を関連付ける関数としましょう。 TPTL 式のモデルは、このような関数です。 通常、 は、時間指定の単語または信号のいずれかです。 その場合、は離散サブセットまたは 0 を含む区間のいずれかになります。 ${\displaystyle T\subseteq \mathbb {R} _{+}}$${\displaystyle \gamma :T\to {\mathcal {P}}(AP)}$${\displaystyle t\in T}$${\displaystyle \gamma}$${\displaystyle \gamma}$${\displaystyle T}$

および を上記と同じとします。 をクロックの集合とします。(上のクロック値) とします。 ${\displaystyle T}$${\displaystyle \gamma}$${\displaystyle X}$${\displaystyle \nu :X\to \mathbb {R} _{\geq 0}}$${\displaystyle X}$

ここで、TPTL 式が評価 に対して時刻 で成り立つとはどういうことかを説明します。これは で表されます。および を時計の集合 上の 2 つの式、時計の集合 上の式、、、 数値、 を< 、≤、=、≥、> などの比較演算子とします。まず、主演算子が LTL にも属する式を考えます。 ${\displaystyle \phi}$${\displaystyle t}$${\displaystyle \nu}$${\displaystyle \gamma ,t,\nu \models \phi }$${\displaystyle \phi}$${\displaystyle \psi}$${\displaystyle X}$${\displaystyle \xi}$${\displaystyle X\cup \{y\}}$${\displaystyle x\in X}$${\displaystyle l\in {\mathtt {AP}}}$${\displaystyle c}$${\displaystyle \sim}$

• ${\displaystyle \gamma ,t,\nu \models l}$が成り立つ場合、${\displaystyle l\in \gamma (t)}$
• ${\displaystyle \gamma ,t,\nu \models \neg \phi }$成立する${\displaystyle \gamma ,t,\nu \not \models \phi }$
• ${\displaystyle \gamma ,t,\nu \models \phi \lor \psi }$またはのいずれかの場合に成立します${\displaystyle \gamma ,t,\nu \models \phi }$${\displaystyle \gamma ,t,\nu \models \psi }$
• ${\displaystyle \gamma ,t,\nu \models \phi \mathbin {\mathcal {U}} \psi }$が存在し、かつ各 に対して が存在するとき成立する。 ${\displaystyle t<t''}$${\displaystyle \gamma ,t'',\nu \models \psi }$${\displaystyle t<t'<t''}$${\displaystyle \gamma ,t',\nu \models \phi }$
• ${\displaystyle \gamma,t,\nu\models\phi\mathbin{\mathcal{S}}\psi}$が存在し、かつ各 に対して が存在するとき成立する。 ${\displaystyle t''<t}$${\displaystyle \gamma ,t'',\nu \models \psi }$${\displaystyle t''<t'<t}$${\displaystyle \gamma ,t',\nu \models \phi }$
• ${\displaystyle \gamma,t,\nu\modelsx\simc}$が成り立つ場合、${\displaystyle t-\nu (y)\sim c}$
• ${\displaystyle \gamma ,t,\nu \models y.\xi }$保持される場合は保持されます。${\displaystyle \gamma ,t,\nu [y\to t]\models \phi }$

メトリック時相論理は、 LTL のもう 1 つの拡張であり、時間の測定を可能にします。変数を追加する代わりに、負でない数の間隔に対して無限の演算子とを追加します。ある時点での式 の意味は、の時刻が区間 で発生するという制約を除き、式 の意味と本質的に同じです。 ${\displaystyle {\mathcal {U}}_{I}}$${\displaystyle {\mathcal {S}}_{I}}$${\displaystyle I}$${\displaystyle \phi \mathbin {\mathcal {U_{I}}} \psi }$${\displaystyle t}$${\displaystyle \phi \mathbin {\mathcal {U}} \psi }$${\displaystyle t''}$${\displaystyle \psi }$${\displaystyle t+I}$

TPTLは少なくともMTLと同等の表現力を持っています。実際、MTL式はTPTL式（ここでは新しい変数）と同等です。^[2]${\displaystyle \phi \mathbin {\mathcal {U_{I}}} \psi }$${\displaystyle x.\phi {\mathcal {(}}x\in I\land \psi )}$${\displaystyle x}$

したがって、ページMTLで導入されたその他の演算子( や など)も TPTL 式として定義できます。 ${\displaystyle \Box }$${\displaystyle \Diamond }$

TPTLは、時間指定語と信号の両方において、MTL ^{[1] : 2}よりも厳密に表現力が優れています。時間指定語では、 と同等のMTL式はありません。信号では、 と同等のMTL式はありません。これは、時点1より前の最後の原子命題が であることを述べています。 ${\displaystyle \Box (a\implies x.\Diamond (b\land \Diamond (c\land x\leq 5)))}$${\displaystyle x.\Diamond (a\land x\leq 1\land \Box (x\leq 1\implies \neg b))}$${\displaystyle a}$

標準的な（時間制限のない）無限ワードは、から までの関数です。時間、および関数の集合を使用して、このようなワードを検討することができます。この場合、任意の LTL 式について、の場合のみ、 となります。ここで、 は非厳密な演算子を持つ TPTL 式と見なされ、 は空集合上で定義された唯一の関数です。 ${\displaystyle w=a_{0},a_{1},\dots ,}$${\displaystyle \mathbb {N} }$${\displaystyle A}$${\displaystyle T=\mathbb {N} }$${\displaystyle \gamma (i)=a_{i}}$${\displaystyle \phi }$${\displaystyle w,i\models \phi }$${\displaystyle \gamma ,i,\nu \models \phi }$${\displaystyle \phi }$${\displaystyle \nu }$