Time-abstracting Bisimulation for Probabilistic Timed Automata

摘要：

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.

作者: Taolue Chen Tingting Han Joost-Pieter Katoen

作者单位: CWI PO Box 94079, 1090 GB Amsterdam, The Netherlands MOVES, RWTH Aachen University, Germany FMT, University of Twente, The Netherlands

会议类型: 国际会议

会议名称: 第二届IFIP/IEEE软件工程理论基础国际研讨会(TASE 2008)(Second IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering)

会议地点: 南京

会议语种:英文

页码: 177-184

在线出版日期: 2008-06-17（万方平台首次上网日期，不代表论文的发表时间）