Reachability for Updatable Timed Automata made faster and more effective

TL;DR

This paper improves the static analysis algorithm for updatable timed automata, making reachability checks faster and more effective, with applications to scheduling models and implementation in the TChecker tool.

Contribution

It introduces a more efficient static analysis method for UTA that computes smaller constraints sets and ensures broader termination, enhancing reachability analysis.

Findings

Smaller sets of constraints are computed with the new algorithm.

The approach guarantees termination for more UTA subclasses.

Experimental validation shows improved performance in TChecker.

Abstract

Updatable timed automata (UTA) are extensions of classic 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.