Probably safe or live

DOI10.1145/2603088.2603147MaRDI QIDQ4635640zbMATH OpenOpenAlexWikidataFDO

Authors Lei Song, Joost-Pieter Katoen, Lijun Zhang

Publication date 23 April 2018

Published in Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1401.7171, https://research.utwente.nl/en/publications/probably-safe-or-live(ab1fe6e9-4a8f-4ec9-9187-050fa073a9d7).html

zbMATH Keywords

livenessPCTLsafety

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Abstract: This paper presents a formal characterisation of safety and liveness properties `a la Alpern and Schneider for fully probabilistic systems. As for the classical setting, it is established that any (probabilistic tree) property is equivalent to a conjunction of a safety and liveness property. A simple algorithm is provided to obtain such property decomposition for flat probabilistic CTL (PCTL). A safe fragment of PCTL is identified that provides a sound and complete characterisation of safety properties. For liveness properties, we provide two PCTL fragments, a sound and a complete one. We show that safety properties only have finite counterexamples, whereas liveness properties have none. We compare our characterisation for qualitative properties with the one for branching time properties by Manolios and Trefler, and present sound and complete PCTL fragments for characterising the notions of strong safety and absolute liveness coined by Sistla.

Recommendations

• Recognizing safety and liveness
• A lattice-theoretic characterization of safety and liveness
• scientific article; zbMATH DE number 139631
• scientific article; zbMATH DE number 17700
• scientific article; zbMATH DE number 1318512

Cited in

(15)

• Recognizing safety and liveness
• Spanning the spectrum from safety to liveness
• On relative and probabilistic finite counterability
• Do we need liveness? Approximation of liveness properties by safety properties
• scientific article; zbMATH DE number 17700 (Why is no real title available?)
• Deciding safety and liveness in TPTL
• scientific article; zbMATH DE number 139631 (Why is no real title available?)
• scientific article; zbMATH DE number 1318512 (Why is no real title available?)
• Reactive safety
• On relative and probabilistic finite counterability
• Quantitative safety and liveness
• Copying safety and liveness properties of computational artefacts
• Another glance at the Alpern-Schneider characterization of safety and liveness in concurrent executions
• Safety and liveness of quantitative properties and automata
• Safety and liveness from a methodological point of view

This page was built for publication: Probably safe or live

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635640)