Decidability and undecidability results for duration calculus. (English) Zbl 0811.68115

Zhou, Chaochen; Hansen, Michael R.; Sestoft, Peter

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

MSC:

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

Keywords:

duration calculus; temporal logic