Distributed Verification of Finite-State Probabilistic Systems
The project concentrates on verification methods that are appropriate to reason about probabilistic aspects of parallel and distributed systems. The probabilistic aspects have to be taken into account when one models a system that reacts on the stimuli of the environment and interacts with the environment. The environment could be a physical process which is probablistic in its nature. Porbabilistic choices are often used to model uncertainties, e.g. when the sytem is too complex and a kind of abstraction has to be applied to model it. Yet another example are systems based on randomized algorithms.
The aim of the project is to develop parallel and distributed methods and algorithms for verification of temporal properties of finite-state probabilistic systems. The ultimate goal of the project is to enrich DiVinE with tools enabling automatic distributed verification of large probabilistic systems.Researchers
Ivana Cerna (project leader), Lubos Brim, Jiri Barnat, Milan Ceska, Jana Tumova
Publications
J. Barnat, L. Brim, I. Cerna, M. Ceska, J. Tumova: Distributed Qualitative LTL Model Checking of Markov Decision Processes. Technical Report FIMU-RS-2006-04, Faculty of Informatics, Brno. (pdf)Meetings
The groups meets each Monday at 10:00 in Room C408.