Quantitative Model Checking 2010

March 2-5, 2010      IT University Copenhagen, Denmark organised and funded by ARTIST 

Program

There will be lectures and exercise sessions on the theory of quantitative model checking, and practical sessions providing some hands-on tool experience. The precise schedule is still evolving; below is the current state. (Click on the titles to see the abstracts.)
 
Tuesday 2 March

Finite-state model checking

Wolper Temporal logics and explicit-state model checking
This lecture will introduce linear and branching time temporal logics and discuss the link between these logics and finite automata. Focusing on the linear-time case, the construction of automata from temporal logic formulas will be fully described as well as the classical automata-based model checking algorithms.
Heljanko Bounded model checking for finite-state systems
This lecture will cover bounded model checking (BMC) for finite state systems. BMC is a symbolic model checking technique applying propositional satisfiability (SAT) solving techniques to model checking. We will cover the basics of BMC, encoding transition relations, encoding linear temporal logic formulas, as well as advanced topics in BMC.
Cimatti Symbolic model checking

Wednesday 3 March

Real-time model checking

Larsen Introduction to timed automata
In this talk we introduce the basic definitions of timed automata and show their relevance for modelling real-time systems.
Bouyer-Decitre Decidability
We introduce the region abstraction, which are a cornerstone notion for most decidability results in timed automata.
Markey Timed temporal logics
We extend classical temporal logics with timing constraints. In the general case, this leads to undecidability, but decidability can be preserved in some cases.
Larsen UPPAAL (tool session)

Bouyer-Decitre Timed games
Timed games are a two-player extension of timed automata, useful for representing open systems. We define those games and present recent decidability results.
Markey Priced timed automata
Priced timed automat are another extension of timed automata with extra quantitative information (resource consumption for instance). We present some recent results in this setting.
Thursday 4 March

Probabilistic model checking

Baier Probabilistic computation tree logic and quantitative linear-time properties
The tutorial provides an introduction to the model checking techniques for probabilistic systems modelled by finite-state discrete-time Markov chains and Markov decision processes. It consideres the logic probabilistic computation tree logic and the quantitative analysis against linear-time properties using omega-automata, explains the treatment of fairness assumptions and the main ideas of partial order reduction for probabilistic parallel systems.
Katoen Model checking and abstraction of continuous-time Markov chains
This lecture will provide an introduction to the verification of CTMCs, a model that combines discrete probabilistic branching with random state residence times. CTMCs are prominent in performance and dependability evaluation, occur as semantic model of high-level modeling formalisms such as stochastic Petri nets and process algebras, and are frequently used in systems biology. We will introduce a branching-time logic on CTMCs, and explain in detail how the validity of these logical formulas can be model-checked on finite CTMCs. In order to handle large, or even infinite CTMCs, we introduce an abstraction technique that fits within the realm of three-valued abstraction methods. The key ingredients of this technique are a partitioning of the state space combined with an abstraction of transition probabilities by intervals. We will present the underlying theory of this abstraction, some examples, and indicate how such abstraction can be applied in a compositional manner.
Parker Probabilistic model checking in practice
This tutorial will cover some of the practical aspects of probabilistic model checking. In particular, it will focus on the use of PRISM, a widely used tool for verification of discrete-time Markov chains, continuous-time Markov chains, Markov decision processes and extensions of these models with costs and rewards. The tutorial will cover PRISM’s modelling and property specification languages and give an overview of its underlying techniques. It will also offer hands-on experience with the tool itself.
Friday 5 March

Hybrid model checking

Raskin An introduction to hybrid automata
In this lecture, I will review hybrid automata: their syntax, semantics, and basic semi-algorithms for their analysis.
Frehse Tools for hybrid systems reachability
This lecture covers algorithms for computing the reachable states of two fundamental classes of hybrid systems, linear hybrid automata and piecewise affine systems, and how they can be extended to more general classes. The lecture is accompanied by a hands-on lab session.
Fränzle Automatic analysis of hybrid systems
Embedded digital systems have become ubiquitous in everyday life. Many such systems, including many of the safety-critical ones, operate within or comprise tightly coupled networks of both discrete-state and continuous-state components. The behavior of such hybrid discrete-continuous systems cannot be fully understood without explicitly modeling and analyzing the tight interaction of their discrete switching behavior and their continuous dynamics, as mutual feedback confines fully separate analysis to limited cases. Tools for building such integrated models and for simulating their approximate dynamics are commercially available. Simulation is, however, inherently incomplete and has to be complemented by verification, which amounts to showing that the coupled dynamics of the embedded system and its environment is well-behaved, regardless of the actual disturbance and the influences of the application context, as entering through the open inputs of the system under investigation. Basic notions of being well-behaved demand that the system under investigation may never reach an undesirable state (safety), that it will converge to a certain set of states (stabilization), or that it can be guaranteed to eventually reach a desirable state (progress).
Within this lecture, we concentrate on automatic verification and analysis of hybrid systems, with a focus on symbolic methods manipulating both the discrete and the continuous state components symbolically by means of predicative encodings and dedicated constraint solvers. We provide a brief introduction to hybrid discrete-continuous systems, demonstrate the use of predicative encodings for compactly encoding operational high-level models, and continue to a set of constraint-based methods for automatically analyzing different classes of hybrid discrete-continuous dynamics. Covering the range from non-linear discrete-time hybrid systems to probabilistic hybrid systems, advanced arithmetic constraint solvers will be used as a workhorse for manipulating large and complex-structured Boolean combinations of arithmetic constraints arising in their analysis tasks.


The program will start at 9:00 on all days. On Friday, we will finish around 17:00.

(c) Artist Consortium, All Rights Reserved - 2006, 2007, 2008, 2009

Réalisation Axome - Création de sites Internet