the model checking algorithms for
stochastic models rely on a combination of model checking techniques for
non-stochastic systems, such as graph
algorithms, but also mathematical, often numerical methods for calculating
probabilities, such as linear equation
solving or linear programming.
Many of the advanced techniques
for very large non-stochastic models
have been adapted to treat stochastic
systems, including variations of decision diagrams to represent large state
spaces symbolically. 30 Complementary
techniques attempt to abstract from
irrelevant or redundant details in the
model and to replace the model with a
smaller, but “equivalent” one. Some of
them rely on the concept of lumpability
for stochastic processes, which in the
formal verification setting is known as
bisimulation quotienting, and where
states with the same probabilistic behavior are collapsed into a single representative. 16, 27
Other advanced techniques to fight
the state-explosion problem include
symmetry exploitation, 24 partial order
reduction, 5 or some form of abstraction28, possibly combined with automatic refinement. 15, 19 All these approaches take inspiration in classical
model checking advances, which often
get much more intricate to realize, and
raise interesting theoretical and practical challenges. All together, they have
advanced the field considerably in the
ability to handle cases as the ones discussed earlier.
An important feature of model
checkers for non-stochastic systems is
the generation of counterexamples for
properties that have been refuted by
the model checker. The principal situation is more difficult in the stochastic
setting, as for probabilistic properties,
say the requirement that a certain undesired event will appear with probability at most 10-3, single error traces
are not adequate. The generation and
representation of counterexamples is
therefore a topic of much increasing
attention17, 29 within the community.
To overcome the limitation to finite
state spaces, much work has been done
to treat infinite-state probabilistic systems, in many different flavors. 1, 23
Another topic of ongoing interest
lies in combining probabilistic behav-
ior with continuous dynamics as in
timed25 or hybrid automata, but more
work on the tool side is needed to as-
sess the merits of these approaches
faithfully. Theorem-proving tech-
niques for analyzing probabilistic sys-
tems21 are also a very promising direc-
tion. One of the major open technical
problems is the treatment of models
with nondeterminism and continuous
distributions. Initial results are inter-
esting but typically subject to (severe)
We thank Andrea Bobbio, Gianfranco
Ciardo, William Knottenbelt, Marta
Kwiatkowska, Evgenia Smirni, and the
anonymous reviewers for their valuable feedback.
Due to space limitations, a comprehensive list of all
references cited in this article can be found at the authors’
1. Abdulla, p., bertrand, n., rabinovich, A. and
Schnoebelen, p. Verification of probabilistic systems
with faulty communication. Inf. and Comp. 202, 2
2. Ajmone Marsan, M., conte, g., balbo, g. A class of
generalized stochastic petri nets for the performance
evaluation of multiprocessor systems. ACM Trans.
Comput. Syst. 2, 2 (1984), 93-122.
3. Andova, S., hermanns, h., and Katoen, j.-p. discrete-time rewards model-checked. FORMATS, LNCS 2791,
4. Aziz, A., Sanwal, K., Singhal, V. and brayton, r. K. Model
checking continuous-time Markov chains. ACM TOCL
1, 1 (2000), 162–170.
5. baier, c., größer, M., and ciesinski, f. partial order
reduction for probabilistic systems. Quantitative
Evaluation of Systems. Ieee cS press, 2004,
6. baier, c., haverkort, b.r., hermanns, h., and Katoen,
j-p. Model checking algorithms for continuous-time
Markov chains. IEEE TSE 29, 6 (2003), 524–541.
7. baier, c. and Katoen, j-p. Principles of Model Checking.
MIt press, 2008.
8. bianco, A. and de Alfaro, l. Model checking of
probabilistic and non-deterministic systems.
Foundations of Softw. Technology and Theor. Comp.
Science. LNCS 1026 (1995), 499–513.
9. bohnenkamp, h., van der Stok, p., hermanns, h.,
and Vaandrager, f.w. cost optimisation of the Ipv4
zeroconf protocol. In Proceedings of the Intl. Conf. on
Dependable Systems and Networks. Ieee cS press.
10. bolch, g., greiner, S., de Meer, h., trivedi, K. S. Queueing
Networks and Markov Chains. wiley press, 1998.
11. clarke, e. M., grumberg, o., and peled, d. Model
Checking. MIt press, 1999.
12. cloth, l. and haverkort, b.r. Model checking for
survivability. Quantitative Evaluation of Systems. Ieee
cS press (2005), 145–154.
13. coker, A., taylor, V., bhaduri, d., Shukla, S.,
raychowdhury, A., and roy, K. Multijunction fault-
tolerance architecture for nanoscale crossbar
memories. IEEE Trans. on Nanotechnology 7, 2 (2008),
Christel Baier ( firstname.lastname@example.org) is a professor
at tu dresden, germany.
Boudewijn R. haverkort ( email@example.com) is a
professor at the university of twente, and scientific
director of the embedded Systems Institute, eindhoven,
holger hermanns ( firstname.lastname@example.org) is a
professor at Saarland university, Saarbrücken, germany.
Joost-Pieter Katoen ( email@example.com) is a
professor at rwth Aachen university, Aachen, germany.