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. | VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73 Towards Model-checking Probabilistic Timed Automata against Probabilistic Duration PropertiesI Van Hung Dang1,∗, Miaomiao Zhang2 , Dinh Chinh Pham1 1 2 VNU University of Engineering and Technology, Hanoi, Vietnam School of Software Engineering, Tongji University, Shanghai, China Abstract 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. Received 25 November 2015, revised 20 December 2015, accepted 31 December 2015 Keywords: Probabilistic Duration Calculus, Probabilistic Timed Automata, Model-checking, Markov Decision Process. 1. Introduction developed by Dimitar Guelev [5], and in [6] we have shown that the calculus is useful for reasoning about QoS contracts in componentbased real-time systems. In 1992, Chaochen Zhou, Hoare and Anders Ravn introduced Duration Calculus [1] as a logic for reasoning about real-time systems. The calculus has attracted a great deal of attention, and was then developed further in many other works because of its rich meanings. Many of those works have been summarized in the monograph [2]. For specifying the dependability of real-time systems, a kind of probabilistic extension of Duration Calculus has been introduced in [3, 4]. No rigorous syntax has been introduced in these papers, and the authors just focused on the development of techniques for reasoning instead of the ones for checking. A version with a .
