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].

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