2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering Time-Abstracting Bisimulation for Probabilistic Timed Automata June 17-June 19 ISBN: 978-0-7695-3249-3
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TASE.2008.29
This paper focuses on probabilistic timed automata (PTA), an extension of timed automata with discrete probabilistic branchings. As the regions of these automata often lead to an exponential blowup, reduction techniques are of utmost importance. In this paper, we investigate probabilistic time-abstracting bisimulation (PTaB), an equivalence notion that abstracts from exact time delays. PTaB is proven to preserve probabilistic computational tree logic (PCTL). The region equivalence is a (very refined) PTaB. Furthermore, we provide a non-trivial adaptation of the traditional partition-refinement algorithm to compute the quotient under PTaB. This algorithm is symbolic in the sense that equivalence classes are represented as polyhedra.
Index Terms:
time-abstracting bisimulation, probabilistic timed automata
Citation:
Taolue Chen, Tingting Han, Joost-Pieter Katoen, "Time-Abstracting Bisimulation for Probabilistic Timed Automata," tase, pp.177-184, 2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, 2008 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||