Towards Model-Checking Probabilistic Timed Automata against Probabilistic Duration Properties

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.