Model Checking & Games (MCG)

PhDCourse@DISI

Location: DISI University of Genova

Date: July 19-23, 2010

Hours: 20

Teachers:
Giorgio Delzanno (Assoc. Prof., DISI, Univ. of Genova) giorgio@disi.unige.it

Arnaud Sangnier (PostDoc, DISI, Univ. of Genova) sangnier@disi.unige.it


Contents:

Course description

Per model checking si intende una famiglia di metodi formali per la verifica automatica di macchine a stati finiti (finite-state machine), un modello che puo' essere utilizzato pre rappresentare il funzionamento di design hardware, protocolli di comunicazione e sistemi concorrenti, o astrazioni di programmi. Il problema del model checking e' definito partendo da nozioni di logica matematica. Un sistema viene rappresentato come un modello di Kripke (un grafo) mentre le sue proprieta' vengono formalizzate tramite formule in logiche che esprimono proprieta' della computazione (ad es. in tutte le esecuzioni non raggiungo mai uno stato di errore). Formalmente, dato un modello ed una formula, il problema del model checking consiste nel provare automaticamente che la formula e' soddisfacibile nel modello. Nel corso presenteremo diversi formalismi che possono essere usati per descrivere proprieta' qualitative e quantitative di macchine a stati (o loro estensioni). Studieremo algoritmi e strutture dati per risolvere in maniera efficiente il problema del model checking. Inoltre vedremo come estendere il metodo al caso di macchine con spazio degli stati infinito ed in particolare a sistemi parametrici (ad esempio, sistemi costituiti da un numero finito ma arbitrario di componenti ripetute).

Infine vedremo come la game theory (teoria dei giochi), ed in particolare 2-players game, puo' essere utilizzata per rappresentare modelli di sistemi che interagiscono con un ambiente. Per questo tipo di modelli studieremo algoritmi per decidere l'esistenza di strategie vincenti e la loro applicazione per model checking di sistemi aperti.


Model checking is a formal method for  the automatic verification of finite-state models of a computer system (e.g. hardware design, abstractions of communication protocols and software code). The principle of model-checking is the following: the system is represented by a mathematical model and the property to verify is given by a logic formula. The aim of model-checking is to check whether the model satisfies the formula. In the first part of the course we present different logical formalisms (Modal Logic, Linear Temporal Locic, Branching Temporal Logic,etc.) that can be used to formally describe the temporal behavior of a computer system modelled as a finite state automaton (or Kripke structure). We will study the expressivity of these different logical formalisms and explain how the problem of model-checking can be solved efficiently. We then discuss how to extend the method to models with infinite state space (infinite-state systems). An important class of these models consists of parameterized families of finite-state automata (used to represent families of hardware design or concurrent processes). In general, the model-checking problem is undecidable for infinite-state systems. In the seminars we discuss subclasses of infinite-state systems and of verification properties that  have decidability properties. Finally we present another mathematical formalism which is more suited for the verification of open systems whose behavior depend on the action of an environment. These systems can be seen as 2-player games where the first player models the system and the second player represents the environment. The aim is then to see if there exists a way (or strategy) for player 1 to achieve an objective no matter what player 2 choose to do.  In this context we  discuss algorithms to analyze 2-player games. Furthermore, we show that there exist strong connections between model-checking of temporal logics over finite state automata and the verification of 2-player games.

Program:

Introduzione ai modelli di Kripke, automi finiti ed infiniti

Logica modale e temporale (branching e lineare)

mu-calculus

Algoritmi efficienti per model checking

Estensioni al caso di sistemi infinite-state

Giochi a 2 ruoli

Algoritmi per risolvere giochi

Relazione tra giochi e model checking


Brief introduction to Kripke structures, finite automata and infinite automata

Modal, linear and branching temporal Logic

mu-calculus

Efficient algorithms for model-checking

Toward infinite state systems

Introduction to 2-player finite state games

Algorithms to solve games

Connection between games and model-checking


Exam:

L'esame consiste in una presentazione (seminario) di 20 minuti su argomenti e materiale proposto dai docenti.


The exam will take the form of a 20 minutes oral presentation (in english).

Bibliography and material for students: