Le séminaire MV a lieu salle 076 presque tous les jeudis à 11H30.
| Date | Orateur | Titre |
|---|
| jeudi 26 janvier 2012 | Peter Habermehl (LIAFA, Paris)
| Forest Automata for Verification of Heap Manipulation |
| We consider verification of programs manipulating
dynamic linked data structures such as various forms of singly and doubly-linked
lists or trees. We consider important properties for this kind of systems like
no null-pointer dereferences, absence of garbage, shape properties, etc. We
develop a verification method based on a novel use of tree automata to represent
heap configurations. A heap is split into several ``separated'' parts such that
each of them can be represented by a tree automaton. The automata can refer to
each other allowing the different parts of the heaps to mutually refer to their
boundaries. Moreover, we allow for a hierarchical representation of heaps by
allowing alphabets of the tree automata to contain other, nested tree automata.
Program instructions can be easily encoded as operations on our representation
structure. This allows verification of programs based on a symbolic state-space
exploration together with refinable abstraction within the so-called abstract
regular tree model checking. A motivation for the approach is to combine
advantages of automata-based approaches (higher generality and flexibility of
the abstraction) with some advantages of separation-logic-based approaches
(efficiency). We have implemented our approach and tested it successfully on
multiple non-trivial case studies.
(joint work with Lukas Holik, Adam Rogalewicz, Jiri Simacek and Tomas Vojnar) |
| jeudi 19 janvier 2012 | Lorenzo Clemente (LaBRI)
| Optimizing Buechi Automata Inclusion Checking with Subsumption Preorders |
| Inclusion checking is a central algorithmic problem in the theory of automata, with important applications, e.g., in formal methods.
The problem is PSPACE-complete, thus under standard complexity-theoretic assumptions no deterministic algorithm with worst case polynomial time can be expected.
We optimize the so-called Ramsey-based approach to inclusion checking.
In this approach, one explores a semigroup of exponential size for a counter-example to inclusion.
The exploration starts from a small set of generators, and all elements of the semigroup are progressively computed by composition.
On the way, a test operation is used to check for counter-examples.
The exploration stops if a counter-example is found; otherwise, all elements are generated.
Clearly, exhaustive exploration of the semigroup is in general infeasible, due to its exponential size.
We show how coarse simulation-based subsumption preorders between elements of the semigroup can be designed,
allowing one to prune away significant parts of the search space.
Subsumption allows us to solve inclusion checking for automata with thousand states, which was unthinkable before.
More details can be found on http://www.languageinclusion.org/. |
| jeudi 12 janvier 2012 | Ocan Sankur (LSV, ENS Cachan)
| Robustness and Implementability of Timed Automata |
| Timed automata are a well established model in real-time system design. They offer an automata-theoretic framework to design, verify and synthesize systems with timing constraints. The theory behind timed automata has been extensively studied and mature model-checking tools are available. However, this model makes unrealistic assumptions on the system, such as the perfect continuity of clocks and instantaneous reaction times, which are not preserved in implementation even in digital hardware with arbitrary finite precisions. While these assumptions are natural in the design phase, they must be validated before implementing the system.
In this talk, I will first outline recent results on robustness analysis of timed automata, that is, deciding/computing an upper bound on the imprecisions under which a given property holds. I will then concentrate on the implementability problem, by presenting algorithms that render timed automata implementable: given a timed automaton, the goal is to construct a new timed automaton whose behavior under imprecisions is equivalent to the behavior of the first automaton.
Based on joint works with Patricia Bouyer, Kim Larsen, Nicolas Markey, Claus Thrane.
|
| jeudi 08 décembre 2011 | André Arnold (LaBRI) ()
| Propriétés de séparation dans la hiérarchie du mu-calcul sur les arbres (3) |
| Description: Pour le premier exposé d'une petite série sur les hiérarchies de langages, nous accueillons André Arnold pour nous parler de séparation dans la hiérarchie du mu-calcul sur les arbres. Selon Kuratowski, une famille Gamma de parties d'un ensemble E a la propriété de séparation si pour toute paire disjointe A,B d'ensembles dans Gamma, il existe un ensemble C dans Gamma tel que E-C est aussi dans Gamma, et A inclus dans C, B inclus dans E-C. Nous nous intéressons à la propriété de séparation pour les classes Sigma_n et Pi_n des ensembles d'arbres définis par des automates à parité, dont on sait qu'elles forment une hiérarchie infinie. A ce jour, on sait que la classe Pi_2 a la propriété de séparation [Rabin 1970, Arnold and Niwinski 1990, Santocanale and Arnold 2005] et que la classe Sigma_2 ne l'a pas [Hummel and Michalewski and Niwinski 2009] Dans cet exposé il sera montré que les classes Sigma_n (n>2) n'ont pas non plus la propriété de séparation, et expliqué pourquoi le problème n'est pas encore résolu pour les classes Pi_n (n>2). Auparavant, le problème de la séparation dans la hiérarchie des omega-langages reconnus par des automates __déterministes__ à parité sera entièrement traité. |
| jeudi 01 décembre 2011 | André Arnold (LaBRI)
| Propriétés de séparation dans la hiérarchie du mu-calcul sur les arbres (2) |
|
| jeudi 24 novembre 2011 | André Arnold (LaBRI)
| Propriétés de séparation dans la hiérarchie du mu-calcul sur les arbres |
| Description:
Pour le premier exposé d'une petite série sur les hiérarchies de langages, nous accueillons André Arnold pour nous parler de séparation dans la hiérarchie du mu-calcul sur les arbres.
Selon Kuratowski, une famille Gamma de parties d'un ensemble E a la propriété de séparation si pour toute paire disjointe A,B d'ensembles dans Gamma, il existe un ensemble C dans Gamma tel que E-C est aussi dans Gamma, et A inclus dans C, B inclus dans E-C.
Nous nous intéressons à la propriété de séparation pour les classes Sigma_n et Pi_n des ensembles d'arbres définis par des automates à parité, dont on sait qu'elles forment une hiérarchie infinie.
A ce jour, on sait que la classe Pi_2 a la propriété de séparation [Rabin 1970, Arnold and Niwinski 1990, Santocanale and Arnold 2005] et que la classe Sigma_2 ne l'a pas [Hummel and Michalewski and Niwinski 2009]
Dans cet exposé il sera montré que les classes Sigma_n (n>2) n'ont pas non plus la propriété de séparation, et expliqué pourquoi le problème n'est pas encore résolu pour les classes Pi_n (n>2).
Auparavant, le problème de la séparation dans la hiérarchie des omega-langages reconnus par des automates __déterministes__ à parité sera entièrement traité.
|
| jeudi 17 novembre 2011 | Pierre-Alain Reynier (LIF (Marseille))
| Visibly Pushdown Transducers: Functionality, k-Valuedness and Streamability |
| Visibly pushdown transducers (VPTs) form a strict subclass of pushdown transducers (PTs) 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 VPTs enjoy strong properties, in contrast to PTs. In particular, functionality is decidable in PTIME, k-valuedness is in NPTIME and equivalence of (non-deterministic) functional VPTs is EXPTIME-C.
In a second part, we study the problem of evaluating in streaming (i.e. in a single left-to-right pass) the transduction realized by a functional VPT. A transduction is said to be height bounded memory (HBM) if it can be evaluated with a memory that depends only on the height of the input word (and not on its length). We show that it is decidable in coNTPTime whether such a transduction is HBM. In this case, the required amount of memory may depend exponentially on the height of the input word. We exhibit a sufficient, decidable condition for a VPT to be evaluated with a memory that depends quadratically on the height of the input word. This condition defines a class of transductions that strictly contains all determinizable VPTs.
This talk is based on the two following papers :
Properties of Visibly Pushdown Transducers. Emmanuel Filiot, Jean-François Raskin, Pierre-Alain Reynier Reynier, Frédéric Servais and Jean-Marc Talbot. In Proc. MFCS’10.
Streamability of Nested Word Transductions. Emmanuel Filiot, Olivier Gauwin, Pierre-Alain Reynier and Frédéric Servais. In Proc. FSTTCS’11. |
| jeudi 10 novembre 2011 | Xavier Blanc (LaBRI)
| Vpraxis et évolution d'application internet |
| Pratiquement toutes les applications s’exécutent aujourd’hui sur Internet,
quel que soit leur usage et quel que soit leur domaine. Une application qui
s’exécute sur internet fait partie d’un réel écosystème d’applications. Elle
utilise et propose des ressources (donnée et/ou traitement) qui forment
l’écosystème. Ces ressources, qui étaient il y a quelques années encore du
simple texte, des images ou des vidéos, sont aujourd’hui beaucoup plus
complexes, tels que des données sémantiques ou des services web par exemple.
Cette complexité croissante fait que le développement des applications
internet, et donc de l’écosystème, ne peut plus se faire par des équipes
bien structurées, maîtres des artefacts logiciels qu’elles produisent et
appliquant des cycles de développement traditionnels. Nous soutenons que le
développement d’application internet doit nécessairement prendre en
considération le concept d’écosystème logiciel. Les applications de demain
seront de plus en plus dépendantes de leur écosystème. Sans une forte
réactivité de développement face aux évolutions de l’écosystème, une
application deviendra vite dépassée et donc inutilisable ou extrêmement
couteuse en maintenance.
Le thème Sphere du LaBRI (http://sphere.labri.fr) développe l’approche
VPraxis qui vise à contrôler l’évolution des applications internet. Notre
objectif est de modéliser les histoires des différents composants des
applications internet afin de contrôler leur interdépendance. Cette
présentation portera sur VPraxis et montrera le modèle qu’il propose afin de
modéliser l’évolution d’un écosystème logiciel. |
| jeudi 03 novembre 2011 | Anca Muscholl (LaBRI)
| Controlling distributed systems |
| We consider the problem of controlling distributed automata that cooperate via
shared variables (rendez-vous). The setting corresponds to the framework of
Ramadge and Wonham, where certain actions (controllable ones) can be forbidden
by the local controller. Although the general question is still open, we
show that the problem is decidable on acyclic architectures, albeit of
non-elementary complexity.
Joint work with B. Genest, H. Gimbert and I. Walukiewicz. |
| jeudi 13 octobre 2011 | Benjamin Monmege (LSV, ENS Cachan)
| Weighted Expressions and Pebble Automata over Nested Words |
| We introduce a calculus over nested words (or equivalently, trees) to express quantitative properties of XML documents or recursive programs. Our weighted expressions borrow purely logical constructs from XPath, but they also involve rational arithmetic expressions. The latter allow us to perform computations in an arbitrary (commutative) semiring. For instance, one can count how often a given entry occurs in an XML document, or compute the memory consumption of a program execution. We characterize a fragment of weighted expressions in terms of a new class of weighted automata. In the spirit of tree-walking automata, our device traverses a nested word along its edges and may place pebbles during a traversal.
After proving this expressiveness result, we give a list of interesting decision or computation problems, with some hints on their resolution, and a set of possible applications of these problems, depending of the chosen semiring. |
| jeudi 06 octobre 2011 | Lukasz Kaiser (LIAFA, CNRS)
| Model Checking the Quantitative mu-Calculus on Infinite Transition Systems |
| We consider the model-checking problem for a quantitative
extension of the modal mu-calculus on two classes of infinite
quantitative transition systems. The first class, initialized linear
hybrid systems, is motivated by verification of systems which
exhibit continuous dynamics. We show that the value of a formula
of the quantitative mu-calculus can be approximated with arbitrary
precision on initialized linear hybrid systems. The other class,
increasing tree rewriting systems, is motivated by efforts to allow
counting formulas in discrete verification. On such systems, we
show that the value of a quantitative formula can be computed
exactly. For both these classes of systems, the problem in the end
reduces to solving a new form of parity games with counters. |
| jeudi 29 septembre 2011 | Barbara Jobstmann (Verimag)
| Quantitative Verification and Synthesis |
| Quantitative constraints have been successfully used to state and
analyze non-functional properties such as energy consumption,
performance, or reliability. Functional properties are typically
viewed in a purely qualitative sense. Desired properties are written
in temporal languages and the outcome of verification is a simple Yes
or No answer stating that a system satisfies or does not satisfy the
desired property. We believe that this black and white view is
insufficient both for verification and for synthesis. Instead, we
propose that specifications should have a quantitative aspect.
Our recent research shows that quantitative techniques give new
insights into qualitative specifications. For instance,
average-reward properties allow us to express properties like default
behavior or preference relations between implementations that all
satisfy the functional property. These additional properties are
particularly useful in a synthesis setting, where we aim to
automatically construct a system that satisfies the specification,
because they allow us to guide the synthesis process making the outcome
of synthesis more predictable.
In this talk I will give an overview of
(1) how classical specification can be augmented with quantitative constraints,
(2) list different quantitative constraints that arise in this way, and
(3) show how to verify and synthesize systems that satisfied the
initial specification and optimize such quantitative constraints.
This is joint work with R. Bloem, K. Chatterjee, K. Greimel, T. Henzinger,
A. Radhakrishna, R. Singh, and C. von Essen.
|
| jeudi 22 septembre 2011 | Marc Zeitoun (LaBRI)
| Model checking vector addition systems with one zero-test |
| We design a variation of the Karp-Miller algorithm to compute a
finite representation of the cover (i.e., the downward closure of
the reachability set) of a vector addition system with one
zero-test. This algorithm yields decision procedures for several
problems on these systems, open until now, such as
place-boundedness or LTL model-checking.
The proof techniques to handle the zero-test are based on two new
notions of cover: the refined and the filtered cover. The refined
cover is hybrid between the reachability set and the classical
cover. It inherits properties of the reachability set: equality
of two refined covers is undecidable, even for usual Vector
Addition Systems (with no zero-test), but the refined cover of a
Vector Addition System is a recursive set. The second notion of
cover, called the filtered cover, is the central tool of our
algorithms. It inherits properties of the classical cover, and in
particular, one can effectively compute a finite representation
of this set, even for Vector Addition Systems with one zero-test. |
| jeudi 30 juin 2011 | Amélie Stainer (INRIA Rennes)
| A game approach to determinize timed automata |
| Timed automata are frequently used to model real-time systems.
Their determinization is a key issue for several validation problems.
However, not all timed automata can be determinized, and determinizability
itself is undecidable. In this talk, we will present a game-based algorithm
which, given a timed automaton,
tries to produce a language-equivalent deterministic timed automaton,
otherwise a deterministic over-approximation. Our method subsumes two
recent contributions: it is at once more general than a recent determinization
procedure and more precise than the existing over-approximation algorithm.Then, we will explain how this method can be adapted to be usefull for test generation.
This talk is a joint work with Nathalie Bertrand, Thierry Jéron and Moez Krichen. Papers will be presented at FoSSaCs'11 and TACAS'11. |
| jeudi 23 juin 2011 | Gérald Point (LaBRI)
| Génération de séquences de pannes de modèles AltaRica |
| Les analyses de sûreté visent à réduire la probabilité
d'occurrence d'incidents critiques dans un système. Un des moyens
d'évaluer cette probabilité est de calculer les principales
combinaisons de pannes des composants du système qui engendrent
l'incident critique étudié. Cet ensemble de combinaisons permet
ensuite d'évaluer, éventuellement de manière pessimiste, la
probabilité de défaillance du système.
Lors de ce séminaire je présenterai comment nous avons utilisé de
vieilles recettes pour calculer l'ensemble des séquences critiques
d'un système modélisé en langage AltaRica.
Ces algorithmes sont désormais disponibles dans ARC, le model-checker
pour AltaRica.
La présentation sera en français.
|
| jeudi 09 juin 2011 | David Janin (LaBRI)
| Vers un modèle de contrôle temps-réels, hiérarchique, concurrent et réactifs |
| A priori, tout et dans le titre, les mots clés qui le composent et les questions qui en découlent. Quelles peuvent être les motivations pour définir de tels contrôleurs ? Comment ordonner les paradigmes (parfois transversaux) de modélisation qu'ils doivent inclure ? Que sait-on déjà de ce type de contrôleurs ? Comment le modèle qui s'impose peut-il être relié aux notions déjà existantes d'automates d'états finis, d'automates synchrones, d'automates à piles, de diagrammes d'états (statecharts), d'automates temps réels, de modèles de flux synchrones, etc....
Dans cet exposé, à travers la définition d'un modèle de contrôleurs qui tente d'intégrer tout les paradigmes évoqués, je tâcherais d'illustrer par l'exemple quelques éléments de réponses à ces questions en m'appuyant notamment sur la problématique de "la modélisation à visée applicative" qui agit comme un filtre à concepts selon le principe "si ça marche, ça doit avoir des propriétés mathématiques intéressantes".
|
| jeudi 19 mai 2011 | Rohit Chadha (LSV)
| Power of Randomization in Finite State Monitoring |
| We introduce the model of finite state probabilistic monitors (FPM), which are finite state automata on infinite strings that have probabilistic transitions and an absorbing reject state. FPMs are a natural automata model that can be seen as either randomized run-time monitoring algorithms or as models of open, probabilistic reactive systems that can fail. We give a number of results that characterize, topologically as well as with respect to their computational power, the sets of languages recognized by FPMs. We also study the emptiness and universality problems for such automata and give exact complexity bounds for these problems. Joint work with A. Prasad Sistla and Mahesh Viswanathan. |
| jeudi 12 mai 2011 | Renaud Tabary (LaBRI)
| Hybrid syntactic/semantic computer virus detection scheme |
| The detection problem in computer virology is known to be undecidable. Nonetheless, a large body of work is still devoted to the subject. We will present the state of the art on detection schemes: the syntactic and semantic detection schemes.
Subsequently, we will introduce a new hybrid syntactic/semantic detection scheme, where the extraction of the virus signature is performed through abstract interpretation techniques while virus detection is let to efficient syntactic detectors. We will present a new abstract domain that is able to automatically extract the signature of a polymorphic virus as a context free grammar. Preliminary results on some real polymorphic virus samples will also be shown. |
| jeudi 05 mai 2011 | Youssouf Oualhadj (LaBRI)
| Computing Optimal Strategies for Markov Decision Processes with Parity and Positive-Average Conditions |
| We study Markov decision processes (one-player stochastic games)
equipped with parity and positive-average conditions.
In these games, the goal of the player is to maximize the probability that both the
parity and the positive-average conditions are fulfilled.
We show that the values of these games are computable in polynomial time.
We also show that optimal strategies exist, require only finite memory and can be effectively computed.
Joint work with Hugo Gimbert and Soumya Paul. |
| jeudi 28 avril 2011 | Srivathsan Balaguru (LaBRI)
| A lazy reachability algorithm for timed automata |
| We consider the classic reachability problem for timed automata:
given an automaton, decide if there exists a path from its initial state
to a given target state. The standard solution to this problem involves
computing the *zone graph* of the automaton, which in principle could be
infinite. In order to make the graph finite, zones are approximated using
an extrapolation operator. For reasons of efficiency it is required that an
extrapolation of a zone is always a zone; and in particular that it is *convex*.
We propose a new solution to the reachability problem that uses no
such extrapolation operators. To ensure termination, we provide an
efficient algorithm to check if a zone is included in the
*region closure* of another. Although theoretically better,
closure cannot be used in the standard algorithm since a closure of
a zone may not be convex.
The structure of this new algorithm permits to calculate
approximating parameters on-the-fly during exploration of the zone
graph, as opposed to the current methods which do it by a static
analysis of the automaton prior to the exploration. This allows for
further improvements in the algorithm. Promising experimental results
are presented.
Joint work with Frédéric Herbreteau, Dileep Kini, Igor Walukiewicz
|
| jeudi 07 avril 2011 | Régis Gascon (INRIA Sophia Antipolis)
| Contraintes sur le temps logique dans la conception de systemes embarques |
| Je presenterai un langage de contrainte permettant d'exprimer des contraintes chronologiques et causales
sur les evenements du systeme (horloges logiques) et certains de mes travaux en cours sur ce langage: d'une
part la comparaison de ce langage avec la logique temporelle lineaire et d'autre part l'extension de ce langage
avec un systeme de priorites. |
| jeudi 17 février 2011 | Stefan Schwoon (LSV, Cachan)
| Unfoldings of contextual Petri nets |
| In a seminal paper, McMillan proposed a technique for constructing a finite complete prefix of the unfolding of bounded (i.e., finite-state) Petri nets, which can be used for verification purposes.
Contextual nets are a generalisation of Petri nets suited to model systems with read-only access to resources. When working with contextual nets, a finite complete prefix can be obtained by applying McMillan's construction to a suitable encoding of the contextual net into an ordinary net.
However, it has been observed that if the unfolding is itself a contextual net, then the complete prefix can be significantly smaller than the one obtained with the above technique. We propose a an unfolding algorithm that works for arbitrary semi-weighted, bounded contextual nets.
The talk is based on joint work with Paolo Baldan, Andrea Corradini, and Barbara Koenig. |
| jeudi 03 février 2011 | Mohamed Faouzi Atig (LIAFA, PARIS)
| Global Model Checking of Ordered Multi-Pushdown Systems |
| In this talk, we address the verification problem of ordered multi-pushdown systems, a multi-stack extension of pushdown systems that comes with a constraint on stack operations: a pop can only be performed on the first non-empty stack (which implies that we assume a linear ordering on the collection of stacks). First, we show that for an ordered multi-pushdown system the set of all predecessors of a regular set of configurations is an effectively constructible regular set. Then, we exploit this result to solve the global model checking which consists in computing the set of all configurations of an ordered multi-pushdown system that satisfy a given w-regular property (expressible in linear-time temporal logics or the linear-time µ-calculus). As an immediate consequence of this result, we obtain an 2ETIME upper bound for the model checking problem of w-regular properties for ordered multi-pushdown systems (matching its lower-bound).
|