CTIT University of Twente
Research Business & Innovation About CTIT Research Calls Looking for a job? Intranet

SYRUP

SYmbolic RedUction of Probabilistic Models

Project Manager: Prof. dr. ir. Joost-Pieter Katoen

Faculty of Electrical Engineering, Mathematics and Computer Science

Tel.: +31 53 489 5675

Email: j.p.katoen@ewi.utwente.nl

Project website:

Summary

Efficient model-checking algorithms exist for qualitative and quantitative properties for a range of probabilistic models. Their popularity is due to the presence of powerful software tools, and their wide applicability; security, distributed algorithms, systems biology, dependability and performance analysis, to mention a few. The main deficiencies of probabilistic model checking are the state explosion problem and the restricted treatment of data.

The state space grows exponentially in the size of system components and data domains. Whereas most abstraction techniques obtain smaller models by collapsing sets of concrete states at the model level, this project takes a radically different approach. We will seek and implement symbolic reduction techniques for probabilistic models. These techniques aim to reduce models by model transformations at the language level in order to minimize state spaces prior to their generation while preserving functional and quantitative properties. Our symbolic reductions will support data as first-class citizens, i.e., we will develop techniques to symbolically reduce formalisms for modeling probabilistic systems that are equipped with rich data types, allowing, e.g., probabilistic choices parameterized with data.

Our approach is based on successful symbolic transformation techniques in the traditional and timed setting, viz. linear process equations (LPEs). We will generalize and extend these techniques to probabilistic automata (PA), a model akin to Markov Decision Processes that is tailored to compositional modeling. The LPE technique is applicable to large or even infinite systems, and will be equipped with symbolic transformations such as confluence reduction, bisimulation minimization and static analysis for PA.

Project duration: 2009-2013

Project budget: 190.5 k-€

Number of person/years: 1.3 fte

Involved groups: Formal Methods and Tools (FMT)