Safety and Liveness -- New Results and Perspectives

Joost-Pieter Katoen
RWTH Aachen University
Friday, 23 January, 2015 - 14:00
NO Solvay (5th floor)

Lamport’s notions of safety and liveness properties are folklore. Safety says that nothing wrong happens whereas liveness ensures that progress is made.  Since the 1980s, several formalizations and variations have been investigated.

This talk presents some new developments on this classical property classification.  This includes new results for LTL, for Markov chains and timed automata.  We present a sound and complete characterization of safety in probabilistic CTL — every safe PCTL formula is a safety property and every safety property (expressible in PCTL) can be expressed in safe PCTL.  The same holds for liveness, but this necessarily resorts on satisfiability checking.

For timed systems we provide a topological characterisation of branching-time real-time safety and liveness properties and give sound and complete fragments of timed CTL.  We show that deciding whether a TCTL-formula is safety or liveness is in general undecidable.  We discuss how a (finitely branching) timed CTL formula can be decomposed into the conjunction of a safety and a liveness property, both represented by timed alternating tree automata.