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.
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
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.