Loading...
Please wait, while we are loading the content...
Towards Model-checking Probabilistic Timed Automata against Probabilistic Duration Properties
| Content Provider | Semantic Scholar |
|---|---|
| Author | Dang, Van Hung Zhang, Miaomiao Pham, Dinh Chinh |
| Copyright Year | 2016 |
| 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 |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.jcsce.vnu.edu.vn/index.php/jcsce/article/download/121/33 |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
