Parameterized Verification of Disjunctive Timed Networks

Explore new techniques for parameterized verification of disjunctive timed networks (DTNs) in this 16-minute conference talk presented at VMCAI'24. Delve into the minimum-time reachability problem (Minreach) in DTNs and learn about an efficient zone-graph algorithm for solving it. Discover how solving Minreach enables the construction of a "summary" timed automaton that captures the behaviors of a single timed automaton within a DTN of any size. Understand how these combined results facilitate parameterized verification of DTNs without the need for exponential-size cutoff systems. Explore sufficient conditions for solving Minreach and parameterized verification problems in cases where locations with clock invariants appear in location guards. Gain insights into the practical implementation of these techniques and their effectiveness through experimental results.