POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom

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 Jan

Displayed 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
20m
Talk
Project and Conquer: Fast Quantifier Elimination for Checking Petri Nets Reachability
VMCAI
Nicolas Amat LAAS-CNRS, Silvano DAL ZILIO LAAS-CNRS, Didier Le Botlan LAAS-CNRS, INSA-Toulouse
Pre-print
16:20
20m
Talk
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
20m
Talk
Resilience and Home-Space for WSTS
VMCAI
Alain Finkel ENS Paris Saclay, Mathieu Hilaire ENS Paris Saclay
17:00
20m
Talk
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
10m
Talk
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