Parameterized Verification of Disjunctive Timed NetworksRecorded
We introduce new techniques for the parameterized verification of disjunctive timed networks (DTNs), i.e., networks of timed automata (TAs) that communicate via location guards that enable a transition only if there is another process in a given location. This computational model has been considered in the literature before, example applications are gossiping clock synchronization protocols or planning problems. We address the minimum-time reachability problem (Minreach) in DTNs, and show how to efficiently solve it based on a novel zone-graph algorithm. We further show that solving Minreach allows us to construct a “summary” TA capturing exactly the possible behaviors of a single TA within a DTN of arbitrary size. The combination of these two results enables the parameterized verification of DTNs, while avoiding the construction of an exponential-size cutoff system required by existing results. Additionally, we develop sufficient conditions for solving Minreach and parameterized verification problems even in certain cases where locations that appear in location guards can have clock invariants, a case that has usually been excluded in the literature. Our techniques are also implemented, and experiments show their practicality.
Mon 15 JanDisplayed time zone: London change
16:00 - 17:30 | Session 4: Infinite State Systems, Runtime VerificationVMCAI at Marconi Room Chair(s): Helmut Seidl Technische Universität München | ||
16:00 20mTalk | Project and Conquer: Fast Quantifier Elimination for Checking Petri Nets Reachability VMCAI Pre-print | ||
16:20 20mTalk | Parameterized Verification of Disjunctive Timed NetworksRecorded VMCAI Étienne André Université Sorbonne Paris Nord; LIPN; CNRS, Paul Eichler CISPA - Helmholtz Center for Information Security, Swen Jacobs CISPA, Shyam Karra CISPA | ||
16:40 20mTalk | Resilience and Home-Space for WSTS VMCAI | ||
17:00 20mTalk | Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic VMCAI Ritam Raha University of Antwerp, Antwerp, Belgium, Rajarshi Roy Max Planck Institute for Software Systems, Kaiserslautern, Germany, Nathanaël Fijalkow CNRS, LaBRI, and Alan Turing Institute, Daniel Neider Technical University of Dortmund, Germany, Guillermo A. Perez University of Antwerp Pre-print | ||
17:20 10mTalk | TP-DejaVu: Combining Operational and Declarative Runtime Verification VMCAI Klaus Havelund NASA/Caltech Jet Propulsion Laboratory, Panagiotis Katsaros Aristotle University of Thessaloniki, Moran Omer Bar Ilan University, Israel, Doron Peled Bar Ilan University, Anastasios Temperekidis Aristotle University of Thessaloniki |