Groupe de travail Modélisation et Vérification

Le séminaire MV a lieu salle 076 presque tous les jeudis à 11H30.

Pour proposer un séminaire, le calendrier vous aidera à choisir une date disponible.

Pour s'abonner ou se désabonner de la liste de diffusion.


Prochains exposés

DateOrateurTitre
jeudi 09 février 2012Cezara Dragoi (IST Austria )
jeudi 16 février 2012David Baelde (?) ()



Précédents exposés depuis un an

DateOrateurTitre
jeudi 26 janvier 2012Peter 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 2012Lorenzo 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 2012Ocan 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 2011André 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 2011André Arnold (LaBRI) Propriétés de séparation dans la hiérarchie du mu-calcul sur les arbres (2)
jeudi 24 novembre 2011André 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 2011Pierre-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 2011Xavier 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 2011Anca 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 2011Benjamin 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 2011Lukasz 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 2011Barbara 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 2011Marc 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 2011Amé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 2011Gé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 2011David 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 2011Rohit 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 2011Renaud 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 2011Youssouf 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 2011Srivathsan 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 2011Ré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 2011Stefan 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 2011Mohamed 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).



Archives des années précédentes




Responsables



Hugo Gimbert

Jérôme Leroux

Srivathsan Balaguru

first.LAST@labri.fr