Séminaires
Séminaire du 10 Octobre 2008
Lieu
LACL, la salle des thèses, bâtiment P2, niveau dalle: comment y aller
Programme
14h00-15h00: Hanna Klaudel, IBISC, Université d'Evry-val-d'Essonne, Towards Efficient Verification of Systems with Dynamic Process Creation
Abstract: Modelling and analysis of dynamic multi-threaded state systems often encounters obstacles when one wants to use automated verification methods, such as model checking. Our aim in this paper is to develop a technical device for coping with one such obstacle, namely that caused by dynamic process creation.
We first introduce a general class of coloured Petri nets-not tied to any particular syntax or approach-allowing one to capture systems with dynamic (and concurrent) process creation as well as capable of manipulating data. Following this, we introduce the central notion of our method which is a marking equivalence that can be efficiently computed and then used, for instance, to aggregate markings in a reachability graph. In some situations, such an aggregation may produce a finite representation of an infinite state system which still allows one to establish the relevant behavioural properties. We show feasibility of the method on an example and provide initial experimental results.
15h00-15h30 : Florent Bouchy, LSV - ENS de Cachan, Reachability in Timed Counter Systems
Abstract: Nous définissons un nouveau modèle de systèmes infinis, combinant les systèmes à compteurs et les automates temporisés. L'accessibilité est généralement indécidable dans ces systèmes, à cause des compteurs. Pour les analyser, nous abstrayons le côté temporisé (i.e. les valuations d'horloges) par un graphe de régions classique. Nous montrons ensuite qu'une version "détemporisée" du problème d'accessibilité est décidable pour trois sous-classes de nos Timed Counter Systems.