March 2-5, 2010 IT University Copenhagen, Denmark | organised and funded by ARTIST |
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. |
(c) Artist Consortium, All Rights Reserved - 2006, 2007, 2008, 2009