Title :
On Verification of Probabilistic Timed Automata against Probabilistic Duration Properties
Author :
Van Hung, Dang ; Zhang, Miaomiao
Author_Institution :
United Nations Univ., Macau
Abstract :
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.
Keywords :
calculus of communicating systems; formal verification; probabilistic automata; probabilistic logic; dependability requirement; model checking algorithm; probabilistic duration property; probabilistic linear duration invariant; probabilistic timed automata verification; probabilistic timed automaton; real-time system; simple probabilistic duration calculus; Automata; Calculus; Computer applications; Distributed computing; Embedded computing; Logic; Probability distribution; Real time systems; Software engineering; State-space methods;
Conference_Titel :
Embedded and Real-Time Computing Systems and Applications, 2007. RTCSA 2007. 13th IEEE International Conference on
Conference_Location :
Daegu
Print_ISBN :
978-0-7695-2975-2
DOI :
10.1109/RTCSA.2007.53
