Towards Model-checking Probabilistic Timed Automata against Probabilistic Duration Properties

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:
Probabilistic Duration Calculus
Probabilistic Timed Automata
Model-checking
Markov Decision Process
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
Description
Summary: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.

Similar Items