IPA Herfstdagen on Stochastic Systems

Best Western Hotel Marijke, Bergen (NH),
November 27 - December 1 2006

The IPA Herfstdagen are an annual five day event, dedicated to a theme that is of current interest to the IPA community.

Stochastic Systems

Traditionally, a distinction is made in computer science between functional (qualitative) and non-functional (quantitative or performative) properties of systems. Models and techniques for the analysis and validation of these two kinds of properties were developed in separate communities: researchers in Formal Methods concentrated on the qualitative properties of systems, whereas researchers in Performance Analysis focussed on quantitative properties.

In modern systems, like embedded and networked systems, the distinction between functional and performance properties is getting blurred: both kinds of properties are of equal importance, and often properties of one kind affect properties of the other kind. This was recognized in the '90's, when a move towards integrated frameworks started, in which methods and techniques from Formal Methods are brought together with probabilistic and stochastic approaches from Performance Analysis.

Researchers in IPA have played an active role in bringing about this synthesis, and the research school has dedicated its Lentedagen to this topic in 1999 and an EEF Summer School in 2000. The aim of this year's Herfstdagen is to present an overview of the current state of this flourishing research area. The program for the event is composed by Jos Baeten (TU/e), Boudewijn Haverkort (UT), Joost-Pieter Katoen (RWTH Aachen), and Frits Vaandrager (RU).

The Herfstdagen will present different approaches to the modelling and analyses of stochastic and probabilistic systems (automata, process algebra, model checking), and also highlight applications of these approaches in other domains (such as biology). To keep the program self-contained, a tutorial on the central concepts of stochastic and probabilistic methods has been included on Monday afternoon.

Like last year, the IPA PhD council is organising an "open session", where PhD students can give short presentations on their research. If would like to participate, please contact Mohammad Torabi Dashti (Mohammad.Dashti "at" cwi.nl). A new feature for this year's Herfstdagen is the "clinic" on PRISM, a probabilistic symbolic model checker that is developed at the University of Birmingham. Dave Parker, a member of the core development team, will give a half day introduction to the tool consisting of a tutorial combined with hands-on experience (bring your laptop!)

Monday November 27

Arrival and registration (11.00 - 12.30)

12.30 - 14.00 Lunch

Theme: Algorithms

Session: Randomised distributed algorithms

14.00 - 14.45 Wan Fokkink (VU): Leader election for anonymous rings Abstract Paper

14.45 - 15.30 Henrik Bohnenkamp (RWTH Aachen): Are you still there? Abstract Paper

15.30 - 16.00 Coffee & tea

Introduction

Tutorial

16.00 - 17.30 Boudewijn Haverkort (UT): A brief introduction into Markov Chains Abstract

17.30 - 18.30 Drinks

18.30 - 20.30 Dinner

Tuesday November 28

Theme: Model checking

Session: Discrete Time Markov Chains

09.00 - 09.45 Joost-Pieter Katoen (RWTH Aachen): Probabilistic computation tree logic Paper

09.45 - 10.30 Tingting Han (RWTH Aachen): Counterexamples in probabilistic model checking Abstract

10.30 - 11.00 Coffee and tea

Session: Continuous Time Markov Chains

11.00 - 11.45 Boudewijn Haverkort (UT): Model checking CSL

11.45 - 12.30 Lucia Cloth (UT): CSRL - Model checking performability propertiesPaper

12.30 - 13.30 Lunch

Session: Infinite state models

13.30 - 14.15 Anne Remke (UT): CSL model checking algorithms for QBDs Abstract

14.15 - 15.00 Nikola Trcka & Jasen Markovski (TU/e): Lumping Markov Chains with Silent Steps Abstract Paper

15.00 - 15.45 Daniel Willems (RWTH Aachen): Abstraction for infinite Continuous Time Markov Chains Abstract

15.45 - 16.15 Coffee and tea

Theme: Automata

16.15 - 17.00 David Jansen (UT): StoCharts = Stochastic StateCharts, Model and Analysis Abstract

17.00 - 17.45 Ana Sokolova (RU):Probabilistic automata - types and semantics Abstract

Wednesday November 29

09.00 - 09.45 Frits Vaandrager (RU): Switched probabilistic i/o automata

09.45 - 10.30 Jasper Berendsen (RU): Probably on time and within budget Abstract

10.30 - 11.00 Coffee and tea

Theme: Process algebra

11.00 - 11.45 Jos Baeten (TU/e): Probabilistic and stochastic process algebra

11.45 - 12.30 Suzana Andova (NTNU Trondheim): Silent transitions in probabilistic systems Abstract

12.30 - 13.30 Lunch

13.30 - 14.15 Jasen Markovski (TU/e): Embedding real-time in stochastic process algebras Abstract Paper

14.15 - 15.00 Holger Hermanns (Universität des Saarlandes): Modest modeling of hard and softly timed systems Abstract Presentation

