On the Dutch side, the participating Universities are the Radboud University Nijmegen and the University of Twente.

The German participating Universities are the RWTH Aachen, the Technische Universität Dresden, the Saarland University, and the University of the Federal Armed Forces Munich.

As of January 2005, VOSS is in its second phase. For information on the first phase (2001-2004) see the homepage of VOSS I and its

final report.

The Voss II project aims at the integration of modelling and
computer-aided verification techniques for the analysis of complex
systems with stochastic behaviour. Rather than proving that systems
will always behave correctly, we aim at establishing properties such as
"The probability that an airbag will be deployed inadvertently during
its operational life is less than 10^{-9}". Our goal is to
adapt and extend some prominent techniques that have been successful
for modelling and assessing qualitative characteristics of computer
systems to a stochastic setting. Modelling formalisms such as
input-output automata and process algebra, and verification techniques
such as model checking will be thoroughly investigated. We plan to
apply these techniques to model, analyse, and optimise systems
described as Markov processes, Markov decision processes, and related
formalisms.

The joint research activities are focussed on the following four research strands:

**Semantic models and equivalences. **The goal is to add
stochastic features to existing modelling frameworks, such as
input-output automata, UML statechart diagrams, or the modelling
language of tools such as MoDeST. We wish to
develop a uniform framework to reason about non-determinism,
concurrency, randomisation and time. We also plan to investigate
several notions of testing, process equivalences and other
implementation relations, in order to provide these languages with an
abstract, well-understood semantics and study the impact of process
equivalences as basis for abstraction purposes.

**Analysis techniques and tools.** For industrial use, it is
essential that future tools (a) can handle much bigger systems, and (b)
support a richer class of models and properties than the currently
available tools. Problem (a) is an especially challenging one, since
the number of a system's states typically grows exponentially in the
number of components or state variables. This problem will be attacked
via two routes, namely symbolic state space representation and
abstraction techniques. We study variants of classical multi-terminal
binary decision diagrams in order to obtain compact representations of
huge Markov models, and develop new methods for the symbolic
quantitative analysis. We will develop abstraction techniques for
continuous-time Markov decision processes, whose effectiveness will be
investigated empirically. In order to advance the state-of-the-art of
area (b), the project focuses on temporal logic model checking, where
we will develop more expressive temporal logics, being capable of
expressing path-based and reward-based properties.

**Games and controller synthesis.** We address the question
of how to schedule controllable events in a non-deterministic
probabilistic setting such that a given specification is fulfilled.
This will be perfomed for models with discrete probabilities or
stochastic timing (with non-determinism).

**Case Studies.** The techniques and tools developed in the
project will be used to conduct case studies of industrial relevance.

- F. W.Vaandrager
- J. Berendsen

- M. Hendriks

- C. Baier
- T. Blechmann
- N. Betrand

- F. Ciesinski
- M.
Groesser

- J. Klein
- S. Klüppelholz

- K. Lampka
- J.
Schuster

- M. Siegle
- M. Riedel

- Erika Abraham
- H.
Bohnenkamp

- T. Han
- J.-P.Katoen
- T. Noll
- M. Neuhaeusser
- Daniel Willems
- I. Zapreev

24. - 25.01.2005: Saarbrücken/Germany (Agenda)

12. - 13.09.2005: Munich/Germany (Agenda)

12. - 13.01.2006: Twente/Netherlands (Agenda)

28. - 29.09.2006: Kerkrade/Netherland (Agenda)

08. - 09.02.2007: Dresden/Germany (Agenda)

12. - 16.11.2007: Leiden/Netherlands

K. Lampka, last modified 10/2006