The IPA Herfstdagen are an annual five day event, dedicated to a theme that is of current interest to the IPA community.
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)
Arrival and registration (11.00 - 12.30)
12.30 - 14.00 Lunch
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
16.00 - 17.30 Boudewijn Haverkort (UT): A brief introduction into Markov Chains Abstract
17.30 - 18.30 Drinks
18.30 - 20.30 Dinner
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
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
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
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
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
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
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
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
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
17.00 - 18.30 Short research presentations by PhD students (organised by the IPA PhD council)
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
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 are based on single room)
| IPA Ph.D. students (shared room only!) | free | ||
| Speakers | free | ||
| IPA members and associated Ph.D. students |
| ||
| Associated members |
|
||
| Other participants |
|
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 closed on Wednesday November 22, 2006
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).
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).
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.