Probably safe or live

Joost P. Katoen, Lei Song, Lijun Zhang

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    7 Citations (Scopus)
    53 Downloads (Pure)

    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
    PublisherAssociation for Computing Machinery (ACM)
    Pages55
    Number of pages10
    ISBN (Print)978-1-4503-2886-9
    DOIs
    Publication statusPublished - 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
    Duration: 14 Jul 201418 Jul 2014

    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

    Keywords

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

    Cite this