Abstract Probabilistic Automata

Benoît Delahaye, Joost-Pieter Katoen, Kim Guldstrand Larsen, Axel Legay, Mikkel Larsen Pedersen, Falak Sher, Andrzej Wasowski

    Publikation: Artikel i tidsskrift og konference artikel i tidsskriftTidsskriftartikelForskningpeer review

    Abstract

    Probabilistic Automata (PAs) are a widely-recognized mathematical framework for the specification and analysis of systems with non-deterministic and stochastic behaviors. This paper proposes Abstract Probabilistic Automata (APAs), that is a novel abstraction model for PAs. In APAs uncertainty of the non-deterministic choices is modeled by may/must modalities on transitions while uncertainty of the stochastic behavior is expressed by (underspecified) stochastic constraints. We have developed a complete abstraction theory for PAs, and also propose the first specification theory for them. Our theory supports both satisfaction and refinement operators, together with classical stepwise design operators. In addition, we study the link between specification theories and abstraction in avoiding the state-space explosion problem.

    OriginalsprogEngelsk
    TidsskriftInformation and Computation
    Vol/bind232
    Sider (fra-til)66-116
    Antal sider50
    ISSN0890-5401
    DOI
    StatusUdgivet - nov. 2013

    Emneord

    • Specification
    • Abstraction
    • Compositional reasoning
    • Interface automata
    • Probabilistic Automata

    Fingeraftryk

    Dyk ned i forskningsemnerne om 'Abstract Probabilistic Automata'. Sammen danner de et unikt fingeraftryk.

    Citationsformater