On Verification of Probabilistic Timed Automata against Probabilistic Duration Properties

Daegu, Korea August 21-August 24

DOI Bookmark:

http://doi.ieeecomputersociety.org/10.1109/RTCSA.2007.53

13th IEEE International Conference on ...

	This Article
	PURCHASE ARTICLE: $19 PDF HTML IEEE Xplore Subscribers
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Dang Van Hung Articles by Miaomiao Zhang

	ASCII Text	x
	Dang Van Hung, Miaomiao Zhang, "On Verification of Probabilistic Timed Automata against Probabilistic Duration Properties," Real-Time Computing Systems and Applications, International Workshop on, pp. 165-172, 13th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA 2007), 2007.

	BibTex	x
	@article{ 10.1109/RTCSA.2007.53, author = {Dang Van Hung and Miaomiao Zhang}, title = {On Verification of Probabilistic Timed Automata against Probabilistic Duration Properties}, journal ={Real-Time Computing Systems and Applications, International Workshop on}, volume = {0}, year = {2007}, issn = {1533-2306}, pages = {165-172}, doi = {http://doi.ieeecomputersociety.org/10.1109/RTCSA.2007.53}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Real-Time Computing Systems and Applications, International Workshop on TI - On Verification of Probabilistic Timed Automata against Probabilistic Duration Properties SN - 1533-2306 SP165 EP172 A1 - Dang Van Hung, A1 - Miaomiao Zhang, PY - 2007 KW - null VL - 0 JA - Real-Time Computing Systems and Applications, International Workshop on ER -

Dang Van Hung, United Nations University

Miaomiao Zhang, Tongji University

In this paper, we introduce an extension of Duration Calculus called Simple Probabilistic Duration Calculus (SPDC) to express dependability requirements for real-time systems, and address the problem to decide if a probabilistic timed automaton satisfies a SPDC formula. We prove that the problem is decidable for a class of SPDC called probabilistic linear duration invariants, and provide a model checking algorithm for solving this problem.

Citation:

Dang Van Hung, Miaomiao Zhang, "On Verification of Probabilistic Timed Automata against Probabilistic Duration Properties," rtcsa, pp.165-172, 13th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA 2007), 2007

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.