Anzeige
Erschienen in:
2000 | OriginalPaper | Buchkapitel
Are Timed Automata Updatable?
verfasst von : Patricia Bouyer, Catherine Dufourd, Emmanuel Fleury, Antoine Petit
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.