Skip to main content

Reachability for updatable timed automata made faster and more effective

Publication ,  Conference
Gastin, P; Mukherjee, S; Srivathsan, B
Published in: Leibniz International Proceedings in Informatics, LIPIcs
December 1, 2020

Updatable timed automata (UTA) are extensions of classical timed automata that allow special updates to clock variables, like x := x − 1, x := y + 2, etc., on transitions. Reachability for UTA is undecidable in general. Various subclasses with decidable reachability have been studied. A generic approach to UTA reachability consists of two phases: first, a static analysis of the automaton is performed to compute a set of clock constraints at each state; in the second phase, reachable sets of configurations, called zones, are enumerated. In this work, we improve the algorithm for the static analysis. Compared to the existing algorithm, our method computes smaller sets of constraints and guarantees termination for more UTA, making reachability faster and more effective. As the main application, we get an alternate proof of decidability and a more efficient algorithm for timed automata with bounded subtraction, a class of UTA widely used for modelling scheduling problems. We have implemented our procedure in the tool TChecker and conducted experiments that validate the benefits of our approach.

Duke Scholars

Published In

Leibniz International Proceedings in Informatics, LIPIcs

DOI

ISSN

1868-8969

ISBN

9783959771740

Publication Date

December 1, 2020

Volume

182
 

Citation

APA
Chicago
ICMJE
MLA
NLM
Gastin, P., Mukherjee, S., & Srivathsan, B. (2020). Reachability for updatable timed automata made faster and more effective. In Leibniz International Proceedings in Informatics, LIPIcs (Vol. 182). https://doi.org/10.4230/LIPIcs.FSTTCS.2020.47
Gastin, P., S. Mukherjee, and B. Srivathsan. “Reachability for updatable timed automata made faster and more effective.” In Leibniz International Proceedings in Informatics, LIPIcs, Vol. 182, 2020. https://doi.org/10.4230/LIPIcs.FSTTCS.2020.47.
Gastin P, Mukherjee S, Srivathsan B. Reachability for updatable timed automata made faster and more effective. In: Leibniz International Proceedings in Informatics, LIPIcs. 2020.
Gastin, P., et al. “Reachability for updatable timed automata made faster and more effective.” Leibniz International Proceedings in Informatics, LIPIcs, vol. 182, 2020. Scopus, doi:10.4230/LIPIcs.FSTTCS.2020.47.
Gastin P, Mukherjee S, Srivathsan B. Reachability for updatable timed automata made faster and more effective. Leibniz International Proceedings in Informatics, LIPIcs. 2020.

Published In

Leibniz International Proceedings in Informatics, LIPIcs

DOI

ISSN

1868-8969

ISBN

9783959771740

Publication Date

December 1, 2020

Volume

182