Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete

要約

時限命題時間論理(TPTL)の${0, \infty}$ 断片の決定可能性を調べる．TPTL$^{0,}infty}$の充足可能性検査がPSPACE-completeであることを示す。さらに、その1変数の断片(1-TPTL$^{0, \infty}$)ですら、満足性検査がEXPSPACE完全であるMetric Interval Temporal Logic (MITL)よりも厳密に表現力が高い。従って、我々は、計算上容易な充足可能性検査を持つ、厳密に表現力の高い論理を手に入れたことになる。我々の知る限り、TPTL$^{0, \infty}$ はTPTLの多変数の断片の中で、時限語に対する束縛や制限（例えば、束縛された可変性、束縛された時間など）を課すことなく、充足可能性検査が決定可能である最初のものである。PSPACEへのメンバシップは、Unilateral Very Weak Alternating Timed Automata (VWATA$^{0, \infty}$)と呼ばれる、複数のクロックを持つ新しい’非パンクチュアル’な交互時限オートマトン(Alternating Timed Automata)の空性チェック問題への漸化によって得られる。これは、与えられたVWATA$^{0, \infty}$ の大きさの多項式であるシミュレーション等価な非決定時オートマトンを構成することによって示される。

要約(オリジナル)

We investigate the decidability of the ${0,\infty}$ fragment of Timed Propositional Temporal Logic (TPTL). We show that the satisfiability checking of TPTL$^{0,\infty}$ is PSPACE-complete. Moreover, even its 1-variable fragment (1-TPTL$^{0,\infty}$) is strictly more expressive than Metric Interval Temporal Logic (MITL) for which satisfiability checking is EXPSPACE complete. Hence, we have a strictly more expressive logic with computationally easier satisfiability checking. To the best of our knowledge, TPTL$^{0,\infty}$ is the first multi-variable fragment of TPTL for which satisfiability checking is decidable without imposing any bounds/restrictions on the timed words (e.g. bounded variability, bounded time, etc.). The membership in PSPACE is obtained by a reduction to the emptiness checking problem for a new ‘non-punctual’ subclass of Alternating Timed Automata with multiple clocks called Unilateral Very Weak Alternating Timed Automata (VWATA$^{0,\infty}$) which we prove to be in PSPACE. We show this by constructing a simulation equivalent non-deterministic timed automata whose number of clocks is polynomial in the size of the given VWATA$^{0,\infty}$.

arxiv情報

提供元, 利用サービス

arxiv.jp, DeepL