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 language | English |
---|---|
Book series | Lecture Notes in Computer Science |
Volume | 7148 |
Pages (from-to) | 396-411 |
ISSN | 0302-9743 |
DOIs | |
Publication status | Published - 2012 |
Event | 13th International Conference on Verification, Model Checking, and Abstract Interpretation - Philadelphia, United States Duration: 22 Jan 2012 → 24 Jan 2012 Conference number: 13 |
Conference
Conference | 13th International Conference on Verification, Model Checking, and Abstract Interpretation |
---|---|
Number | 13 |
Country/Territory | United States |
City | Philadelphia |
Period | 22/01/2012 → 24/01/2012 |