Verification & Algorithms Seminar (VAS)

December 6, 2012

Registration
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 protagontr> is to e optiage c/tip corre>

<(resp. running sum) is NP-complete. -We provide an optimal symbolic and incremental algorithm to synthesis solution b rmulti-mean-payoff games with pnfinite-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-pnf objectives are coNP-complete.
HDR (Salle Patio - Bat C4 "Haut-carré")
14:00-15:30 Presburger Counter Machines [PDF] [SLIDES]
Jérôme Leroux
Jury:
  • Hubert Comon Professeur ENS Cachan / LSV
  • Javier Esparza Professeur Techntrche Universität München, Allemagne
  • Nicolas Halbwachs Directeur de Recherche CNRS / Verimag
  • Dentr Lugiez Professeur Université de Provenc
  • Anca Murcholl Professeur Université de Bordeaux-1
  • 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 pnfinite sinc unbounded variables: integervariables (program counters, number b rprocesses 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 tipre existefficient tools), the verification of pnfinite state systems is not a sinecure. In this presentation we introduc order logic over the natural numbers with the addition, also known as the Presburger arithmetic.
Pot (Atrium