In classical timed automata, as defined by ALUR and DILL [AD90, AD94] and since widely studied, the only operation allowed to modify the clocks is the reset operation. For instance, a clock can neither be set to a non-null constant value, nor be set to the value of another clock nor, in a non-deterministic way, to some value lower or higher than a given constant. In this paper we study in details such updates. We characterize in a thin way the frontier between decidability and undecidability. Our main contributions are the following: - We exhibit many classes of updates for which emptiness is undecidable. These classes depend on the clock constraints that are used - diagonal-free or not - whereas it is well known that these two kinds of constraints are equivalent for classical timed automata. - We propose a generalization of the region automaton proposed by ALUR and DILL, allowing to handle larger classes of updates. The complexity of the decision procedure remains PSPACE-complete. © Springer-Verlag Berlin Heidelberg 2000.
CITATION STYLE
Bouyer, P., Dufourd, C., Fleury, E., & Petit, A. (2000). Are timed automata updatable? Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 1855, 464–479. https://doi.org/10.1007/10722167_35
Mendeley helps you to discover research relevant for your work.