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

Abstract. Resilience of unperfect systems is a key property for improving safety by insuring that if a system could go into a bad state then it can also leave this bad state and reach a safe state. We consider six types of resilience (one of them is the home-space property) defined by an upward closed set Safe (Safe =↑ Safe) or a downward-closed set (Safe =↓ Safe), and by the existence of a bound k on the length of minimal runs starting from Bad and reaching Safe, where Bad is generally the complementary of Safe. We study the decidability of each type of resilience for two kinds of models: WSTS and VASS. We first show that most of all resilience problems are undecidable for WSTS with strong compatibility (and with effective pred-basis). Then we prove the decidability of resilience for completion-post-effective ω 2 -WSTS with strong compatibility (almost all known WSTS are in this class) and Safe =↑ Safe. Moreover, some resilience properties are decidable for three other classes of WSTS : (1) WSTS with effective ↑ post ∗ basis and Safe =↑ Safe ; (2) ideal-effective WSTS with downward and upward compatibilities ; and (3) ideal-effective downward- compatible WSTS with Safe =↓ Safe. Finally, we study the resilience for VASS with semi-linear subsets Bad and Safe and for variations of VASS (lossy counter machines, integer VASS and continuous VASS); most of the resilience properties are shown decidable.

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