Computer Science – Logic in Computer Science
Scientific paper
2011-06-10
Computer Science
Logic in Computer Science
Long version of CONCUR'11 with the same title: added extension to simulations, countable states
Scientific paper
Probabilistic automata (PA) have been successfully applied in the formal verification of concurrent and stochastic systems. Efficient model checking algorithms have been studied, where the most often used logics for expressing properties are based on PCTL and its extension PCTL*. Various behavioral equivalences are proposed for PAs, as a powerful tool for abstraction and compositional minimization for PAs. Unfortunately, the behavioral equivalences are well-known to be strictly stronger than the logical equivalences induced by PCTL or PCTL*. This paper introduces novel notions of strong bisimulation relations, which characterizes PCTL and PCTL* exactly. We also extend weak bisimulations characterizing PCTL and PCTL* without next operator, respectively. Thus, our paper bridges the gap between logical and behavioral equivalences in this setting.
Godskesen Jens Chr.
Song Lei
Zhang Lijun
No associations
LandOfFree
Bisimulations Meet PCTL Equivalences for Probabilistic Automata does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Bisimulations Meet PCTL Equivalences for Probabilistic Automata, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Bisimulations Meet PCTL Equivalences for Probabilistic Automata will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-413689