loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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
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.