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

safetylivenessPCTL

Mathematics Subject Classification ID

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

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

(13)

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

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)