LACL, bâtiment P2-RdC, salle des thèses: comment y aller
Abstract:Model checking is an automatic verification technique, which provides an answer to the question whether a program, given as a state-transition system, satisfies its specification, given in terms of a temporal-logic formula. Model checking is very well studied as far as boolean finite-state programs are concerned.
To take into account several sources of infinity such as an unknown number of processes or infinite data structures, the classical setting has been extended in several orthogonal directions. In the context of concurrent programs, one may ask whether a specification is satisfied independently of the number of participating processes. This question is referred to as parameterized verification. Second, a system may have to cope with variables ranging over an infinite domain such as the natural numbers or finite strings. Depending on the operations that are allowed on this domain, system executions can then be described as words over an infinite alphabet that is possibly equipped with one or several binary relations such as equality or a total order. Those words are usually referred to as data words. Many models and results from both areas, parameterized verification and data words, smoothly extend the classical finite-state approach and, in particular, provide decidable instances of the model-checking problem.
Our concern in this talk will be distributed algorithms, where an unknown number of (identical) processes cooperate to achieve a common goal. However, assuming perfectly identical processes, even simple tasks such as electing a leader cannot always be accomplished. One may, therefore, assume that every process is equipped with a unique process identifier from an unbounded domain, and that identifiers can be compared with one another wrt. a total order. Thus, when modeling distributed algorithms, one has to cope with both sources of infinity mentioned above: the number of processes and infinite data. This may be one reason why there have been only a few approaches to the formal verification of distributed algorithms.
In this talk, I survey recent developments in the areas of parameterized verification and data words, and we demonstrate how they can be exploited towards a framework for the formal verification of distributed algorithms.
Abstract:Tableau methods are used to decide the satisfiability of a given formula. We will present our tableau procedure for the full Alternating-time Temporal Logic, also called ATL*. ATL (and its extensions) is a natural framework to describe open systems, that is systems interacting with their environment. Components of the system as well as its environment are represented by means of a game where players or coalitions of players must find a strategy to reach their goal. In this presentation, we will briefly describe the syntax and the semantics of ATL*, give the general structure of the procedure and focus on the particularities needed to adapt the procedure to ATL*.