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 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 |