In distributed real-time systems, we cannot assume that clocks are perfectly synchronized. To model them, we use independent clocks and define their timed semantics. The universal timed language, and the timed language inclusion of icTA are undecidable. Thus, we propose Recursive Distributed Event Clock Automata (DECA). DECA are closed under all boolean operations and their timed language inclusion problem is decidable (more precisely PSPACE-complete), allowing stepwise refinement. We also propose Distributed Event Clock Temporal Logic (DECTL), a real-time logic with independent time evolutions. This logic can be model-checked by translating a DECTL formula into a DECA automaton. © 2011 Springer-Verlag.
CITATION STYLE
Ortiz, J., Legay, A., & Schobbens, P. Y. (2011). Distributed event clock automata: Extended abstract. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6807 LNCS, pp. 250–263). https://doi.org/10.1007/978-3-642-22256-6_23
Mendeley helps you to discover research relevant for your work.