Verification & Algorithms Seminar (VAS)

December 6, 2012

The event is open to the public and free.
Venue : HOWTO
Travel to the LaBRI / Hotel in Bordeaux
Opening (Salle Patio - Bat C4 "Haut-carré")
10:00-10:15 Opening and Coffee
Invited Talks (Salle Patio - Bat C4 "Haut-carré")
10:15-11:15 A perfect model for bounded verification
Javier Esparza
A class of languages C is perfect if it is closed under Boolean operations and the emptiness problem is decidable. Perfect language classes are the basis for the automata- theoretic approach to model checking: a system is correct if the language generated by the system is disjoint from the language of bad traces. Regular languages are perfect, but because the disjointness problem for context-free languages is undecidable, no class containing them can be perfect.In practice, verification problems for language classes that are not perfect are often under-approximated by checking if the property holds for all behaviors of the system belonging to a fixed subset. A general way to specify a subset of behaviors is by using bounded languages. A class of languages C is perfect modulo bounded languages if it is closed under Boolean operations relative to every bounded language, and if the emptiness problem is decidable relative to every bounded language.We consider finding perfect classes of languages modulo bounded languages. We show that the class of languages accepted by multi-head pushdown automata are perfect modulo bounded languages, and characterize the complexities of decision problems. We also show that bounded languages form a maximal class for which perfection is obtained. We show that computations of several known models of systems, such as recursive multi-threaded programs, recursive counter machines, and communicating finite-state machines can be encoded as multi-head pushdown automata, giving uniform and optimal underapproximation algorithms modulo bounded languages.
11:15-12:15 Multi-dimension Quantitative Games: Complexity and Strategy Synthesis
Jean-Francois Raskin
In mean-payoff games, the objective of the protagonist is to ensure that the limit average of an infinite sequence of numeric weights is nonnegative. In energy games, the objective is to ensure that the running sum of weights is always nonnegative. Multi-mean-payoff and multi-energy games replace individual weights by tuples, and the limit average (resp. running sum) of each coordinate must be (resp. remain) nonnegative. These games have applications in the synthesis of resource-bounded processes with multiple resources. In this talk, I will summarize several recent results that we have obtained recently: -We prove the finite-memory determinacy of multi-energy games and show the inter-reducibility of multi-mean-payoff and multi-energy games for finite-memory strategies. -We improve the computational complexity for solving both classes of games with finite-memory strategies: while the previously best known upper bound was ExpSpace, and no lower bound was known, we give an optimal coNP-complete bound. For memoryless strategies, we show that the problem of deciding the existence of a winning strategy for the protagonist is NP-complete. -We provide an optimal symbolic and incremental algorithm to synthesis strategies in multi-energy games. -We present the first solution of multi-mean-payoff games with infinite-memory strategies. We show that multi-mean-payoff games with mean-payoff-sup objectives can be decided in NP and in coNP, whereas multi-mean-payoff games with mean-payoff-inf objectives are coNP-complete.
HDR (Salle Patio - Bat C4 "Haut-carré")
14:00-15:30 Presburger Counter Machines [PDF] [SLIDES]
Jérôme Leroux
  • Hubert Comon Professeur ENS Cachan / LSV
  • Javier Esparza Professeur Technische Universität München, Allemagne
  • Nicolas Halbwachs Directeur de Recherche CNRS / Verimag
  • Denis Lugiez Professeur Université de Provence / LIF
  • Anca Muscholl Professeur Université de Bordeaux-1 / LaBRI
  • Jean Éric Pin Directeur de Recherches CNRS / LIAFA
  • Jean François Raskin Professeur Université Libre de Bruxelles, Belgique
  • Philippe Schnoebelen Directeur de Recherche CNRS / LSV

Critical, embedded or real-time systems have many applications from the control (automotive and avionic industry), to signal processing(audio or video data, GPS navigation systems) and communication (cellphones, internet). Usually these systems are infinite since they are based on potentially unbounded variables: integervariables (program counters, number of processes connected to a remoteserver) or real numbers (clocks modeling elapsing time), communication channels, stacks, memory heap, and so on. Whereas the verification offinite state systems is algorithmically decidable (and there existefficient tools), the verification of infinite state systems is not a sinecure. In this presentation we introduce frameworks for deciding reachability problems of infinite state systems. The frameworks are illustrated by the Presburger counter machines, a class of machines manipulating a finite set of counters with semantics definable in the first order logic over the natural numbers with the addition, also known as the Presburger arithmetic.
Pot (Atrium du Bâtiment A30)