LSV Seminar

The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.

The seminar is open to public and does not require any form of registration.

Past Seminars

Finite Representations for Reconfigurable Systems

 Roland Meyer
Tuesday, November 24 2009 at 11:00AM
Salle de Conférence (Pavillon des Jardins)
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.

About LSV