The purpose of the workshop is to bring together students and researchers from the computer science, dynamical systems, and control communities on the general theme of verification and hybrid systems. The workshop will emphasize the dynamical aspect of verification methods.

The first day of the workshop will be an introductory minicourse by Professor R. Alur (University of Pennsylvania, USA). This minicourse will emphasize the dynamical aspects of hybrid systems and verification. The second day will consist of invited talks. All talks will be in tutorial format and informal discussions between the participants will be encouraged throughout the two days.

Annual dynamics workshops. This is the fifth of a series of annual workshops held in Belgium on topics related to dynamical systems. The goal of this series of workshops is to gather researchers from different disciplines around the general theme of dynamical systems in a casual and informal athmosphere.

July 16 One day introductory minicourse

Hybrid Systems: Modeling and Verification
Rajeev Alur (Department of Computer and Information Science, University of Pennsylvania, USA).

Part 1. Modeling and Semantics
Part 2. Decidability, Verification, and Control
Part 3. Symbolic Reachability Analysis
Part 4. Application Domains

July 17 Invited lectures

9:00 9:15  Introduction.
Pierre Wolper (University of Liège, Belgium)
 
9:15 10:15  About Some Canonical Structures Used in Model Checking.
Laurent Fribourg (Laboratoire Spécification et Vérification, Ecole Normale Supérieure de Cachan, France).
Laurent will introduce Ordered Binary Decision Diagrams and Difference Bounded Matrices. Both notions are used in verification methods. He will focus his attention on uniqueness properties of reduced forms.

10:15 11:15  Symbolic representation systems for infinite state spaces.
Bernard Boigelot (University of Liège, Belgium)

11:45 12:45  Analysis of Safety and Liveness Properties of Parametric Counter/Clock Automata.
Ahmed Bouajjani (LIAFA, University of Paris 7, France)
Ahmed will introduce Parametric Difference Bound Matrices and show how these can be used to address the problem of automatic analysis of parametric counter and clock automata. This material is based on recent papers in CAV'00 and SAS'01.

14:30 15:30  Noise and Decidability
Eugene Asarin (VERIMAG, Grenoble, France).
Many properties of hybrid systems are algorithmically undecidable. In practice however, systems are only known up to a certain degree of accuracy and are subject to noise and perturbations. Eugene will consider various classes of hybrid systems and will analyse how noise affects decidability for these classes. His presentation will be based on recent attempts by Asarin-Bouajjani, Henzinger-Raskin and others to formalize the impact of noise on computational capabilities of hybrid systems.

15:30 16:30  Efficient Verification Tools for Real-Time and Hybrid Systems. From Ideas to Usages.
Kim Larsen (BRICS, Aalborg University, Denmark)
There are a number of softwares for automatic verification of real-time and hybrid systems. Kim will describe the development of the software UPPAAL that is based on a variety of newly developed, efficient data structures and algorithms for symbolic representation and manipulation of the state-space of real-time and hybrid systems. In his presentation (including an online demo) he will emphasise the evolution of the algorithms and datastructures underlying the software, and their impact on performance. He will also present experiences with industrial collaborations.

Registration is by email. If you wish to participate in this workshop, please send your name and surname, affiliation and email to dynamics@inma.ucl.ac.be. There are no registration fees. The deadline for registration is July 1st.

The workshop will be held in the main building of the Royal Academy of Science in Brussels. The academy is located in central Brussels, next to the Royal Palace and at walking distance from most facilities. The academy is easily accessible by public transportation (Palais des Académies, Rue Ducale 1, B-1000 Brussels, underground station "Trône" or "Art-Loi").

Vincent Blondel, University of Louvain
Bernard Boigelot, University of Liège
Jean-François Raskin, University of Brussels
Rodolphe Sepulchre, University of Liège

Fond National de la Recherche Scientifique (FNRS).
Académie Royale des Sciences, Lettres et Beaux-Arts de Belgique (classe des sciences).

The Conference on Computer Aided Verification (CAV01) in Paris starts right after the workshop. Brussels is at 1h30 distance from Paris by train.