Recently, model-checking and probabilistic timed simulation verification methods of probabilistic timed automata have been developed. In this paper, we propose probabilistic timed transition systems by generalizing probabilistic timed automata, and propose deductive verification rules of probabilistic real-time linear temporal logic over probabilistic timed transition systems. As our proposed probabilistic timed transition system is a general computational model, we have developed general verification methods.
Weitere Kapitel dieses Buchs durch Wischen aufrufen
- Deductive Probabilistic Verification Methods of Safety, Liveness and Nonzenoness for Distributed Real-Time Systems
- Springer Berlin Heidelberg
Neuer Inhalt/© ITandMEDIA