LSV Seminar

Date

Tuesday, November 24 2009 at 11:00AM

Place

Salle de Conférence (Pavillon des Jardins)

Speaker

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.