Abstract Probabilistic Automata

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

doi:10.1016/j.ic.2013.10.002

Abstract Probabilistic Automata

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

Computer Science

Research output: Journal Article or Conference Article in Journal › Journal article › Research › peer-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 language	English
Journal	Information and Computation
Volume	232
Pages (from-to)	66-116
Number of pages	50
ISSN	0890-5401
DOIs	https://doi.org/10.1016/j.ic.2013.10.002
Publication status	Published - Nov 2013

Keywords

Specification
Abstraction
Compositional reasoning
Interface automata
Probabilistic Automata

Access to Document

10.1016/j.ic.2013.10.002

MT-Lab - Modelling of Information Technology
Wasowski, A. (CoI), Godskesen, J. C. (PI), Song, L. (CoI), Traonouez, L.-M. (CoI) & Biondi, F. (CoI)
01/11/2008 → 31/10/2013
Project: Research

Cite this

@article{6c95463f3f9d4433b1b832dee649f2b0,

title = "Abstract Probabilistic Automata",

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.",

keywords = "Specification, Abstraction, Compositional reasoning, Interface automata, Probabilistic Automata, Specification, Abstraction, Compositional reasoning, Interface automata, Probabilistic Automata",

author = "Beno{\^i}t Delahaye and Joost-Pieter Katoen and Larsen, {Kim Guldstrand} and Axel Legay and Pedersen, {Mikkel Larsen} and Falak Sher and Andrzej Wasowski",

year = "2013",

month = nov,

doi = "10.1016/j.ic.2013.10.002",

language = "English",

volume = "232",

pages = "66--116",

journal = "Information and Computation",

issn = "0890-5401",

publisher = "Academic Press",

}

TY - JOUR

T1 - Abstract Probabilistic Automata

AU - Delahaye, Benoît

AU - Katoen, Joost-Pieter

AU - Larsen, Kim Guldstrand

AU - Legay, Axel

AU - Pedersen, Mikkel Larsen

AU - Sher, Falak

AU - Wasowski, Andrzej

PY - 2013/11

Y1 - 2013/11

N2 - 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.

AB - 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.

KW - Specification

KW - Abstraction

KW - Compositional reasoning

KW - Interface automata

KW - Probabilistic Automata

KW - Specification

KW - Abstraction

KW - Compositional reasoning

KW - Interface automata

KW - Probabilistic Automata

U2 - 10.1016/j.ic.2013.10.002

DO - 10.1016/j.ic.2013.10.002

M3 - Journal article

SN - 0890-5401

VL - 232

SP - 66

EP - 116

JO - Information and Computation

JF - Information and Computation

ER -

Abstract Probabilistic Automata

Abstract

Keywords

Access to Document

Fingerprint

Projects

MT-Lab - Modelling of Information Technology

Cite this