Towards Model-checking Probabilistic Timed Automata against Probabilistic Duration Properties

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...

Full description

Saved in:
Bibliographic Details
Main Authors: Dang, Van Hung, Miaomiao, Zhang, Pham, Dinh Chinh
Format: Article
Language:English
Published: ĐHQGHN 2017
Subjects:
Online Access:http://repository.vnu.edu.vn/handle/VNU_123/56777
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Vietnam National University, Hanoi
Language: English
id oai:112.137.131.14:VNU_123-56777
record_format dspace
spelling oai:112.137.131.14:VNU_123-567772018-08-07T01:07:19Z Towards Model-checking Probabilistic Timed Automata against Probabilistic Duration Properties Dang, Van Hung Miaomiao, Zhang Pham, Dinh Chinh Probabilistic Duration Calculus Probabilistic Timed Automata Model-checking Markov Decision Process 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. 2017-08-14T07:52:22Z 2017-08-14T07:52:22Z 2016 Article Dang, V. H, Miaomiao, Z, Pham, D. C. (2016). Towards Model-checking Probabilistic Timed Automata against Probabilistic Duration Properties. VNU Journal of Science, Comp. Science & Com. Eng., 32, 1, 58–73. 0866-8612 http://repository.vnu.edu.vn/handle/VNU_123/56777 en Journal of Comp. Science & Com. Eng. application/pdf ĐHQGHN
institution Vietnam National University, Hanoi
building VNU Library & Information Center
country Vietnam
collection VNU Digital Repository
language English
topic Probabilistic Duration Calculus
Probabilistic Timed Automata
Model-checking
Markov Decision Process
spellingShingle Probabilistic Duration Calculus
Probabilistic Timed Automata
Model-checking
Markov Decision Process
Dang, Van Hung
Miaomiao, Zhang
Pham, Dinh Chinh
Towards Model-checking Probabilistic Timed Automata against Probabilistic Duration Properties
description 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.
format Article
author Dang, Van Hung
Miaomiao, Zhang
Pham, Dinh Chinh
author_facet Dang, Van Hung
Miaomiao, Zhang
Pham, Dinh Chinh
author_sort Dang, Van Hung
title Towards Model-checking Probabilistic Timed Automata against Probabilistic Duration Properties
title_short Towards Model-checking Probabilistic Timed Automata against Probabilistic Duration Properties
title_full Towards Model-checking Probabilistic Timed Automata against Probabilistic Duration Properties
title_fullStr Towards Model-checking Probabilistic Timed Automata against Probabilistic Duration Properties
title_full_unstemmed Towards Model-checking Probabilistic Timed Automata against Probabilistic Duration Properties
title_sort towards model-checking probabilistic timed automata against probabilistic duration properties
publisher ĐHQGHN
publishDate 2017
url http://repository.vnu.edu.vn/handle/VNU_123/56777
_version_ 1680963261487382528