Bisimulation, Logic and Reachability Analysis for Markovian Systems

L.M. Bujorianu, M.C. Bujorianu

    Research output: Book/ReportReportProfessional

    22 Downloads (Pure)

    Abstract

    In the recent years, there have been a large amount of investigations on safety verification of uncertain continuous systems. In engineering and applied mathematics, this verification is called stochastic reachability analysis, while in computer science this is called probabilistic model checking (PMC). In the context of this work, we consider the two terms interchangeable. It is worthy to note that PMC has been mostly considered for discrete systems. Therefore, there is an issue of improving the application of computer science techniques in the formal verification of continuous stochastic systems. We present a new probabilistic logic of model theoretic nature. The terms of this logic express reachability properties and the logic formulas express statistical properties of terms. Moreover, we show that this logic characterizes a bisimulation relation for continuous time continuous space Markov processes. For this logic we define a new semantics using state space symmetries. This is a recent concept that was successfully used in model checking. Using this semantics, we prove a full abstraction result. Furthermore, we prove a result that can be used in model checking, namely that the bisimulation preserves the probabilities of the reachable sets.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherFormal Methods and Tools (FMT)
    Number of pages6
    Publication statusPublished - 13 Mar 2008

    Publication series

    NameCTIT Technical Report Series
    PublisherCentre for Telematics and Information Technology, University of Twente
    No.TR-CTIT-08-23
    ISSN (Print)1381-3625

    Keywords

    • MSC-68Q85
    • EWI-12112
    • IR-64682
    • METIS-250908

    Cite this