Chers collègues,
Nous n'aurons pas de séminaire jeudi prochain (2007-07-26).
Jérôme,
========================================================================
La page du groupe de travail:
http://www.labri.fr/~leroux/seminaire/
========================================================================
Date (YYYY-MM-DD) | Orateur/Animateur | Titre |
---|---|---|
2007-06-28 | Thomas Brihaye (LSV, Cachan, France) | A probabilistic semantic for timed automata |
Il s'agit d'un travail en collaboration avec Christel Baier, Nathalie Bertrand, Patricia Bouyer et Marcus Größer | ||
2007-06-26 | Stéphane Demri (LSV, Cachan, France) | Logiques pour la Spécification et Vérification |
logiques pour la spécification et vérification. Ce sera l'occasion de rappeler la place des formalismes logiques en informatique avec un éclairage particulier pour la vérification formelle et l'interrogation de données. Parmi les sujets abordés plus en détail, on peut trouver les logiques temporelles avec mécanisme de mémoire et les contraintes de régularité dans les graphes. Plus de détails sont disponibles sur www.lsv.ens-cachan.fr/~demri/soutenance.php | ||
2007-06-21 | Nicolas Caniart (LaBRI, Bordeaux, France) | Accélération de l'algorithme Cegar |
abstraction refinement) connait un très vif succès au sein de la communauté de la vérification. Il a permis de vérifier des systèmes de taille conséquente et réaliste. Cependant, inhérent à sa nature de semi-algorithme, il existe encore de nombreux cas, parfois triviaux, dans lequel il se comporte mal, voir échoue. Dans cette exposé, on commencera par redéfinir Cegar et expliquer son fonctionnement. On mettra en suite en avant quelques exemples de systèmes (très simples) sur lesquels l'algorithme se comporte de fa- çon inappropriée. On proposera ensuite quelques solutions envisagées pour améliorer le comportement dans l'algorithme, au moyen de techni- ques d'accélération et d'interpolation. | ||
2007-06-07 | Patrick Chervet (LaBRI, Bordeaux, France) | Minimizing variants of visibly pushdown automata |
studied. Two subclasses of VPA are introduced: call driven automata, and block automata. For the first class, minimization results are presented unifying and generalizing those present in the literature. A drawback of this class, and all the other classes known till now, is that it is exponentially less succinct than VPA. The second class, block automata, is introduced to address this problem. These automata are as succinct as VPA. A minimization procedure for them is presented that requires one additional parameter to be fixed. An example of an exponential gain in succinctness is presented. | ||
2007-05-31 | Felix Klaedtke (ETH-Zentrum, Zurich, Switzerland) | Don't Care Words with an Application to the Automata-based Approach for Real Addition |
certain first-order theories of linear arithmetic, like the first-order theory over the reals with addition and the ordering. Reals are represented as infinite words, and the automata are recursively constructed from the formulas. This automata-based approach for representing and manipulating sets of reals has also applications in infinite-state model checking. However, analogous to BDDs to represent finite sets, the sizes of the automata are an obstacle in the automata-based set representation. In this talk, I will show how so-called "don't cares sets" for BDDs can be generalized to languages as a means to reduce the automata sizes and how "don't care words" can be used to build a more efficient automata-based decision procedure for real addition. A general result about don't care words is that the minimal weak deterministic B"uchi automaton with respect to a given don't care set with certain restrictions is uniquely determined and can be constructed efficiently. Our implementation LIRA uses don't care words and outperforms other state-of-the-art tools. | ||
2007-04-26 | Frédéric Herbreteau (LaBRI, Bordeaux, France) | Hybrid Acceleration |
2007-04-05 | Fabrice Chevalier (LSV, Cachan, France) | Décidabilité et contrôle de logiques temps-réel |
2007-03-22 | Nathalie Bertrand (Université de Dresden, Allemagne) | Vérification des Lossy Channel Systems probabilistes et non-déterministes. |
introduit pour représenter des protocoles de communication par file d'attentes imparfaites. Ce modèle a permis de vérifier des propriétés de sureté pour des protocoles de communication asynchrone concus pour pallier les pertes de messages. Néanmoins, il était trop pessimiste concernant les questions de vivacité, car il introduisait des comportements marginaux très peu probables (tels que l'exécution où tous les messages sont systématiquement perdus). Nous avons défini un modèle combinant probabilités et non-déterminisme pour les LCS, dénoté NPLCS. Ce modèle permet de représenter les pertes de messages comme des événements aléatoires, et les lectures ou écritures dans les canaux par des choix non-déterministes. Nous avons alors considéré le problème de la vérification qualitative, dont une instance est par exemple : " existe-t-il un comportement non-déterministe (appelé adversaire) pour lequel la probabilité de vérifier une formule est positive ?". On montre que la vérification qualitative est indécidable pour les NPLCS. Néanmoins, lorsqu'on considère la classe raisonnable des adversaires à mémoire finie, la vérification qualitative est décidable. Nous exposerons ces résultats (indécidabilité et décidabilité), en détaillant en particulier les ingrédients qui fournissent la décidabilité, à savoir : (1) l'existence d'un attracteur fini, et (2) un théorème de convergence du calcul itératif de certains points fixes. | ||
2007-03-15 | Axel Legay (Institut Montefiore, Liege, Belgique) | Sociable Interfaces: Theory, Implementation, and Future |
Since the last decades, various models have been introduce to model open systems. Among them one finds game-based models that represent the interaction between the behavior originating within a component, and the behavior originating from the component's environment as a game. In this talk, I will first recall the basic advantages of using a game-based model for the specification, verification, composition, and refinement of open systems. I will then introduce sociable interfaces, a recent concrete asynchronous game-based model where components have rich communication primitives that facilitate the modeling of software and distributed systems as well as global resources. The Sociable Interfaces model has been implemented in a tool called TICC. I will describe the main features of TICC, and explain the difficulties of moving from the theoretical description of the model to its implementation. Finally, I will discuss the possibility of adding time to the model. Joint work with Luca de Alfaro and Marco Faella. | ||
2007-03-08 | Pierre-Alain Reynier (LSV, Cachan, France) | Dépliages temporisés de réseaux d'automates temporisés |
2007-02-15 | Radu Iosif (VERIMAG, Grenoble, France) | Flat Parametric Counter Automata |
decidable fragments of integer arithmetic. We establish a hierarchy of flat counter automata, by restricting the number of parameters, the number of loops and the form of the transition relations. For each class in the hierarchy, we found a matching subtheory of integers, in the sense that, for each automaton in the class, the reachability (emptiness) problem can be expressed as the satisfiability of a formula in the language of a given theory, and viceversa. Using the same arithmetic theories allowed us to also establish the relation of flat counter automata with previous work on 2-way reversal bounded counter machines. Last, we report on an effective procedure to answer the question whether a given 1-parametric linear Diophantine system has a solution. | ||
2007-02-01 | Nicolas Markey (LSV, Cachan, France) | Verification of (One-clock) Priced Timed Automata |
extended with cost functions [ATP01,BFH+01]. The cost functions are just "observers", and cannot act upon the behavior of the automaton. We consider two classical problems: - computation of optimal cost and optimal winning strategies in PTGAs, - quantitative (w.r.t. costs) CTL model-checking in PTAs. We show that they are undecidable in general for priced timed automata, and prove that they are decidable when restricting to one-clock PTAs. | ||
2007-01-25 | Julien Bertrane (LIENS, Paris, France) | Certification de la résistance des réseaux de programmes synchrones aux erreurs matérielles |
synchrones communicants tenant compte des imperfections matérielles (désynchronisation des horloges, retards dans la transmission des données). Ces imperfections étant inévitables, les programmes incluent des techniques de robustesse qui permettent d'implémenter leur spécification malgré ces défauts. Cependant, ces techniques sont complexes, modifient fortement les programmes, et sont souvent ajoutées "à la main". Nous proposons donc une analyse statique (i.e. sur le code source et pas à l'exécution) et automatique, basée sur la théorie de l'interprétation abstraite, permettant de prouver formellement certaines de ces spécifications. | ||
2007-01-18 | Kaninda Musumbu (LaBRI, Bordeaux, France) | Graf and Saïdi97'algorithm : Construction of abstract state graph Revisited |
That requires - the construction of a model (STE) of execution of the system - a temporal logic - evaluation of the satisfaction of the property on the model. This method does not apply to the system having a infite number of states. It has nevertheless the advantage of being entirely automatizable. The abstraction is a technique of checking which consists in building a finite model for a system having an infinite number of states. That makes it possible to verify the properties wished on the abstract model by model-checking. The construction of an abstract model consists in defining an abstract domain and building a system of transition on this domain. Graf and Saïdi have proposed an automatic algorithm of connstruction of abstraction which requires many obligation of proof. The goal of the talk is to present a simplification of this construction. | ||
2007-01-11 | Laure Gonnord (VERIMAG, Grenoble, France) | Combining Widening and Acceleration in Linear Relation Analysis |
the most powerful, abstract interpretations working in an infinite lattice. As such, it makes use of a widening operator to enforce the convergence of fixpoint computations. While the approximation due to widening can be arbitrarily refined by delaying the application of widening, the analysis quickly becomes too expensive with the increase of delay. Previous attempts at improving the precision of widening are not completely satisfactory, since none of them is guaranteed to improve the precision of the result, and they can nevertheless increase the cost of the analysis. In this talk, we investigate an improvement of Linear Relation Analysis consisting in computing, when possible, the exact (abstract) effect of a loop. This technique is fully compatible with the use of widening, and whenever it applies, it improves both the precision and the performance of the analysis. | ||
2006-12-14 | Antoine Miné (LIENS, Paris, France) | L'analyseur statique Astrée |
2006-12-07 | Anca Muscholl (LaBRI, Bordeaux, France) | Logics and automata with infinite alphabets |
results on logics and automata with infinite alphabets. In this setting, we reason about data word and data tree languages, where we allow (in addition to usual regular operations) equality tests on the infinite alphabet component. At the beginning of the 90's, research on this topic focused on automata models à la Kaminski/Francez, and Neven/Schwentick/Vianu. However, the results obtained were mostly about undecidability and noncomparability of different automata models and of logics. Motivated by applications in XML data reasoning and in verification, recent work focused on exhibiting restricted decidable logics with data. Some examples are 1) two-variable FO logics with order and successor over finite and infinite data words, 2) two-variable FO logics with successor over data tree languages (Bojanczyk et al.) and 3) fragments of LTL with freeze operator (Demri/Lazic). | ||
2006-11-30 | The Quang Tran (LaBRI, Bordeaux, France) | Unfolding Concurrent Well-Structured Transition Systems |
------------------------------------------------------- In this work, our main objective is to combine partial-order methods with verification techniques for infinite-state systems in order to obtain efficient verification algorithms for concurrent infinite-state systems. This paper presents a general framework for partial-order modeling and verification of well-structured transition systems. Firstly, McMillan has proposed a technique in the verification of systems modelled with finite-state Petri nets [McM95]. This technique is based on the concept of net unfoldings and a well-known partial-order semantics of Petri nets. It construct only a finite complete prefix of the unfolding which contains full information about the reachable states. The unfolding technique has been later developed for other model of concurrency, e.g. Synchronous Products of Transition Systems [ER99], High-Level Petri Nets [KK03], Extended Finite State Machines [LI05]; and applied to other verification problems, e.g. checking relevant properties of speed independent circuits [KKTV95], simple branching time logic [Esp94]. Although the finite prefix obtained by unfolding technique avoids the interleaving explosion, it is sometimes much larger than necessary. Several works trying to resolve this problem can be classified into two types. The first one is to give a more adequate criteria in truncating the unfolding, e.g. based on a total order of trace [ER99], based on the symmetry of Petri Nets w.r.t some notions [CGP01]; and the second one is to avoiding the unuseful multiplication of a same labeled event when unfolding non-safe Petri nets [KKKV05]. In our work, we model concurrent systems as synchronized products of (heterogeneous) components, where the semantics of components is given in terms of event structures. This allows us to benefit from the intrinsic concurrency in each component. We propose event structures for counters and queues, and we present an on-the-fly compositional unfolding algorithm that computes event structures for synchronized products. For the particular case of well-structured components, we give property-preserving truncation criteria [FS01] on event structures in order to obtain effective decision algorithms for the boundedness, termination and quasi-liveness problems. Moreover, our technique for avoiding redundancy in the unfolding can also resolving the irrelevant multiplication problem stated in [KKKV05]. We have implemented a tool, called ESU, for demonstrating the benefits of our approach. [CGP01] Jean-Michel Couvreur, Sébastien Grivet, and Denis Poitrenaud. Unfolding of products of symmetrical petri nets. In ICATPN, pages 121-143, 2001. [ER99] J. Esparza and S. Römer. An unfolding algorithm for synchronous products of transition systems. In International Conference on Con- currency Theory, volume 1664 of Lecture Notes in Computer Sci- ence, pages 2-20, 1999. [Esp94] Javier Esparza. Model checking using net unfoldings. Sci. Comput. Program., 23(2-3):151-195, 1994. [FS01]Alain Finkel, Ph. Schnoebelen: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1-2): 63-92 (2001) [KK03] Victor Khomenko and Maciej Koutny. Branching processes of highlevel petri nets. In TACAS, pages 458-472, 2003. [KKKV05] Victor Khomenko, Alex Kondratyev, Maciej Koutny, and Walter Vogler. Merged processes - a new condensed representation of petri net behaviour. In CONCUR, pages 338-352, 2005. [KKTV94] Michael Kishinevsky, Alex Kondratyev, Alexander Taubin, and Victor Varshavsky. Analysis and identification of speed-independent circuits on an event model. Formal Methods in System Design, 4(1):33-75, 1994. [LI05] Yu Lei and S. Purushothaman Iyer. An approach to unfolding asynchronous communication protocols. In FM, pages 334-349, 2005. [McM95]Kenneth L. McMillan. A Technique of State Space Search Based on Unfolding. Formal Methods in System Design 6(1): 45-65 (1995). | ||
2006-11-16 | Philippe Darondeau (IRISA, Rennes, France) | Implementations distribuees du controle superviseur a la Ramadge et Wonham par synthese de reseaux de Petri |
permet, pour divers types de problemes de controle poses en termes de langages reguliers, de decider si ces problemes sont faisables, et de construire alors des automates finis realisant le controle. Diverses extensions de la theorie portent sur le controle des systemes decentralises mais le controle des systemes asynchrones et distribues reste un probleme ouvert. Nous montrons comment integrer la synthese de reseaux de Petri et la theorie de Ramadge-Wonham afin d'avoir une reponse partielle a ce probleme. | ||
2006-11-09 | Joel Ouaknine (Oxford University Computing Laboratory, Oxford, England) | The Cost of Punctuality |
An obvious question to ask is, what happens if punctuality is allowed? Until recently, it was widely believed that the faintest presence of punctuality in any linear-time timed temporal logic would automatically lead to undecidability. Although this was recently disproved, until now no decidable punctual fragment of MTL was known to have even primitive recursive complexity (with certain fragments having provably non-primitive recursive complexity!). Very recently, in joint work with Patricia Bouyer, Nicolas Markey, and James Worrell, we have been able to precisely pinpoint the complexity of the main decidable punctual fragments of MTL. Our complexity bounds involve a connection between MTL formulas and reversal-bounded Turing machines. We will present an overview of these results and how they relate to standard (untimed) verification. | ||
2006-10-19 | Morgan Magnin (IRCCYN, Nantes, France) | Réseaux de Petri à Chronométre - temps dense ou temps discret ? |
Deux approches peuvent alors être considérées. La première consiste à considérer le temps comme une grandeur continue (c'est-à-dire que le système peut changer d'état à n'importe quel moment), la seconde à l'envisager comme une grandeur discrète (la progression du temps est assurée par l'occurrence de tics d'horloge et le système ne peut alors évoluer qu'à des instants précis). Notre objectif durant cette thèse est de comparer ces deux approches : nous souhaitons dégager les spécificités de chacune et déterminer les différentes propriétés qu'elles permettent de vérifier. Ces recherches théoriques s'accompagnent d'un volet pratique. En effet, nous implantons nos résultats dans Roméo, un logiciel d'analyse de systèmes embarqués, et assurons ainsi leur valorisation auprès du tissu industriel. | ||
2006-10-12 | Blaise Genest (IRISA, Rennes, France) | On Zielonka's Theorem and its Application to Verification |
2006-10-05 | Igor Walukiewicz (LaBRI, Bordeaux, France) | Réunion de rentrée du thème Modélisation Vérification |