Time-Abstracting Bisimulation for Probabilistic Timed Automata

T. Chen, Tingting Han, Joost P. Katoen

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

5 Citations (Scopus)

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 languageUndefined
Title of host publicationProceedings of the 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE)
PublisherIEEE Computer Society
Pages177-184
Number of pages8
ISBN (Print)978-0-7695-3249-3
DOIs
Publication statusPublished - Jun 2008
Event2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008 - Nanjing, China
Duration: 17 Jun 200819 Jun 2008
Conference number: 2

Publication series

Name
PublisherIEEE Computer Society
Number2008/16200

Conference

Conference2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008
Abbreviated titleTASE
CountryChina
CityNanjing
Period17/06/0819/06/08

Keywords

  • EWI-14719
  • METIS-255049
  • IR-62643

Cite this

Chen, T., Han, T., & Katoen, J. P. (2008). Time-Abstracting Bisimulation for Probabilistic Timed Automata. In Proceedings of the 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE) (pp. 177-184). [10.1109/TASE.2008.29] IEEE Computer Society. https://doi.org/10.1109/TASE.2008.29
Chen, T. ; Han, Tingting ; Katoen, Joost P. / Time-Abstracting Bisimulation for Probabilistic Timed Automata. Proceedings of the 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE). IEEE Computer Society, 2008. pp. 177-184
@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",
year = "2008",
month = "6",
doi = "10.1109/TASE.2008.29",
language = "Undefined",
isbn = "978-0-7695-3249-3",
publisher = "IEEE Computer Society",
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 Computer Society, 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 Computer Society, 2008. p. 177-184 10.1109/TASE.2008.29.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Time-Abstracting Bisimulation for Probabilistic Timed Automata

AU - Chen, T.

AU - Han, Tingting

AU - Katoen, Joost P.

N1 - 10.1109/TASE.2008.29

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 Computer Society

ER -

Chen T, Han T, Katoen JP. Time-Abstracting Bisimulation for Probabilistic Timed Automata. In Proceedings of the 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE). IEEE Computer Society. 2008. p. 177-184. 10.1109/TASE.2008.29 https://doi.org/10.1109/TASE.2008.29