zbMATH — the first resource for mathematics

Dynamical properties of timed automata revisited. (English) Zbl 1142.68040
Raskin, Jean-François (ed.) et al., Formal modeling and analysis of timed systems. 5th international conference, FORMATS 2007, Salzburg, Austria, October 3–5, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-75453-4/pbk). Lecture Notes in Computer Science 4763, 130-146 (2007).
Summary: We give a generalization of a solution by Puri to the problem of checking emptiness in timed automata with drifting clocks for the case of automata with non-closed guards. We show that non-closed guards pose certain specific problems which cannot be handled by Puri’s algorithm, and propose a new algorithm, based on the idea of “boundary clock regions” of Alur, LaTorre and Pappas. We then give a symbolic algorithm for solving the reachability problem. Our algorithm is based on a symbolic construction of the “neighborhood” of a zone, and on a procedure that, given a set of zones $$\mathcal{Z}$$, builds the forward propagation of the strongly connected components which can be reached from $$\mathcal{Z}$$. This improves a symbolic algorithm of Daws and Kordy, due to the ability to handle sets of zones.
For the entire collection see [Zbl 1138.68007].

MSC:
 68Q45 Formal languages and automata
HyTech
Full Text: