The logic of event clocks. Decidability, complexity and expressiveness. (English) Zbl 0978.03015

Raskin, Jean-François; Schobbens, Pierre-Yves

J. Autom. Lang. Comb. 4, No. 3, 247-282 (1999).

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.

MSC:

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

Keywords:

real-time logic of event clocks; event clock automata