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 24 mai 2012Pierre Bourhis ()
jeudi 07 juin 2012M Praveen (LSV)
jeudi 21 juin 2012Michael Monerau (ENS, Ecole des mines, Paris)



Précédents exposés depuis un an

DateOrateurTitre
jeudi 10 mai 2012Madhavan Mukund (CMI, India) Tagging Make Local Testing of Message-Passing Systems Feasible
The only practical way to test distributed message-passing systems is to use local testing. In this approach, used in formalisms such as concurrent TTCN-3, some components are replaced by test processes. Local testing consists of monitoring the interactions between these test processes and the rest of the system and comparing these observations with the specification, typically described in terms of message sequence charts. The main difficulty with this approach is that local observations can combine in unexpected ways to define implied scenarios not present in the original specification. Checking for implied scenarios is known to be undecidable for regular specifications, even if observations are made for all but one process at a time. We propose an approach where we append tags to the messages generated by the system under test. Our tags are generated in a uniform manner, without referring to or influencing the internal details of the underlying system. These enriched behaviours are then compared against a tagged version of the specification. Our main result is that detecting implied scenarios becomes decidable in the presence of tagging. This is joint work with Puneet Bhateja.
jeudi 03 mai 2012Michael Emmi (LIAFA, Paris) Bounded Phase Analysis of Message-Passing Programs
We describe a novel technique for bounded analysis of asynchronous message-passing programs with ordered message queues. Our bounding parameter does not limit the number of pending messages, nor the number of “contexts-switches” between processes. Instead, we limit the number of process communication cycles, in which an unbounded number of messages are sent to an unbounded number of processes across an unbounded number of contexts. We show that remarkably, despite the potential for such vast exploration, our bounding scheme gives rise to a simple and efficient program analysis by reduction to sequential programs. As our reduction avoids explicitly representing message queues, our analysis scales irrespectively of queue content and variation.
jeudi 12 avril 2012Aiswarya Cyriac (LSV, ENS Cachan) Model Checking Languages of Data Words
We consider the model-checking problem for data multi- pushdown automata (DMPA). DMPA generate data words, i.e, strings enriched with values from an infinite domain. The latter can be used to represent an unbounded number of process identifiers so that DMPA are suitable to model concurrent programs with dynamic process creation. To specify properties of data words, we use monadic second-order (MSO) logic, which comes with a predicate to test two word positions for data equality. While satisfiability for MSO logic is undecidable (even for weaker fragments such as first-order logic), our main result states that one can decide if all words generated by a DMPA satisfy a given formula from the full MSO logic. This is a joint work with Benedikt Bollig, Paul Gastin and K. Narayan Kumar.
jeudi 05 avril 2012Rémi Bonnet (LSV) Forward Analysis for WSTS : Beyond Regular Accelerations
The well-known Karp and Miller algorithm constructs the coverability tree of a Vector Addition System, obtaining a finite representation of the cover (the downward closure of the reachability set). The series "Forward analysis in WSTS" aims to generalize this procedure for arbitrary well-ordered state spaces. I'll first recall the earlier works by Finkel and Goubbault-Larrecq, that introduced the notion of complete WSTS, in which a finite representation of the cover as set of maximal elements exists. Then, i'll present our formalization of acceleration strategy and a parameterized Karp Miller procedure that relies on these strategy in order to compute this set of maximal elements. As an illustration of these ideas, I'll present an acceleration strategy for Vector Addition Systems with two resets that allows the previously defined procedure to terminate, effectively computing the finite representation of the cover. This is joint work with Alain Finkel.
jeudi 29 mars 2012Uli Fahrenberg (IRISA, Rennes) The Quantitative Linear-Time–Branching-Time Spectrum
We present a distance-agnostic approach to quantitative verification. Taking as input an unspecified distance on system traces, or executions, we develop a game-based framework which allows us to define a spectrum of different interesting system distances corresponding to the given trace distance. Thus we extend the classic linear-time–branching-time spectrum to a quantitative setting, parametrized by trace distance. We also provide fixed-point characterizations of all system distances, and we prove a general transfer principle which allows us to transfer counterexamples from the qualitative to the quantitative setting, showing that all system distances are mutually topologically inequivalent.
jeudi 22 mars 2012Emmanuel Filiot (ULB) Exploiting Structure in LTL Synthesis
The aim of program synthesis is to automatically generate a program that satisfies a given specification, in contrast to program verification, for which both the specification and the program are given as input. The underlying goal is to improve program reliability and optimize design constraints, like time and human errors, and to get rid of the low-level programming tasks, by replacing them with the design of high-level specifications. The old dream of automatic synthesis, which among others was shared by Church, is difficult to realize for general-purpose programming languages. However in recent years, there has been a renewed interest in feasible methods for the synthesis of application specific programs, which have been, for instance, applied to reactive systems, distributed systems, programs manipulating arithmetic or concurrent data-structures. Reactive systems are non-terminating programs that continuously interact with their environment. They arise both as hardware and software, and are usually part of safety-critical systems, for example microprocessors, air traffic controllers, programs to monitor medical devices, or nuclear plants. It is therefore crucial to guarantee their correctness. The temporal logic LTL is a very important abstract formalism to describe properties of reactive systems. As shown by Pnueli and Rosner in 89, the synthesis of reactive systems from LTL specifications is a 2-Exptime complete problem. In this talk, I will present recent progresses in LTL synthesis based on a bounded synthesis approach inspired by bounded model-checking, and show that the high worst-case time complexity of LTL synthesis does not handicap its practical feasibility. This is achieved by exploiting the structure underlying the automata constructions used to solve the synthesis problem
jeudi 15 mars 2012Benoît Delahaye () Compositional Specification Theories for Stochastic Systems
Markov Chains (MCs) and Probabilistic Automata (PAs) are widely-recognized mathematical frameworks for the specification and analysis of systems with non-deterministic and/or stochastic behaviors. Notions of specification, implementation, satisfaction, and refinement, together with operators supporting stepwise design, constitute a specification theory. In the early 1990's, an abstraction of Markov Chains, called Interval Markov Chains (IMCs) has been proposed as a specification theory. This talk shows why IMCs are not perfectly suited to play their role as a specification theory and instead introduces a new, more permissive, abstraction called Constraint Markov Chains (CMCs). We introduce all the operators that make CMCs a complete specification theory and discuss computability and complexity. We then show how to extend CMCs by mixing them with Modal Transition Systems in order to propose a specification theory for Probabilistic Automata.
jeudi 08 mars 2012Gabriele Puppis (LaBRI) The Cost of Repairing Regular Specifications
What do you do if a computational object (e.g., a document, a program trace) fails a specification? An obvious approach is to perform a "repair": modify the object minimally to get something that satisfies the constraints. This approach has been extensively investigated in the database community for relational integrity constraints, and in the AI community for propositional logics. Different modification operators have been considered on the basis of the application scenarios. For instance, a repair of an XML document usually consists of applying to the underlying tree structure a certain number of editing operations such as relabelings, deletions, and insertions of nodes. In this talk I will survey some results related to the worst-case cost of repairing documents between regular specifications. Precisely, I will focus on the number of edits that are needed to get from a document (i.e., a word or a tree) that satisfies a source specification (i.e., a regular language S) to some document that satisfies a target specification (i.e., a regular language T). As this number may well be unbounded, I will consider the problem of determining those pairs of languages (S,T) such that one can get from any word/tree in S to a word/tree in T using a finite, uniformly bounded number of editing operations. I will give effective characterizations of these pairs when S and T are given by finite state automata (word case) or stepwise tree automata (tree case), and derive some complexity bounds for the corresponding problems. The presentation is based on joint works with Michael Benedikt, Cristian Riveros, and Sławek Staworko.
jeudi 16 février 2012Lorenzo Clemente (LaBRI) Fixed-word simulations and ranks
Minimization of Buchi automata is an intriguing topic in automata theory, both for a theoretical understanding of automata over infinite words, and for practical applications. Ideally, for a given language, one would like to find an automaton recognizing it with the least number of states. Since exact minimization is computationally hard (e.g., PSPACE-complete), we concentrate on quotienting, which is a state-space reduction technique which works by "glueing together" certain states. Which states can be merged is dictated by suitable preorders: In this talk, we study fixed-word simulations, which are simulation-like preorders sound for quotienting. We show that fixed-word simulations are coarser than previously studied simulation-like preorders, by characterizing it with a natural (but non-trivial) ranking argument. Our ranking construction is related to the so-called Kupferman-Vardi construction for complementing Buechi automata.
mercredi 15 février 2012 ()
jeudi 09 février 2012Cezara Dragoi (IST Austria ) Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data
We introduce a framework based on abstract interpretation for reasoning about programs with lists carrying integer numerical data. In this framework, abstract domains are used to describe and manipulate complex constraints on configurations of these programs mixing constraints on the shape of the heap, sizes of the lists, and on the data stored in the lists. We consider a domain where data is described by formulas in a universally quantified fragment of the first-order logic over sequences, as well as a domain where data is described using constrains on the multisets of data in the lists. Moreover, we provide powerful techniques for automatic validation of Hoare-triples and invariant checking, as well as for automatic synthesis of invariants and procedure summaries using modular inter-procedural analysis. The approach has been implemented in a tool called CELIA and experimented successfully on a large benchmark of programs.
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.



Archives des années précédentes




Responsables



Hugo Gimbert

Jérôme Leroux

Srivathsan Balaguru

first.LAST@labri.fr