A General Framework for Probabilistic Characterizing Formulae

Joshua Sack, Lijun Zhang

    Research output: Contribution to journalConference articleResearchpeer-review

    Abstract

    Recently, a general framework on characteristic formulae was proposed by Aceto et al. It offers a simple theory that allows one to easily obtain characteristic formulae of many non-probabilistic behavioral relations. Our paper studies their techniques in a probabilistic setting. We provide a general method for determining characteristic formulae of behavioral relations for probabilistic automata using fixed-point probability logics. We consider such behavioral relations as simulations and bisimulations, probabilistic bisimulations, probabilistic weak simulations, and probabilistic forward simulations. This paper shows how their constructions and proofs can follow from a single common technique.
    Original languageEnglish
    Book seriesLecture Notes in Computer Science
    Volume7148
    Pages (from-to)396-411
    ISSN0302-9743
    DOIs
    Publication statusPublished - 2012
    Event13th International Conference on Verification, Model Checking, and Abstract Interpretation - Philadelphia, United States
    Duration: 22 Jan 201224 Jan 2012
    Conference number: 13

    Conference

    Conference13th International Conference on Verification, Model Checking, and Abstract Interpretation
    Number13
    Country/TerritoryUnited States
    CityPhiladelphia
    Period22/01/201224/01/2012

    Fingerprint

    Dive into the research topics of 'A General Framework for Probabilistic Characterizing Formulae'. Together they form a unique fingerprint.

    Cite this