Towards Model-Checking Probabilistic Timed Automata against Probabilistic Duration Properties - Dang, Hung Van; Zhang, Miaomiao; Pham, Chinh Dinh (VNU Journal of Science: Computer Science and Communication Engineering; Vol 32 No 1 (2016), 2016)
In this paper, we consider a subclass of Probabilistic Duration   Calculus formula called Simple Probabilistic Duration Calculus   (SPDC) as a language for specifying dependability requirements for   real-time systems, and address the two problems: to decide if a   probabilistic timed automaton satisfies a SPDC formula, and to   decide if there exists a strategy of a probabilistic timed automaton   satisfies a SPDC formula. We prove that the both problems are   decidable for a class of SPDC called probabilistic linear duration   invariants, and provide model checking algorithms for solving these   problems.