15.00 - 15.30 Coffee and tea

Theme: Modeling in other domains

Session: Biological systems

15.30 - 16.15 Tessa Pronk (UvA): Simulating gene expression in a computer architecture evaluation workbench Abstract

16.15 - 17.00 Verena Wolf (Mannheim): Markov models for biochemical reaction networks Abstract

17.00 - 17.45 Dragan Bosnacki & Erik de Vink (TU/e): Viewing biological networks through PRISM Abstract

18.30 - 20.00 Dinner

20.30 - ..... Social Event

Thursday November 30

Theme: Markov decision processes

09.00-10.00 Christel Baier (TU Dresden): Quantitative analysis of randomized protocols Abstract Paper 1 Paper 2 Paper 3 Paper 4

10.00 - 10.30 Coffee and tea

Clinic: PRISM

Dave Parker (Birmingham)

10.30 - 12.30 PRISM tutorial and demo

12.30 - 14.00 Lunch

14.00 - 16.30 PRISM lab session

During this lab session, participants will receive hands-on training with PRISM, by working out a number of excercises with the tool. Everything regarding the tool is on or linked from the main PRISM web site at: http://www.cs.bham.ac.uk/~dxp/prism/. We invite participants to install the latest version of PRISM (3.1) from the site on their laptops before coming to the Herfstdagen (although it will be possible to do this at the venue). This version can be found in the "Download" section of the website, with precompiled binary distributions (but also source code) for the following platforms: Linux, Mac OS X, Windows and Solaris. Installation instructions are also online but should you encounter problems, you can post to the help forum, which can be accessed via the "Support" section of the website. Other useful resources are the online manual and tutorial (the latter will be updated before the Herfstdagen), which can be found in the "Documentation" section of the website.

16.30 - 17.00 Coffee and tea

Open session

17.00 - 18.30 Short research presentations by PhD students (organised by the IPA PhD council)

Friday December 1

Theme: Modeling in other domains

Session: Security

09.00 - 09.45 Peter van Rossem (RU): Probabilistic aspects of computer security Abstract

09.45 - 10.30 Ichiro Hasuo (RU): Probabilistic anonymity via coalgebraic simulations Abstract Paper

10.30 - 11.00 Coffee and tea

Session: Systems

11.00 - 11.45 Elena Bortnik (TU/e): Verification of Chi models with Uppaal: an industrial case study Abstract

11.45 - 12.30 Anton Wijs (CWI): Extending directed model checking to quantitative model checking AbstractPaper

12.30 - 14.00 Lunch and departure

Costs

(Costs are based on single room)

IPA Ph.D. students (shared room only!) free
Speakers free
IPA members and associated Ph.D. students
5 days 500,-
1 day 100,-
Associated members
5 days 625,-
1 day 125,-
Other participants
5 days 800,-
1 day 160,-

Please note that Ph.D. students who are not in IPA will be charged as IPA members if they belong to a research school that is associated with IPA, and as an other participant otherwise.

To make maximal use of the available capacity, we process applications on the following basis: Registrations are treated "first come, first serve". All Ph.D. students (IPA and non-IPA) have to share a room. Others may also be asked to share if we run out of rooms.

Please remit the amount due, to our bank account with the ABN/AMRO. Account number: 60.27.60.690, in the name of V.A.J. Borghuis e/o S.M.H.J. Joosten, Den Dolech 2, 5600 AM Eindhoven. Please mention participation "IPA Herfstdagen 2006"

Registration

Registration closed on Wednesday November 22, 2006

How to get to Hotel Marijke

Bergen is a little village near the North Sea coast in the province of Noord-Holland, near the city of Alkmaar (it should not be confused with "Bergen aan zee", which is a separate village directly on the coast, a few kilometers more to the west). The Hotel Marijke is situated in the Dorpsstraat 23-25 of Bergen (postcode 1861 KT).

By public transport

Take a train to NS station Alkmaar. From almost anywhere in the Netherlands this means taking a train in the direction of Den Helder, and disembarking at Alkmaar (there are direct trains to Den Helder from, among other stations, Amsterdam CS, Utrecht CS, and Nijmegen). In Alkmaar take (Connexxion) bus 160, in the direction of Bergen. Get off after about 10 minutes at the "Natteweg" (ask the bus driver to drop you off at this stop). Cross the street, enter the Natteweg. The Dorpsstraat is the first street to the right. You arrive at the hotel after about a 4-minutes walk. See schedule at the Connexxion website for times and stops of bus 160 Regio Noordwest: Heerhugowaard - Bergen (in Dutch).

By car

The website of the hotel provides a link to a Dutch website for planning your journey by car, the ANWB-planner, type in 1861 KT as the "postcode" for the destination. If you like a more international perspective, you could use the Michelin planner.