Abstract

This paper presents a formal characterisation of safety and liveness properties 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 a 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, and show that a sound and complete logical characterisation of liveness properties hinges on the (open) satisfiability problem for PCTL. 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.
Original languageUndefined
Title of host publicationProceedings 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)
Place of PublicationNew York
PublisherACM
Pages55
Number of pages10
ISBN (Print)978-1-4503-2886-9
DOIs
StatePublished - Jul 2014
EventJoint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2014 - Vienna, Austria

Publication series

Name
PublisherACM

Conference

ConferenceJoint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2014
Abbreviated titleCSL-LICS
CountryAustria
CityVienna
Period14/07/1418/07/14

Fingerprint

Hinges
Decomposition

Keywords

  • EWI-25693
  • IR-94428
  • METIS-309877

Cite this

Katoen, J. P., Song, L., & Zhang, L. (2014). Probably safe or live. 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) (pp. 55). New York: ACM. DOI: 10.1145/2603088.2603147

Katoen, Joost P.; Song, Lei; Zhang, Lijun / Probably safe or live.

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). New York : ACM, 2014. p. 55.

Research output: Scientific - peer-reviewConference contribution

@inbook{ab1fe6e94a8f4ec99187050fa073a9d7,
title = "Probably safe or live",
abstract = "This paper presents a formal characterisation of safety and liveness properties 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 a 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, and show that a sound and complete logical characterisation of liveness properties hinges on the (open) satisfiability problem for PCTL. 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.",
keywords = "EWI-25693, IR-94428, METIS-309877",
author = "Katoen, {Joost P.} and Lei Song and Lijun Zhang",
note = "10.1145/2603088.2603147",
year = "2014",
month = "7",
doi = "10.1145/2603088.2603147",
isbn = "978-1-4503-2886-9",
publisher = "ACM",
pages = "55",
booktitle = "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)",

}

Katoen, JP, Song, L & Zhang, L 2014, Probably safe or live. 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). ACM, New York, pp. 55, Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2014, Vienna, Austria, 14-18 July. DOI: 10.1145/2603088.2603147

Probably safe or live. / Katoen, Joost P.; Song, Lei; Zhang, Lijun.

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). New York : ACM, 2014. p. 55.

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - Probably safe or live

AU - Katoen,Joost P.

AU - Song,Lei

AU - Zhang,Lijun

N1 - 10.1145/2603088.2603147

PY - 2014/7

Y1 - 2014/7

N2 - This paper presents a formal characterisation of safety and liveness properties 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 a 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, and show that a sound and complete logical characterisation of liveness properties hinges on the (open) satisfiability problem for PCTL. 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.

AB - This paper presents a formal characterisation of safety and liveness properties 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 a 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, and show that a sound and complete logical characterisation of liveness properties hinges on the (open) satisfiability problem for PCTL. 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.

KW - EWI-25693

KW - IR-94428

KW - METIS-309877

U2 - 10.1145/2603088.2603147

DO - 10.1145/2603088.2603147

M3 - Conference contribution

SN - 978-1-4503-2886-9

SP - 55

BT - 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)

PB - ACM

ER -

Katoen JP, Song L, Zhang L. Probably safe or live. 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). New York: ACM. 2014. p. 55. Available from, DOI: 10.1145/2603088.2603147