Seminars for 2008-2009

The "Centre Fédéré en Vérification" (CFV) oganizes monthly seminars on computer-aided verification.

• Program: Click here to have a look at the program. You can also see the list of the past seminars.
• Location: The seminars take place at the campus "Plaine" of the Université Libre de Bruxelles. (Click here to see a map of the campus). Click here to know how to reach the university (Campus de la plaine). Please refer to the individual seminar announcements for the exact location (building and classroom). It changes from time to time...
• Time schedule: The usual time schedule for our seminars is as follows:

  14h00 - 15h30	Invited lecture
  15h30 - 16h00	Coffee break
  16h00 - 16h30	Lecture by a CFV partner
  16h30	Discussion

• Coordinator: The coordinator of the CFV seminars is Véronique Bruyère
• Registration: People interested by the seminars and other CFV activities are kindly invited to register, simply by sending a mail to Gilles Geeraerts (gigeerae [at] ulb.ac.be). Informations concerning the CFV seminars will be sent to the originating adresses of the requests.

At 14:00 Invited talk: Regular graphs : a perfect model for infinite state systems?

• Speaker: Christophe Morvan (Université de Marne-la-Vallée, France)
• Abstract:

  There are dozens of models for infinite state systems. Indeed, Turing machine, cellular automata, pushdown systems, Petri nets, or process algebras are only major examples of such systems. Most of these systems do not provides the simplicity and efficiency of finite state systems. Finite graphs, or finite state automata, are the corner stone of computer science, it is still a very active field of research with countless applications. Infinite state systems lack that kind of universal and simple framework. Graph grammars were initially used to produce infinite sets of graphs. But in the early 90's, Courcelle used deterministic graph grammars to characterise a general class of infinite graphs: regular graphs. Recently Caucal built up a nice toolbox for studying regular graphs, and with Hassen they provided an elegant extension of visibly pushdown automata, which captures every deterministic context-free language. In this talk we will present this family (regular graphs), we will discuss on the extension of visibly pushdown automata. And finally we will present probabilistic regular graphs which are a slight, but nice generalisation of probabilistic pushdown automata (the last part being ongoing work with Nathalie Bertrand). We will try to illustrate that these graph grammars are, indeed, a perfect to for modeling infinite state systems.

At 16:00 CFV talk: Control of Infinite Symbolic Transitions Systems under Partial Observation

• Speaker: Gabriel Kalyon (ULB)
• Abstract:

  We propose algorithms for the synthesis of memoryless controllers through partial observation of infinite state systems modelled by Symbolic Transition Systems. We provide models of safe controllers both for potentially blocking and non blocking controlled systems. To obtain algorithms for these problems, we make the use of abstract interpretation techniques which provide overapproximations of the transitions set to disable. To our knowledge, with the hypotheses taken, the improved version of our algorithm provides a better solution than what was previously proposed in the literature. Our tool SMACS allowed us to make an empirical validation of our methods to show their feasibility and usability.

Friday November 28th 2008

At 14:00 Invited talk: On Termination of Linear Programs and the Skolem Problem

• Speaker: James Worrell (Oxford Computing Laboratory)
• Abstract:

  A central problem in software verification concerns the termination of linear programs, i.e. programs consisting of WHILE loops in which the guards, conditionals, and assignments are all linear (or affine). Consider the case of simple WHILE loops without conditionals, i.e., programs of the form: WHILE (Ax > c) do {x := Bx + d} where c and d are vectors, A and B are matrices, and x is a vector of variables. A longstanding open problem is whether termination for such programs is decidable, given an initial value for x. I will discuss some progress and ongoing work on this question, as well as relationships to the Skolem problem in number theory, and to the analysis of Markov chains. This is joint work with Matt Daws and Joel Ouaknine

At 16:00 CFV talk: Partial Projection of Sets Represented by Finite Automata, with Application to State-Space Visualization

• Speaker: Jean-François Degbomont (Université de Liège)
• Abstract:

  This work studies automata-based symbolic data structures for representing infinite sets. Such structures are used in particular by verification tools in order to represent the sets of configurations handled during symbolic exploration of infinite state spaces. Our goal is to develop an efficient projection operator for these representations. There are several needs for such an operator during state-space exploration; we focus here on projecting the set of reachable configurations obtained at the end of exploration. An interesting application is the state-space visualization problem, which consists in providing the user with a graphical picture of a relevant fragment of the reachable state space. For theoretical reasons, the projection of automata-represented sets is inherently costly. The contribution of this talk is to introduce an improved automata-based data structure that makes it possible to reduce in several cases the effective cost of projection. The idea is twofold. First, our structure allows to apply projection to only a part of an automaton, in cases where a full computation is not necessary. Second, the structure is able to store the results of past projection operations, and to reuse them in order to speed up subsequent computations. We show how our structure can be applied to the state-space visualization problem, and discuss some experimental results.

Friday December 12th 2008

At 14:00 Invited talk: Détermination et décidabilité des jeux stochastiques à observation partielle

• Speaker: Hugo Gimbert (LaBRI, Bordeaux)
• Abstract:

  Nous considérons les jeux d'accessibilité à deux joueurs à observation partielle, avec un nombre fini d'états et d'actions.
  Les valeurs de ces jeux étant non-calculables, nous nous intéressons à l'existence de stratégies positivement ou presque-sûrement gagnantes pour chacun des joueurs. Nous montrons le résultat de détermination suivant:
  - soit le joueur 1 peut gagner presque sûrement,
  - soit le joueur 2 peut gagner sûrement,
  - soit les deux joueurs peuvent gagner positivement.
  La mémoire nécessaire aux joueurs pour implémenter leurs stratégies varie selon les cas: doublement-exponentielle, exponentielle voire sans-mémoire. Du point de vue algorithmique, nous montrons qu'en temps doublement exponentiel, on peut décider dans laquelle de ces trois situations on se trouve, et calculer les stratégies correspondantes des deux joueurs. Ce travail est le fruit d'une collaboration avec Blaise Genest et Nathalie Bertrand de l'IRISA.

