Chers collègues,
Nous n'aurons pas de séminaire jeudi prochain (2008-07-31).
Jérôme,
========================================================================
La page du groupe de travail:
http://www.labri.fr/~leroux/seminaire/
========================================================================
| Date (YYYY-MM-DD) | Orateur/Animateur | Titre |
|---|---|---|
| 2008-06-12 | Jean-Francois Raskin (ULB, Brussels, Belgium) | Fixpoint-based Abstraction Refinement and an Application to the converability problem for Petri Nets |
automatic refinement by backward completion in Moore closed abstract domains. We study the properties of our algorithm and prove it to be more precise than the counterexample guided abstract refinement algorithm (CEGAR). Contrary to several works in the literature, our algorithm does not require the abstract domains to be partitions of the state space. We also show that our automatic refinement technique is compatible with so-called acceleration techniques. Then, we show how to develop, from this general algorithm, an abstract interpretation based analysis that reduces the dimensionality of state spaces that are explored during verification of Petri nets. The dimensionality is reduced by trying to gather places that may not be important for the property to establish. If the abstraction that is obtained is too coarse, an automatic refinement is performed and a more precise abstraction is obtained. The refinement is computed by taking into account information about the inconclusive analysis. The process is iterated until the property is proved to be true or false. | ||
| 2008-05-22 | Nathalie Bertrand (IRISA, Rennes, France) | On decision problems for Probabilistic Büchi Automata |
This is a joint work with Christel Baier and Marcus Groesser. | ||
| 2008-04-17 | Delphine Longuet (Centrum voor Wiskunde en Informatica (Netherlands)) | Test de systèmes dynamiques à partir de spécifications modales |
test est une méthode très largement utilisée pour assurer la qualité des systèmes informatiques. Lorsque l'implantation du système n'est pas connue, celui-ci peut être testé par rapport à une spécification formelle ou informelle. Utiliser une spécification formelle comme référence de correction du système permet de formaliser le processus de test et ainsi de faciliter son automatisation. On distingue classiquement deux approches du test à partir de spécifications formelles : les spécifications logiques sont utilisées pour tester les comportements fonctionnels d'un système, tandis que la dynamique est testée à l'aide de modèles à base d'états tels que les systèmes de transitions. On montrera dans cet exposé de quelle façon l'approche du test à partir de spécifications logiques, lorsqu'on considère des spécifications exprimées en logique modale, peut être utilisée pour tester des systèmes dynamiques. | ||
| 2008-04-10 | Tristan Le Gall (IRISA, Rennes, France) | Treillis abstraits et alphabets infinis |
Si les langages réguliers avec un alphabet fini sont bien connus, des problèmes de représentation et de manipulation surgissent quand l'alphabet est infini. J'introduirai la notion d'automates de treillis, qui sont semblables aux automates finis mais dont les transitions sont étiquetées par des éléments d'un treillis atomique infini. Je détaillerai les opérations de déterminisation et de minimisation sur ce type d'automate et j'expliquerai comment on peut définir un opérateur d'élargissement. Je présenterai aussi quelques résultats expérimentaux. En collaboration avec Bertrand Jeannet | ||
| 2008-03-27 | Grégoire Sutre (LaBRI, Bordeaux, France) | Accelerated Data-flow Analysis |
Joint work with Jérôme Leroux. | ||
| 2008-03-20 | Nicolas Caniart (LaBRI, Bordeaux, France) | Accelerating Interpolant-based Model-checking |
have been widely proved successful and efficient for reachability checking. Surprisingly, these two techniques have never been combined to strengthen each other. Intuitively, acceleration provides under- approximation of the reachability set by computing the exact effect of some control-flow cycles and combining them with other transitions. On the other hand, interpolation-based model-checking is refining an over-approximation of the reachable states based on spurious error-traces. In this talk we present a technique to combine acceleration with interpolation-based model-checking at the refinement stage. Our method, called “interpolant acceleration”, helps to refine the abstraction, ruling out not only a single spurious error-trace but a possibly infinite set of error-traces obtained by any unrolling of its cycles. Interpolant acceleration is also proved to strictly enlarge the set of transformations that can be usually handled by acceleration techniques. | ||
| 2008-03-13 | Patricia Bouyer (LSV, Cachan, France) | Probabilities in Timed Automata |
This is based on joint works with Christel Baier, Nathalie Bertrand, Thomas Brihaye, Nicolas Markey and Marcus Groesser. | ||
| 2008-03-06 | Helmut Seidl (Institut für Informatik (Garching Germany)) | On the Relationship between Interval Analysis and Mean Payoff Games |
for precise interval analysis based on strategy iteration. While practically observed run-times are quite decent, precise upper and lower complexity bounds have been unknown. In this talk, we clarify the relationship of precise interval analysis to mean-payoff games. In particular, we show that mean-payoff games are polynomially equivalent to a class of total-payoff games which in turn are equivalent to simple integer equations. Since the latter form a sub-class of interval equations, this means that proving precise interval analysis to be polynomial is at least as hard as proving mean-payoff games to be polynomial - which would solve a long-standing open problem in theoretical computer science. This work is an extension of joint work with Thomas Gawlitza and based on late night discussions with Marcin Jurdzinski and Uri Zwick at Dagstuhl. | ||
| 2008-02-14 | Hugo Gimbert (LaBRI, Bordeaux, France) | Jeux avec observation partielle |
les joueurs prennent leurs décisions sans connaître l'état exact du système, ils n'ont accès qu'à des signaux émis lors des changements d'état. Le calcul des valeurs et des stratégies optimales de ces jeux se révèle beaucoup plus ardu que dans le cas des jeux avec information parfaite: au cours de cet exposé, nous présenterons plusieurs résultat d'indécidabilité et de calculabilité, certains classiques, d'autres récents ou inédits. | ||
| 2008-02-07 | Andrey Rybalchenko (Max Planck Institute for Software Systems, Saarbrücken, Germany) | path invariants |
suitable abstraction of a program automatically. We propose a method for automated abstraction refinement which overcomes some limitations of current predicate discovery schemes. In current schemes, the cause of a false alarm is identified as an infeasible error path, and the abstraction is refined in order to remove that path. By contrast, we view the cause of a false alarm ---the spurious counterexample--- as a full-fledged program, namely, a fragment of the original program whose control-flow graph may contain loops and represent unbounded computations. There are two advantages to using such path programs as counterexamples for abstraction refinement. First, we can bring the whole machinery of program analysis to bear on path programs, which are typically small compared to the original program. Specifically, we use constraint-based invariant generation to automatically infer invariants of path programs ---so-called path invariants. Second, we use path invariants for abstraction refinement in order to remove not one infeasibility at a time, but at once all (possibly infinitely many) infeasible error computations that are represented by a path program. Unlike previous predicate discovery schemes, our method handles loops without unrolling them; it infers abstractions that involve universal quantification and naturally incorporates disjunctive reasoning. | ||
| 2008-01-24 | Bernard Boigelot (Institut Montefiore, Liege, Belgique) | A Generalization of Cobham's Theorem to Automata over Real Numbers |
This work studies the expressive power of finite-state automata recognizing sets of real numbers encoded positionally. Those automata can be used as data structures for representing the sets of values that have to be handled during state-space exploration of systems relying on integer and real variables, such as timed or hybrid automata. It is known that the sets that are definable in the first-order additive theory of real and integer variables ( R, Z, +, leq) can all be recognized by weak deterministic Büchi automata, regardless of the encoding base r geq 1. In this paper, we prove the reciprocal property, i.e., that a subset of R that is recognizable by weak deterministic automata in every base r geq 1 is necessarily definable in ( R, Z, +, leq ). This result generalizes to real numbers the well-known Cobham's theorem on the finite-state recognizability of sets of integers. Our proof gives interesting insight into the internal structure of automata recognizing sets of real numbers, which may lead to efficient data structures for handling these sets. | ||
| 2008-01-17 | Fares Chucri (LaBRI, Bordeaux, France) | CEGAR Model-Checking pour AltaRica |
Il présente l'avantage de produire une trace de tout comportement indésirable (décrit par une expression logique) du système. Mais cette méthode présente l'inconvénient d'exploser en mémoire (the state explosion problem). L'approche CEGAR (CounterExemple Guided Abstraction Refinement) permet de vérifier un système en utilisant une abstraction finie de ce dernier. Grâce à cette approche il est possible de vérifier des gros systèmes et des systèmes infinis. Une implémentation de la méthode CEGAR pour les modèles AltaRica à été rélisée dans Mec V, afin de comparer cette approche par rapport aux méthodes de vérifications exhaustives classiques. | ||
| 2007-12-13 | Jean-Louis Boulanger (UT Compiègne, France) | V and V dans le cadre des systèmes certifiables |
réalisation de système complexe ayant un impact sur la vie des personnes. De tel systèmes sont dit "critique" et "sûr de fonctionnement". Pour chaque domaine (ferroviaire, nucléaire, aéronautique, ...), il existe des référentiels définissant les processus a mettre en oeuvre. Dans certain cas, il existe parmis ces processus des activités obligatoires liées à la certification du système. Dans le cadre de cette présentation, nous rappelerons les exigences associées aux systèmes certifiables. Nous ferons le point de ce qui a été fait et nous montrerons les contraintes qui restent a prendre en compte et les évolutions en cours. Mot-clés : méthode formelle, SAET-METEOR, Système certifiable, système critique, UML, ... | ||
| 2007-11-29 | Thomas Gazagnaire (IRISA, Rennes, France) | _HMSC Causaux_ |
Dans cet exposé nous introduisons une extension des HMSC appelée HMSC causaux, qui ajoute aux HMSC classiques la possibilité de commuter sur chaque processus certains évènements. Cette extension permet de modéliser des langages de MSC non finiment engendrés et non existentiellement bornés. Nous introduisons ensuite deux sous-classes syntaxiques de cette extension, les HMSC causaux réguliers et les HMSC causaux globalement-coopératifs, qui étendent strictement les classes du même nom pour les HMSC. Nous montrons que pour la première de ces classes, la régularité du langage des entrelacement est assurée, et pour la seconde l'inclusion et la vacuité de l'intersection est décidable. | ||
| 2007-10-25 | Florian Horn (LIAFA, Paris) | Des Fruits Aléatoires sur l'Arbre de Zielonka |
pour la synthèse de contrôleurs en milieux ouvert, lorsque certaines actions peuvent être considérées comme aléatoires. Les jeux $omega$-réguliers, dont les parties sont de longueur infinie, peuvent ainsi représenter des systèmes réactifs qui doivent réagir correctement à un flux continuel d'évènements. Une ressource critique pour ce genre d'applications est la mémoire utilisée lors de l'implémentation effective du contrôleur. Pour chaque condition de Muller, on peut déduire de l'"arbre de Zielonka" la quantité de mémoire nécessaire et suffisante pour définir des stratégies gagnantes. Dans cet exposé, je montrerai comment l'utilisation de stratégies randomisées permet de gagner "presque sûrement" à moindre coût dans chaque arène. Dans ce contexte également, c'est à partir de l'étude de l'"arbre de Zielonka" que l'on définit une meilleure borne supérieure. De plus, pour chaque condition, il existe certaines arènes (de taille exponentielle) pour lesquelles des stratégies utilisant moins de mémoire sont presque sûrement perdantes. | ||
| 2007-10-11 | Holger Hermanns (Saarland University (Saarbruecken, Germany)) | The quest for quantifiable quality |
of system design. In the era of modern, power-aware, wireless and distributed systems, correctness guarantees for such systems must become _quantifiable_. Instead of guaranteeing that a system is performing the expected tasks, we are ultimately interested in guaranteeing that the system performs its task within a given _time_ bound and with (energy) _costs_ within a given limit. Or better: that the _probability_ thereof is above a given threshold. In this talk I paint the landscape of behavioural models for probability, time, and cost, and discuss foundational and practical aspects of model checking such systems. A more detailled look into our own work on continuous-time, concurrent Markov models concludes the presentation. | ||
| 2007-09-27 | Igor Walukiewicz (LaBRI, Bordeaux, France) | A lower bound on web-services composition |
problem for web services is to decide if a given web service can be constructed from a given set of web services; where the construction is understood as a simulation of the specification by a fully asynchronous product of the given services. We present an EXPTIME-lower bound for this problem, thus matching the known upper bound. Our result also applies to richer models of web services, such as the Roman model. | ||