zbMATH — the first resource for mathematics

The logic of event clocks. Decidability, complexity and expressiveness. (English) Zbl 0978.03015
Summary: In this paper we define the real-time logic of event clocks. This logic is inspired by event clock automata. The logic is defined, illustrated and shown to be decidable in PSPACE by a simple decision procedure that relies on a reduction to event clock automata. The expressive power of the logic is compared to known formalisms.

03B44 Temporal logic
68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B25 Decidability of theories and sets of sentences
03D15 Complexity of computation (including implicit computational complexity)
03D05 Automata and formal grammars in connection with logical questions