Validation of Stochastic Systems (VOSS)


VOSS is a research collaboration between the Netherlands and Germany within the NWO-DFG bilateral cooperation program.
On the Dutch side, the participating Universities are the University of Nijmegen and the University of Twente.
The German participating Universities are the RWTH Aachen, the University of Bonn and the University of Erlangen-Nuernberg.

Summary of the project

This project is concerned with modelling and verification of stochastic aspects of computer systems such as distributed
systems, networks and communication protocols. These aspects are essential to reason about the performance and
dependability characteristics of systems, as well as to assess the correctness of probabilistic, distributed algorithms and
protocols.  The project aims at the integration of modelling and computer-integrated verification techniques for the
analysis of complex systems with stochastic behaviour. The goal is to adapt and extend some prominent techniques that
have been proven to be successful for modelling and assessing qualitative characteristics of computer systems to a
stochastic setting. Modelling techniques, such as input-output (I/O) automata and process algebra, and verification
techniques, such as model checking will be thoroughly investigated. Concretely, we plan to extend existing collaboration
between the partners to apply these techniques to model, analyse, and optimise systems described as Markov processes.

Research Aims

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

Model checking very large stochastic models. We  intend to investigate several abstraction techniques that allow
for symbolic model checking algorithms where sets of states are represented and analysed rather than single states.
The concepts of abstraction and symbolic model checking are well-known for non-probabilistic systems where the
original large (possibly infinite) system is replaced by an (in some sense) equivalent but smaller finite system. Thus,
symbolic methods can be used for verifying special types of infinite systems as well as large finite state systems.

Extension of Markov model checking techniques. We intend to broaden the range of Markov models that model
checking is applicable to. Our primary focus is on Markov reward models, and on action-labelled Markov chains, but
also semi-Markov and MDPs are of interest.

Enhancing construction methods for stochastic models. We intend to integrate probabilistic automata and
stochastic automata (GSMPs). Our aim is to transfer beneficial results obtained for probabilistic automata such as
compression algorithms based on normed weak bisimulations, to stochastic automata.



From Nijmegen (Informatics for Technical Applications) :

From Twente (Formal Methods and Tools):

From Twente (Design and Analysis of Communication Systems)

From Bonn (Theoretical Computer Science and Formal Methods):

From Erlangen (Stochastic Modelling and Verification Group):

From Saarbrücken  (Dependable Systems & Software)

Past Events:

December 8-11, 2002: GI/Dagstuhl Research Seminar Validation of Stochastic System

Project Meetings

28.06. 2001 - 29.06. 2001 Enschede/Twente (Agenda)
22.11.2001 - 23. 11.2001 Bonn  (Agenda)
14.03.2002 - 15.03.2002 Nijmegen  (Agenda)
08.12.2002 - 11.12.2002 Dagstuhl (on behalf of the GI/Dagstuhl Research Seminar )
02.06. 2003 - 03.06. 2003 Erlangen (Agenda)
12.11.2003 - 13.11. 2003 Bonn (Agenda)
05.04.2004 - 06.04.2004 Maastricht (Agenda)


C. Baier, H. Hermanns, B. Haverkort and J.-P. Katoen.
Automated performance and dependability evaluation using model checking.
In M. Calzarossa and S. Tucci, editors,
Performance Evaluation of Complex Systems: Techniques and Tools
volume 2459 of Lecture Notes in Computer Science.
Rome, Italy. Springer-Verlag, 2002, pages 261--289.

C. Baier, J.-P. Katoen, H. Hermanns and B. Haverkort.
Simulation for continuous-time Markov chains.
In L. Brim, P. Jancar, M. Kretinzki and A. Kucera, editors, Concurrency
Theory (CONCUR), volume 2421 of Lecture Notes in Computer Science,
pages 338--354.  Brno, Czech Republic, 2002.

H. Bohnenkamp, P. van der Stok, H. Hermanns, and F. Vaandrager.
Cost-Optimisation of the IPv4 Zeroconf Protocol.
In Proceedings of the 2003 International Conferences on Dependable Systems and Networks,
June 22-25, San Fransisco CA, IEEE CS Press, pages 531-540, June 2003.

B. Haverkort, H. Hermanns, J-P. Katoen, C. Baier.
Model Checking CSRL-Specified Performabilitiy Properties.
Fifth International Workshop on Performability Modeling of Computer and Communication Systems,
Erlangen, Germany, Sept. 2001.
Appeared in Arbeitsberichte des Instituts für Informatik, Band 34, Nr. 13, Sept. 2001, Universität Erlangen-Nürnberg.

B. Haverkort, L. Cloth, H. Hermanns, J.-P. Katoen and C. Baier.
Model-checking performability properties.
International IEEE Conference on Dependable Systems and Networks (DSN),
pages 103--113.  Washington (DC), USA, 2002.

H. Hermanns, J-P. Katoen, J. Meyer-Kayser, M. Siegle.
Implementing a Model Checker for Performability Behaviour.
Fifth International Workshop on Performability Modeling of Computer and Communication Systems,
Erlangen, Germany, Sept. 2001.
Appeared in Arbeitsberichte des Instituts für Informatik, Band 34, Nr. 13, Sept. 2001, Universität Erlangen-Nürnberg.

H. Hermanns, J.-P. Katoen, J. Meyer-Kayser and M. Siegle.
A tool for model checking Markov chains.
Int. Journal on Software Tools for Technology Transfer, 20 pages,
Springer, 2003 (to appear).

M. Kuntz, M. Siegle
Deriving symbolic representations from stochastic process algebras
In Process Algebra and Probabilistic Methods, Joint Int. Workshop PAPM-PROBMIV 2002,
H. Hermanns, R. Segala, editors, pp. 188-206, Springer LNCS 2399

N.A. Lynch, R. Segala and F.W. Vaandrager.
Compositionality for Probabilistic Automata.
In Proceedings CONCUR'03, Marseille, France, September 3-5, 2003. To appear

M.I.A. Stoelinga and F.W. Vaandrager.
A Testing Scenario for Probabilistic Automata.
In J.C.M. Baeten, J.K. Lenstra, J. Parrow and G.J. Woeginger, editors,
Proceedings ICALP'03, LNCS 2719, pages 407-418. Springer-Verlag, 2003.

under construction

Last modified 24.09.2003
Matthias Kuntz