A Probabilistic LTL Model Checker
|
Supervisor |
|
|
Suitable for |
Abstract
The goal of this project is to write a program that model checks a
Markov chain against an LTL formula, i.e., calculates
the probability
that formula is satisfied. The two main algorithmic tasks are to
efficiently compile LTL formulas
into automata and then to solve
systems of linear equations arising from the product of the Markov
chain and the
automaton. An important aspect of this project is to
make use of an approach that avoids determinising the automaton
that
represents the LTL formula.
Suitable background courses for this project include (one of)
Probabilistic
Verification, Computer-Aided Formal Verification, and
Automata Logics and Games.
Reading:
J-M.
Couvreur, N. Saheb and G. Sutre. An optimal automata approach to
LTL model checking of probabilistic systems. Proceedings
of LPAR'03,
LNCS 2850, Springer 2003.