Resilience and Home-Space for WSTS

Resilience of unperfect systems is a key property for improving safety by insuring that if a system could go into a bad state in \(\textsf {Bad}\) then it can also leave this bad state and reach a safe state in \(\textsf {Safe}\) . We consider six types of resilience (one of them is the home-space property) defined by an upward-closed set or a downward-closed set \(\textsf {Safe}\) , and by the existence of a bound on the length of minimal runs starting from a set \(\textsf {Bad}\) and reaching \(\textsf {Safe}\) ( \(\textsf {Bad}\) is generally the complementary of \(\textsf {Safe}\) ). We first show that all resilience problems are undecidable for effective Well Structured Transition Systems (WSTS) with strong compatibility. We then show that resilience is decidable for Well Behaved Transition Systems (WBTS) and for WSTS with adapted effectiveness hypotheses. Most of the resilience properties are shown decidable for other classes like WSTS with the downward compatibility, VASS, lossy counter machines, reset-VASS, integer VASS and continuous VASS.