Model Checking Probabilistic Timed Systems against Timed Automata Specification

摘要

We study a model checking problem on a complex probabilistic timed system. In such a system, components are interacting with each other under time constraints, and their behaviors exhibit some uncertainties. People always want the system to run along with some demands. We model the system as a network of probabilistic timed automata, and use a timed automaton to denote the demands about the interactions among the system's components. To solve the problem, we use the method of "observe" which let the requirement automaton to observe the running of the system, and also the probabilistic model checker PRISM is used to calculate the probability reflecting the satisfying level of the original system to the demands.