Seminars for 2009-2010

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 Nicolas Maquet (nmaquet [at] ulb.ac.be). Informations concerning the CFV seminars will be sent to the originating adresses of the requests.

Upcoming Seminars

The CFV seminar dates for 2010-2011 will be announced at a later time.


Past Seminars

May 28th 2010 : NO Building, 5th Floor (Solvay Room)

At 14:00 Invited talk: Quantitative languages: weighted automata and beyond

  • Speaker: Laurent Doyen, LSV - ENS Cachan, Paris.
  • Abstract:

    Quantitative generalizations of classical languages, which assign to each word a real number instead of a boolean value, have applications in modeling resource-constrained computation. We use nondeterministic weighted automata (finite automata with transition weights) to define classes of quantitative languages over infinite words. The value of a word w is the maximal value of all runs over w, and the value of a run r is a function of the sequence of weights that appear along r. We consider several natural functions such as Max, LimSup, LimInf, limit average (or mean-payoff), and discounted sum of transition weights.

    We study the natural generalization of decision problems and closure properties from automata theory: threshold-emptiness, threshold-universality, language inclusion, language equivalence, and closure under the pointwise operations max(L,L'), min(L,L'), 1-L (which generalize the boolean operations), and sum L + L' where L, L' are quantitative languages.

    In this survey, we give an overview of the results and open questions about decidability, expressiveness (including determinization), and closure properties of the various classes of quantitative languages defined by weighted automata.

    As none of these classes enjoys both full decidability and positive closure properties (even if we consider an extension to alternating automata), we present mean-payoff automaton expressions, a new syntax to specify quantitative languages with limit-average value. We show that this class of quantitative languages is robust and decidable: it is closed under the four pointwise operations, and we show that all decision problems are decidable. We also present for the first time an algorithm to compute distance between two quantitative languages (given as mean-payoff automaton expressions)

At 16:00 CFV talk: Lattice-Valued Binary Decision Diagrams

  • Speaker: Nicolas Maquet, ULB
  • Abstract: We introduce a new data structure, called Lattice-Valued Binary Decision Diagrams (or LVBDD for short), for the compact representation and manipulation of functions of the form θ : 2^P -> L, where P is a finite set of Boolean propositions and L is a finite distributive lattice. Such functions arise naturally in several verification problems. LVBDD are a natural generalisation of multi-terminal ROBDD which exploit the structure of the underlying lattice to achieve more compact representations. We introduce two canonical forms for LVBDD and present algorithms to symbolically compute their conjunction, disjunction and projection. We provide experimental evidence that this new data structure can outperform ROBDD for solving the finite-word LTL satisfiability problem.

May 7th 2010 : NO Building, 9th Floor

At 14:00 Invited talk: Coordinating strategies with imperfect information

  • Speaker: Dietmar Berwanger, LSV - ENS Cachan, France.
  • Abstract:

    A classical paper of Reif on games with imperfect information shows that games for one player against nature can be solved by a power-set construction yielding larger games of perfect information. Similar in spirit to the determinisation of automata, the construction represents (an abstraction of) the knowledge that a player has about the play history. In the same paper, it is shown that the problem of deciding whether a coalition of players can coordinate to win with finite-state strategies is in general undecidable, essentially because players need to keep track of an infinite amount of information.

    In this talk, we aim to shed light on the notion of knowledge needed by players in a coalition to coordinate against nature. As a multi-player variant of the basic construction of Reif, we propose a game representation that keeps track of the information acquired by a player during a play, and discuss conditions under which this representation is finite. On basis of this, we outline a semi-decision algorithm for deciding whether there exist distributed winning strategies in n-player safety games with imperfect information.

At 16:00 CFV talk: Properties of Visibly Pushdown Transducers

  • Speaker: Frédéric Servais, Université Libre de Bruxelles
  • Abstract: Visibly pushdown transducers (VPT) form a strict subclass of pushdown transducers (PT) that extends finite state transducers with a stack. Like visibly pushdown automata, the input symbols determine the stack operations. It has been shown that visibly pushdown languages form a robust subclass of context-free languages. Along the same line, we show that word transductions defined by VPT enjoy all desired properties, in contrast to PT. In particular, functionality is decidable in PTIME, k-valuedness is in NPTIME and equivalence of (non-deterministic) functional VPT is EXPTIME-Complete. Those problems are undecidable for PT. Output words of VPT are not necessarily well-nested. We identify a general subclass of VPT that produce well-nested words, which is closed by composition, and for which the type checking problem is decidable.

