A General Framework for Probabilistic Characterizing Formulae
Publication: Research - peer-review › Article in proceedings – Annual report year: 2012
Standard
A General Framework for Probabilistic Characterizing Formulae. / Sack, Joshua; Zhang, Lijun.
In: Verification, Model Checking, and Abstract Interpretation: 13th International Conference, VMCAI 2012 Philadelphia, PA, USA, January 22-24, 2012 Proceedings. Springer, 2012. p. 396-411 (Lecture Notes in Computer Science; No. 7148).Publication: Research - peer-review › Article in proceedings – Annual report year: 2012
Harvard
APA
CBE
MLA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - A General Framework for Probabilistic Characterizing Formulae
A1 - Sack,Joshua
A1 - Zhang,Lijun
AU - Sack,Joshua
AU - Zhang,Lijun
PB - Springer
PY - 2012
Y1 - 2012
N2 - 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.
AB - 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.
UR - http://lara.epfl.ch/vmcai2012/
U2 - 10.1007/978-3-642-27940-9_26
DO - 10.1007/978-3-642-27940-9_26
SN - 978-3-642-27939-3
BT - Verification, Model Checking, and Abstract Interpretation
T2 - Verification, Model Checking, and Abstract Interpretation
T3 - Lecture Notes in Computer Science
T3 - en_GB
SP - 396
EP - 411
ER -