Abstract Probabilistic Automata

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

    Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-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.

    Original languageEnglish
    JournalInformation and Computation
    Volume232
    Pages (from-to)66-116
    Number of pages50
    ISSN0890-5401
    DOIs
    Publication statusPublished - Nov 2013

    Keywords

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

    Fingerprint

    Dive into the research topics of 'Abstract Probabilistic Automata'. Together they form a unique fingerprint.

    Cite this