Time-Abstracting Bisimulation for Probabilistic Timed Automata

Chen, Taolue and Han, Tingting and Katoen, Joost-Pieter (2008) Time-Abstracting Bisimulation for Probabilistic Timed Automata. In: 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, 17-19 June 2008, Nanjing, China.

PDF
Restricted to UT campus only: Request a copy
176Kb

Abstract:	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.
Item Type:	Conference or Workshop Item
Copyright:	© 2008 IEEE
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Formal Methods and Tools (FMT)
Link to this item:	http://purl.utwente.nl/publications/62643
Official URL:	http://dx.doi.org/10.1109/TASE.2008.29
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 255049