Time-Abstracting Bisimulation for Probabilistic Timed Automata

T. Chen; Tingting Han; Joost P. Katoen

doi:10.1109/TASE.2008.29

Time-Abstracting Bisimulation for Probabilistic Timed Automata

T. Chen, Tingting Han, Joost P. Katoen

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

8 Citations (Scopus)

5 Downloads (Pure)

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.

Original language	Undefined
Title of host publication	Proceedings of the 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE)
Publisher	IEEE
Pages	177-184
Number of pages	8
ISBN (Print)	978-0-7695-3249-3
DOIs	https://doi.org/10.1109/TASE.2008.29
Publication status	Published - Jun 2008
Event	2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008 - Nanjing, China Duration: 17 Jun 2008 → 19 Jun 2008 Conference number: 2

Publication series

Name
Publisher	IEEE Computer Society
Number	2008/16200

Conference

Conference	2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008
Abbreviated title	TASE
Country/Territory	China
City	Nanjing
Period	17/06/08 → 19/06/08

Keywords

EWI-14719
METIS-255049
IR-62643

Access to Document

10.1109/TASE.2008.29

http://eprints.eemcs.utwente.nl/secure2/14719/01/final.pdf

Cite this

@inproceedings{13055a330f3d4d158047a0c1b693db85,

title = "Time-Abstracting Bisimulation for Probabilistic Timed Automata",

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.",

keywords = "EWI-14719, METIS-255049, IR-62643",

author = "T. Chen and Tingting Han and Katoen, {Joost P.}",

note = "10.1109/TASE.2008.29 ; 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008 ; Conference date: 17-06-2008 Through 19-06-2008",

year = "2008",

month = jun,

doi = "10.1109/TASE.2008.29",

language = "Undefined",

isbn = "978-0-7695-3249-3",

publisher = "IEEE",

number = "2008/16200",

pages = "177--184",

booktitle = "Proceedings of the 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE)",

address = "United States",

}

Chen, T, Han, T & Katoen, JP 2008, Time-Abstracting Bisimulation for Probabilistic Timed Automata. in Proceedings of the 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE)., 10.1109/TASE.2008.29, IEEE, pp. 177-184, 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, Nanjing, China, 17/06/08. https://doi.org/10.1109/TASE.2008.29

Time-Abstracting Bisimulation for Probabilistic Timed Automata. / Chen, T.; Han, Tingting; Katoen, Joost P.
Proceedings of the 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE). IEEE, 2008. p. 177-184 10.1109/TASE.2008.29.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Time-Abstracting Bisimulation for Probabilistic Timed Automata

AU - Chen, T.

AU - Han, Tingting

AU - Katoen, Joost P.

N1 - Conference code: 2

PY - 2008/6

Y1 - 2008/6

N2 - 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.

AB - 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.

KW - EWI-14719

KW - METIS-255049

KW - IR-62643

U2 - 10.1109/TASE.2008.29

DO - 10.1109/TASE.2008.29

M3 - Conference contribution

SN - 978-0-7695-3249-3

SP - 177

EP - 184

BT - Proceedings of the 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE)

PB - IEEE

T2 - 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008

Y2 - 17 June 2008 through 19 June 2008

ER -