Le séminaire du LSV

Le séminaire du LSV a lieu le mardi à 11h00. Le lieu habituel est la salle de conférences au Pavillon des Jardins (plan d'accès). Pour être informé par email des prochains séminaires, contacter Stéphane Le Roux and Matthias Fuegger.

Le séminaire du LSV est public et ne nécessite aucune inscription préalable.

Séminaires passés

Finite Representations for Reconfigurable Systems

Visiter le site web pour cet événement | Exporter cet événement au format iCalendar

 Roland Meyer
Date
Le mardi 24 novembre 2009 à 11:00
Lieu
Salle de Conférence (Pavillon des Jardins)
Orateur
Roland Meyer (LIAFA, CNRS, Université Paris Diderot - Paris 7)

To bridge the gap to existing automated verification techniques, we present finite representations for reconfigurable systems (RS). Despite an unbounded number of components and connections, a large class of RS exhibits only finitely many connection patterns at runtime; a property called structural stationarity. We propose a translation of structurally stationary systems into finite place/transition Petri nets, which allows us to reuse existing Petri net verification tools for the verification of RS.

To judge the expressiveness of the system class, we prove that structural stationarity is equivalent to boundedness in the novel functions depth and breadth. The breadth of a RS corresponds to the connection degree of the components, while the depth measures their interdependence. Investigating these larger classes, we find that systems of bounded depth are well-structured. Therefore, properties can be decided on a finite prefix of the computation tree. For systems of bounded breadth, we show Turing completeness.

To recover a Petri net translation for systems of bounded depth, we combine the newly developed structural semantics with classical concurrency semantics. Although the resulting mixed translation generalises the previous approaches, it does not cover the full class of depth bounded systems. An undecidability proof for reachability shows that a translation into finite nets does not exist for the full class.


À propos du LSV

Agenda des séminaires

Exporter l'agenda au format iCalendar | Les séminaires précédents

mar. 19 février

Les séminaires précédents