zbMATH — the first resource for mathematics

Until-since temporal logic based on parallel time with common past. Deciding algorithms. (English) Zbl 1132.03324
Artemov, Sergei N. (ed.) et al., Logical foundations of computer science. International symposium, LFCS 2007, New York, NY, USA, June 4–7, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-72732-3/pbk). Lecture Notes in Computer Science 4514, 486-497 (2007).
Summary: We present a framework for constructing algorithms recognizing admissible inference rules (consecutions) in temporal logics with Until and Since based on Kripke/Hintikka structures modeling parallel time with common past. Logics \(\mathcal{PTL}_\alpha\) with various branching factor \(\alpha\in {\mathcal N} \cup \{\omega\}\) after common past are considered. The offered technique looks rather flexible, for instance, with a similar approach we showed [V. V. Rybakov, “Branching time logic \(\mathcal{PTL}_\alpha\) with operations until and since based on bundles of integer numbers, logical consecutions, deciding algorithms” (2006), submitted] that temporal logic based on sheafs of integer numbers with common origin is decidable by admissibility. In this paper we extend obtained algorithms to logics \(\mathcal{PTL}_\alpha\). We prove that any logic \(\mathcal{PTL}_\alpha\) is decidable w.r.t. admissible consecutions (inference rules), as a consequence, we solve satisfiability problem and show that any \(\mathcal{PTL}_\alpha\) itself is decidable.
For the entire collection see [Zbl 1121.03005].

03B44 Temporal logic
Full Text: DOI