March 12th 2010 : Forum Building, Auditorium G

At 14:00 Invited talk: A Survey of Classical, Real-Time, and Time-Bounded Verification

  • Speaker: Joel Ouaknine, Oxford University.
  • Abstract:

    I will survey the classical, real-time, and time-bounded
    theories of verification, highlighting key differences and similarities
    among them, and giving an overview presentation of the solution to a
    longstanding open problem in the field.

    This is joint work with Alex Rabinovich and James Worrell.

At 16:00 CFV talk: Implicit Real Vector Automata

  • Speaker: Jean-François Degbomont, Institut Montefiore, Université de Liège
  • Abstract:

    This work addresses the efficient handling of non-convex real polyhedra, i.e., sets of real vectors satisfying arbitrary Boolean combinations of linear constraints. We develop a symbolic data structure for representing such sets, based on an implicit and concise encoding of a known structure, the Real Vector Automaton. The resulting formalism provides a canonical representation of non-convex polyhedra, is closed under Boolean operators, and admits an efficient decision procedure for testing the membership of a vector.

    This is joint work with Bernard Boigelot and Julien Brusten.

December 4th 2009 : NO Building, 5th Floor (Solvay Room)

At 14:00 Invited talk: Well Structured Transition Systems

  • Speaker: Alain Finkel, LSV - ENS Cachan
  • Abstract:

    The theory of Well Structured Transition Systems provides the
    good structure for computing a finite basis of the set of predecessors
    of the upward closure of a finite set of states. We address here the
    dual problem which is to compute a finite representation of the set of
    successors of the downward closure of a finite set of states (called the
    cover). This last problem is, a priori, more difficult because in
    general, the cover has no finite basis.
    It is possible to complete any well-ordered set to obtain a cpo in which
    every downward closed set has a finite representation.
    We then define the framework of Complete Well Structured Transition
    Systems and we propose a simple and a conceptual procedure for computing
    the covering set. This procedure terminates more
    often than the generalized Karp-Miller tree procedure when applied on
    extended Petri nets and lossy channel systems.

At 16:00 CFV talk: n/a

  • Speaker: Véronique Bruyère, UMons
  • Abstract: n/a

November 27th 2009 : NO Building, 8th Floor (Rotule Room)

At 14:00 Invited talk: Boundedness problems for finite automata

  • Speaker:  Christof Löding RWTH Aachen.
  • Abstract:

    We consider finite automata (on words or trees) that besides
    accepting or rejecting their input also compute a value for each
    accepted input. This value is determined by the use of counters in the
    automaton that can be incremented or reset to zero. The values of the
    counters do not influence the controlflow of the automaton, they are
    only used to determine the value of the run on the input.

    Such automata on finite words have been used by Kirsten (under the
    name of nested distance desert automata) to solve the (restricted)
    star-height problem: Given a regular language, what is the minimal
    number of nested stars in a regular expression defining the language?
    In this application, the value of a run is the maximal value reached
    by one of the counters during the run. The value of an input is the
    minimal value of one of the runs on the input.  The problem of
    star-height is reduced to the limitedness problem for these automata:
    Is the mapping computed by the automaton on its accepted inputs
    bounded? This problem is shown to be decidable using algebraic
    techniques.

    In recent work a general theory of such automata has been
    developed. The purpose of the talk is to give an introduction and an
    overview of this subject.

At 16:00 CFV talk: Faster Pseudo-Polynomial Algorithms for Mean-Payoff Games

  • Speaker: Raffaella Gentilini , ULB
  • Abstract:

    We consider two-player games played on a weighted graph with mean-payoff objectives. We present a new pseudo-polynomial algorithm for solving such games, improving the best known worst-case complexity for pseudo-polynomial mean-payoff algorithms. Our solution relies on a simple fixpoint iteration to solve the log-space equivalent problem of deciding the winner of energy games.


Follow these links to access the lists of seminars for:

Links to other seminars

Last update: Lun 1er février 2010