Towards Model-checking Probabilistic Timed Automata against Probabilistic Duration Properties - Dang, Van Hung (ĐHQGHN, 2017)
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.