Lei Song ; Lijun Zhang ; Jens Chr. Godskesen ; Flemming Nielson - Bisimulations Meet PCTL Equivalences for Probabilistic Automata

lmcs:1238 - Logical Methods in Computer Science, June 21, 2013, Volume 9, Issue 2 - https://doi.org/10.2168/LMCS-9(2:7)2013
Bisimulations Meet PCTL Equivalences for Probabilistic AutomataArticle

Authors: Lei Song ; Lijun Zhang ; Jens Chr. Godskesen ; Flemming Nielson ORCID

    Probabilistic automata (PAs) have been successfully applied in formal verification of concurrent and stochastic systems. Efficient model checking algorithms have been studied, where the most often used logics for expressing properties are based on probabilistic computation tree logic (PCTL) and its extension PCTL^*. Various behavioral equivalences are proposed, as a powerful tool for abstraction and compositional minimization for PAs. Unfortunately, the equivalences are well-known to be sound, but not complete with respect to the logical equivalences induced by PCTL or PCTL*. The desire of a both sound and complete behavioral equivalence has been pointed out by Segala in 1995, but remains open throughout the years. In this paper we introduce novel notions of strong bisimulation relations, which characterize PCTL and PCTL* exactly. We extend weak bisimulations that characterize PCTL and PCTL* without next operator, respectively. Further, we also extend the framework to simulation preorders. Thus, our paper bridges the gap between logical and behavioral equivalences and preorders in this setting.


    Volume: Volume 9, Issue 2
    Published on: June 21, 2013
    Imported on: March 30, 2012
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • Technology-supported Risk Estimation by Predictive Assessment of Socio-technical Security; Funder: European Commission; Code: 318003
    • Mobility between Europe and Argentina applying Logics to Systems; Funder: European Commission; Code: 295261

    4 Documents citing this article

    Consultation statistics

    This page has been seen 1213 times.
    This article's PDF has been downloaded 457 times.