Seminars for 2007-2008
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.
Past Seminars
May, 30th, Campus Plaine, Forum building, room OF2072
At 14:00 Invited talk: Probabilistic Buechi automata
- Speaker:
Christel
Baier
- Abstract:
Probabilistic finite automata as acceptors for
languages over finite words have been studied by
many researchers. In this talk, we discuss
probabilistic automata for recognizing languages
over infinite words. The idea is to resolve the
choices in a nondeterministic omega-automaton by
probabilities and to require positive probabilities
for the accepting runs. Surprisingly, probabilistic
Buechi automata are more expressive than
non-deterministic omega-automata. However, a
certain subclass of probabilistic Buechi automata
can be identified that has exactly the power of
omega-regular languages. Concerning the efficiency,
probabilistic omega-automata are not comparable with
their nondeterministic counterparts. There are
examples of omega-regular languages that have
probabilistic Buechi automata of polynomial size,
while any nondeterministic omega-automata with
Streett, Rabin or Buechi acceptance is of
exponential size.
The talk will introduce the formal notion of
probabilistic automata with Buechi and other
acceptance conditions and discuss some basic
properties, such as expressiveness, efficiency,
composition operations and decision problems.
At 16:00 CFV talk: Equivalence of Labelled Markov Chains
- Speaker: Jean-François Raskin (ULB)
- Abstract:
We consider the
equivalence problem for probabilistic machines. Two
probabilistic machines are equivalent if every finite
sequence of observations has the same probability of
occurrence in the two machines. We show that
deciding equivalence can be done in polynomial time
for labeled Markov chains, using a reduction to the
equivalence problem for probabilistic automata,
which is known to be solvable in polynomial time.
We provide an alternative algorithm to solve the
equivalence problem, which is based on a new
definition of bisimulation for probabilistic
machines. We also extend that technique to decide
equivalence of weighted probabilistic automata.
Then, we consider the equivalence problem for
labeled Markov decision processes (LMDPs) which asks
given two LMDPs whether for every way of resolving
the decisions in each of the processes, there exists
a way of resolving the decisions in the other
process such that the resulting probabilistic
machines are equivalent. The decidability of this
problem remains open. We show that the strategies
used to resolve the decisions can be restricted to
be observation-based, but may require infinite
memory. Keywords: Labeled Markov chain, Markov
decision process, probabilistic automaton,
equivalence, bisimulation.
Joint work with Tom Henzinger and Laurent Doyen
May, 9th, Campus Plaine, NO building, 5th floor, Solvay room
At 14:00 Invited talk: Unfolding Concurrent Well-Structured Transition Systems
At 16:00 CFV talk: On the Sets of Real Numbers Recognized by Finite Automata in Multiple Bases
- Speaker: Julien Brusten (ULg)
- Abstract:
This work studies the expressive power of finite automata recognizing
sets of real numbers encoded in positional notation. We consider
Muller automata as well as the restricted class of weak deterministic
automata, used as symbolic set representations in actual applications.
In previous work, it has been established that the sets of numbers that
are recognizable by weak deterministic automata in two bases that do
not share the same set of prime factors are exactly those that are
definable in the first order additive theory of real and integer
numbers (R, Z, +, <). This result extends Cobham's theorem, which
characterizes the sets of integer numbers that are recognizable by
finite automata in multiple bases.
In this work, we first generalize this result to multiplicatively
independent bases, which brings it closer to the original statement of
Cobham's theorem. Then, we study the sets of reals recognizable by
Muller automata in two bases. We show with a counterexample that, in
this setting, Cobham's theorem does not generalize to multiplicatively
independent bases. Finally, we prove that the sets of reals that are
recognizable by Muller automata in two bases that do not share the same
set of prime factors are exactly those definable in (R, Z, +, <). These
sets are thus also recognizable by weak deterministic automata. This
result leads to a precise characterization of the sets of real numbers
that are recognizable in multiple bases, and provides a theoretical
justification to the use of weak automata as symbolic representations
of sets.
Joint work with Bernard Boigelot and Véronique Bruyère.
March, 14th, Campus Plaine, NO building, Solvay room (5th floor)
At 14:00 Invited talk: Searchs in graphs for Verification
and Partial Order Reductions
- Speaker: Blaise Genest
- Abstract:
The problem of state
space search is one of the most basic building
blocks of various application, as verification.
Often, the state space is huge, so optimizing the
search is crucial. Some of the actions may commute,
i.e., they result in the same state for every order in
which they are taken. After recalling briefly the
basic search methods and their advantages, we will
review different techniques using the commutation
(Partial Order Reductions) to reduce the state space.
In particular, the state space can be reduced either
by deleting states (e.g. using persistent or ample
sets), or by deleting transitions (e.g. with the sleep
set method). We will present a new partial order
method reducing the number of transitions, shading a
new light on sleep set method. In particular, it
brings tangible benefits regarding the stack
size.
At 16:30
PhD Defense: Development and Validation of Distributed Reactive
Control Systems
- Speaker: Cédric Meuter
- Abstract:
A reactive control system is a computer
system reacting to certain stimuli emitted by its
environment in order to maintain it in a desired
state. Distributed reactive control systems are generally
composed of several processes, running in parallel on one
or more computers, com- municating with one another to
perform the required control task. By their very nature,
distributed reactive control systems are hard to
design. Their distributed nature and/or the communication
scheme used can introduce subtle unforeseen
behaviours. When dealing with critical applications, such
as plane control systems, or traffic light control
systems, those unintended behaviours can have disastrous
consequences. It is therefore essential, for the designer,
to ensure that this does not happen. For that purpose,
rigorous and systematic techniques can (and should) be
applied as early as possible in the development
process. In that spirit, this work aims at providing the
designer with the necessary tools in order to facilitate
the development and validation of such distributed
reactive control systems. In partic- ular, we show how
using a dedicated language called dSL (Distributed
Supervision language) can be used to ease the development
process. We also study how validations techniques such as
model-checking and testing can be applied in this context.
February, 15th, Campus Plaine, Forum building, Auditorium A
At 14:00 Invited talk: Computational Soundness of
Formal Security Protocol Analysis
- Speaker: Steve Kremer (CNRS, ENS
Cachan, France)
- Abstract:
Formal verification of security protocols in
so-called Dolev-Yao models has become common practice and recent tools
are able to analyze complex, real-life case studies such as SSL and
Kerberos. These methods have however been criticised because they make
strong hypotheses on the underlying cryptgraphic primitives (often
refered to as the perfect cryptography assumption).
In an influential paper, Abadi and Rogaway have shown that under
standard cryptographic assumptions the abstractions on cryptographic
primitives made in Dolev-Yao models are sound: formal security proofs
imply security proofs in a detailed, computational model where
adversaries are arbitrary probabilistic poly-time Turing Machines. In
this talk I will first present the seminal result by Abadi and Rogaway.
Then, I will present a general setting for reasoning about the soundness
of abstract models where cryptographic primitives are specified by the
means of equational theories. While the Abadi-Rogaway result only
considers encryption and pairing, we are able to show soundness results
for many more primitives including different encryption functions,
exclusive or and modular exponentiation.
This talk covers material from:
- [AR02] Martín Abadi and Phillip Rogaway. Reconciling Two Views of
Cryptography (The Computational Soundness of Formal Encryption). J.
Cryptology 15(2): 103-127, 2002.
- [BCK05] Mathieu Baudet, Véronique Cortier and Steve Kremer.
Computationally Sound Implementations of Equational Theories against
Passive Adversaries. In Proceedings of the 32nd International
Colloquium on Automata, Languages and Programming (ICALP'05), LNCS 3580,
Springer, 2005.
- [ABW06] Martín Abadi, Mathieu Baudet and Bogdan Warinschi. Guessing
Attacks and the Computational Soundness of Static Equivalence. In
Proceedings of the 9th International Conference on Foundations of
Software Science and Computation Structures (FoSSaCS'06), LNCS 3921,
Springer, 2006.
- [KM07] Steve Kremer and Laurent Mazaré. Adaptive Soundness of Static
Equivalence. In Proceedings of the 12th European Symposium on Research
in Computer Security (ESORICS'07), LNCS 4734, Springer, 2007.
At 16:00 CFV talk: Visibly Pushdown Transducers
- Speaker: Jean-François Raskin
- Abstract:
Visibly pushdown automata
have been recently introduced by Alur and Madhusudan as a
subclass of pushdown automata. This class enjoys nice
properties like closure under all boolean operations and the
decidability of language inclusion. In the same line, we
introduce here visibly pushdown transducers as a subclass of
pushdown transducers. We study properties of those
transducers and identify subclasses with nice properties
like decidability of type checking as well as preservation
of regularity of visibly pushdown languages.
Joint work with Frédéric Servais
Robust Analysis of Timed Automata
- Speaker: Nicolas Markey (LSV, Cachan, France)
- Date: October, 26th
- Place: Solvay room, NO building, 5th floor
- Abstract:
Whereas formal verification of timed systems has become a very active
field of research, the idealized mathematical semantics of timed automata
cannot be faithfully implemented on digital, finite-precision hardwares.
In particular, the properties proved on a timed automaton might not be
preserved in any of its implementations.
In this talk, I will present one way of dealing with this problem, through
an enlarged semantics of timed automata originally proposed in [DDR04]. I
will first explain how to check implementability w.r.t. safety properties
[DDMR04], and then extend this result to LTL properties [BMR06] and
finally to a large fragment of MTL [BMR08].
(based on joint works with Martin De Wulf, Laurent Doyen,
Jean-François Raskin, Patricia Bouyer and Pierre-Alain Reynier)
References:
- [DDR04] Martin De Wulf, Laurent Doyen and Jean-François Raskin. Almost
ASAP Semantics: From Timed Models to Timed Implementations. In
Proceedings of the 7th International Workshop on Hybrid Systems:
Computation and Control (HSCC'04), LNCS 2993. Springer-Verlag,
2004.
- [DDMR04] Martin De Wulf, Laurent Doyen, Nicolas Markey and Jean-François
Raskin. Robustness and Implementability of Timed Automata. In
Proceedings of the Joint International Conferences on Formal
Modelling and Analysis of Timed Systems, (FORMATS'04) and Formal
Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'04),
LNCS 3253. Springer-Verlag, 2004.
- [BMR06] Patricia Bouyer, Nicolas Markey and Pierre-Alain Reynier. Robust
Model-Checking of Linear-Time Properties in Timed Automata. In
Proceedings of the 7th Latin American Symposium on Theoretical
INformatics (LATIN'06), LNCS 3887, pages 238-249. Springer-Verlag,
2006.
- [BMR08] Patricia Bouyer, Nicolas Markey and Pierre-Alain Reynier. Robust
Analysis of Timed Automata. Submitted. 2008.
Automata and XML
-
Speaker: Frank
Neven (Universiteit Hasselt)
- Date: December, 7th
- Place: Solvay room, NO building, 5th floor
- Abstract:
The advent of XML imposes new and exciting
challenges on the field of theoretical computer
science. In this talk we present a tutorial style
introduction to XML schema languages and their
corresponding (unranked) tree and string automata
models. We discuss their expressive power, succinctness
and the complexity of their decision problems.
The talk covers material from:
-
Wouter Gelade, Frank Neven: Succinctness of
Pattern-Based Schema Languages for XML. DBPL 2007:
201-215
-
Wouter Gelade, Wim Martens, Frank Neven: Optimizing
Schema Languages for XML: Numerical Constraints and
Interleaving. ICDT 2007: 269-283
- Geert Jan Bex, Frank Neven, Thomas Schwentick, Karl
Tuyls: Inference of Concise DTDs from XML Data. VLDB
2006: 115-126
- Wim Martens, Frank Neven, Thomas Schwentick, Geert
Jan Bex: Expressiveness and complexity of XML
Schema. ACM Trans. Database Syst. 31(3): 770-813
(2006)
-
Wim Martens, Frank Neven, Thomas Schwentick:
Complexity of Decision Problems for Simple Regular
Expressions. MFCS 2004: 889-900
-
Wouter Gelade, Frank Neven: succinctness of the
complement and intersection of regular expressions.
Timed Concurrent Game Structures
-
Speaker: Thomas
Brihaye (LSV, Cachan)
- Date: December, 7th
- Place: Solvay room, NO building, 5th floor
- Abstract:
We propose a new model for timed games, based on
concurrent game structures. At each step of such a game,
each player chooses a delay and a move function. The
smallest chosen delay then elapses, and a transition is
fired according to the values of all the move functions at
that time.
Compared to the classical timed game automata of Asarin
et al. [AMPS98], our timed~CGSs are ``more concurrent'',
in the sense that they always allow all the agents to act
on the system, independently of the delay they want to
elapse before their action. Timed CGSs weaken the
``element of surprise'' of timed game automata reported by
de Alfaro et al. [AFHM+03].
We prove that our model has nice properties, in
particular that model-checking timed CGSs against timed
ATL is decidable via region abstraction, and in particular
that strategies (and move functions) are ``region-stable''
if winning objectives are. We also propose a new extension
of TATL, containing ATL*, which we call TALTL. We prove
that model-checking this logic remains decidable on timed
CGSs. Last, we explain how our algorithms can be adapted
in order to rule out Zeno (co-)strategies, based on the
ideas of de Alfaro et al. [AFHM+03,HP06].
Joint work with François Laroussinie, Nicolas Markey and
Ghassan Oreiby
Seminars from 2002
Follow these links to access the lists of seminars for: