Advances in Probabilistic Model Checking

11 years 7 months ago
Advances in Probabilistic Model Checking
In the recent years, there have been a large amount of investigations on safety verification of uncertain continuous systems. In engineering and applied mathematics, this verification is called stochastic reachability analysis, while in computer science this is called probabilistic model checking (PMC). In the context of this work, we consider the two terms interchangeable. It is worthy to note that PMC has been mostly considered for discrete systems. Therefore, there is an issue of improving the application of computer science techniques in the formal verification of continuous stochastic systems. We present a new probabilistic logic of model theoretic nature. The terms of this logic express reachability properties and the logic formulas express statistical properties of terms. Moreover, we show that this logic characterizes a bisimulation relation for continuous time continuous space Markov processes. For this logic we define a new semantics using state space symmetries. This is a re...
Joost-Pieter Katoen
Added 05 Mar 2010
Updated 08 Mar 2010
Type Conference
Year 2010
Authors Joost-Pieter Katoen
Comments (0)