At 16:00 CFV talk: ATL with strategy contexts

• Speaker: Arnaud Da Costa Lopes (LSV / ENS-Cachan)
• Abstract:

  We extend the alternating-time temporal logics ATL and ATL* with strategy contexts and memory constraints: the first extension make strategy quantifiers to not ''forget'' the strategies being executed by the other players. The second extension allows strategy quantifiers to restrict to memoryless or bounded-memory strategies. We first consider expressiveness issues. We show that our logics can express important properties such as equilibria, and we formally compare them with other similar formalisms (ATL, ATL*, Strategy Logic, ...). We then address the problem of model-checking for our logics, providing a PSPACE algoritm for the sublogics involving only memoryless strategies and an EXPSPACE algorithm for the bounded-memory case.

February 13th 2009 : Forum Building, Room H

At 14:00 Invited talk: The General Vector Addition System Reachability Problem by Presburger Inductive Invariants" and "TaPAS : The Talence Presburger Arithmetic Suite

• Speaker: Jerome Leroux (LaBRI, Bordeaux)
• Abstract:

  The reachability problem for Vector Addition Systems (VAS) is a central problem of net theory. The general problem is known decidable by algorithms exclusively based on the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney decomposition. This decomposition can be used to prove that Parikh images of languages accepted by VAS are semi-pseudo-linear; a class of sets that can be precisely over-approximated by sets definable in the Presburger arithmetic. We provide an application of this result; we prove that if a final configuration is not reachable from an initial one, there exists a Presburger inductive invariant proving this property. Since we can decide with any decision procedure for the Presburger arithmetic if formulas denote inductive invariants, we deduce that there exist checkable certificates of non-reachability. In particular, there exists a simple algorithm for deciding the general VAS reachability problem based on two semi-algorithms. A first one that tries to prove the reachability by non-deterministically selecting finite sequences of actions and a second one that tries to prove the non-reachability by non-deterministically selecting Presburger formulas. In this presentation we show the existence of these Presburger checkable certificates proving the non-reachability. Note that the Presburger arithmetic has positive aspects: it is decidable and actually many solvers implement decision procedures. In this presentation we also provide an overview of the tool suite TaPAS (The Talence Presburger Arithmetic Suite) developed in Bordeaux. Actually TaPAS encapsulates several classical solvers : LASH, LIRA, MONA, OMEGA, PPL. TaPAS is also distributed with SaTAF, the BDD-like library used for encoding Presburger formulae to automata and the very first implementation of an algorithm decoding automata to Presburger formulae. This is joint work with Gérald Point.
  Some external links:
  "TaPAS : The Talence Presburger Arithmetic Suite" (TACAS'09)
  http://altarica.labri.fr/wiki/tools:tapas:start
  http://www.labri.fr/perso/leroux/publi/Author/LEROUX-J.html
  "The General Vector Addition System Reachability Problem by Presburger Inductive Invariants" (Submitted)
  http://hal.archives-ouvertes.fr/hal-00272667/fr/
  "Least Significant Digit First Presburger Automata" (Extended version of LICS'05)
  http://hal.archives-ouvertes.fr/hal-00118748/en/

At 16:00 CFV talk: TBA

• Speaker:
• Abstract:

April 3rd 2009 : NO Building, 5th Floor (Solvay Room)

At 14:30 Invited talk: Complementation and Determinization of Büchi Automata

• Speaker: Thomas Wilke, Christian-Albrechts-Universität zu Kiel.
• Abstract:

  Ever since Büchi automata were introduced about 50 years ago, attention has been paid to their complementation and determinization, the interest being twofold: First, complementation and determinization are standard problems in automata theory anyhow. Second, respective constructions are useful in concrete settings, for instance, when it comes to proving the decidability of the monadic theory of the natural numbers with successor and of the monadic theory of the infinite binary tree or when it comes to solving Church's problem. In the talk, I will review the development over the last five decades and point out recent results.

At 16:30 CFV talk: Efficient Symbolic Model Checking for Process Algebras

• Speaker: José Vander Meulen (UCL)
• Abstract:

  Different approaches have been developed to mitigate the state space explosion of model checking techniques. Among them, symbolic verification techniques use efficient representations such as BDDs to reason over sets of states rather than over individual states. Unfortunately, past experience has shown that these techniques do not work well for loosely-synchronized models. This talk presents a new algorithm that combines BDD-based model checking with partial order reduction (POR) to allow the verification of models featuring asynchronous processes, with significant performance improvements over currently available tools. We start from the ImProviso algorithm (Lerda et al.) for computing reachable states, which combines POR and symbolic verification. We merge it with the FwdUntil method (Iwashita et al.) that supports verification of a subset of CTL. Then, we present how is possible to extend this algorithm, in order to apply it with Bounded Model Checking methods for checking LTL properties. Our algorithm has been implemented in a prototype that is applicable to action-based models and logics such as process algebras and ACTL. Experimental results on a model of an industrial application show that our method can verify properties for sizes which cannot be handled by conventional model checkers.