zbMATH — the first resource for mathematics

Linear temporal logic with until and before on integer numbers, deciding algorithms. (English) Zbl 1185.03022
Grigoriev, Dima (ed.) et al., Computer science – theory and applications. First international computer science symposium in Russia, CSR 2006, St. Petersburg, Russia, June 8–12, 2006. Proceedings. Berlin: Springer (ISBN 3-540-34166-8/pbk). Lecture Notes in Computer Science 3967, 322-333 (2006).
Summary: As specifications and verifications of concurrent systems employ Linear Temporal Logic (LTL), it is increasingly likely that logical consequence in LTL will be used in description of computations and parallel reasoning. We consider the linear temporal logic \(\mathcal {LTL}^{\text{U,B}}_{\text{N, N}^{-1}}(\mathcal Z)\) extending the standard LTL by operations \(\mathbf B\) (before) and \(\mathbf N^{\mathbf {-1}}\) (previous). Two sorts of problems are studied: (i) satisfiability and (ii) description of logical consequence in \(\mathcal {LTL}^{\text{U,B}}_{\text{N, N}^{-1}}(\mathcal Z)\) via admissible logical consecutions (inference rules). The model checking for LTL is a traditional way of studying such logics. The most popular technique based on automata was developed by M. Vardi. Our paper uses a reduction of logical consecutions and formulas of LTL to consecutions of a uniform form consisting of formulas of temporal degree 1. Based on the technique of Kripke structures, we find necessary and sufficient conditions for a consecution to be not admissible in \(\mathcal {LTL}^{\text{U,B}}_{\text{N, N}^{-1}}(\mathcal Z)\). This provides an algorithm recognizing consecutions (rules) admissible in \(\mathcal {LTL}^{\text{U,B}}_{\text{N, N}^{-1}}(\mathcal Z)\) by Kripke structures of size linear in the reduced normal forms of the initial consecutions. As an application, this algorithm solves also the satisfiability problem for \(\mathcal {LTL}^{\text{U,B}}_{\text{N, N}^{-1}}(\mathcal Z)\).
For the entire collection see [Zbl 1102.68006].

03B44 Temporal logic
68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI