zbMATH — the first resource for mathematics

Decidability and undecidability results for duration calculus. (English) Zbl 0811.68115
Enjalbert, Patrice (ed.) et al., STACS 93. 10th annual symposium on theoretical aspects of computer science, Würzburg, Germany, February 25-27, 1993. Proceedings. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 665, 58-68 (1993).
Duration calculus extends interval temporal logic with assertions about the duration of states, without mention of absolute time. It is used for specification and verification of real-time systems.
This paper identifies decidable and undecidable subsets of duration calculus. We show that for the subset whose only primitive formula is \(\lceil P \rceil\), which means “\(P\) holds almost everywhere”, satisfiability is decidable for discrete and dense time. It is still decidable for discrete time when the primitive formula \(\ell = k\), which means “the interval has length \(k\)”, is allowed, but becomes undecidable for dense time. Adding the integral equation \(\int P = \int Q\), which means “\(P\) and \(Q\) hold for the same duration”, or adding universal quantification \((\forall x.\dots \ell = x \dots)\) over durations, makes satisfiability undecidable for discrete as well as dense time.
For the entire collection see [Zbl 0866.00060].
Reviewer: Chaochen Zhou

68T27 Logic in artificial intelligence
03D35 Undecidability and degrees of sets of sentences
68Q05 Models of computation (Turing machines, etc.) (MSC2010)
68Q45 Formal languages and automata