Probably safe or live

DOI10.1145/2603088.2603147zbMATH Open1394.68231arXiv1401.7171OpenAlexW2035098582WikidataQ57800893 ScholiaQ57800893MaRDI QIDQ4635640FDOQ4635640

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)

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.

Full work available at URL: https://arxiv.org/abs/1401.7171

Recommendations

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

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)

Cited In (8)

• 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
• On relative and probabilistic finite counterability
• Recognizing safety and liveness
• Safety and liveness from a methodological point of view
• Quantitative safety and liveness
• Title not available (Why is that?)
• Title not available (Why is that?)

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)