Le séminaire MV a lieu salle 076 presque tous les jeudis à 11H30.
| Date | Orateur | Titre |
|---|
| jeudi 10 mai 2012 | Madhavan 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 2012 | Michael 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 2012 | Aiswarya 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 2012 | Ré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 2012 | Uli 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 2012 | Emmanuel 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 2012 | Benoî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 2012 | Gabriele 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 2012 | Lorenzo 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 2012 | Cezara 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 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. |