Dr. Roland Meyer

"Finite Representations for Reconfigurable Systems"

Zusammenfassung: 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 have well-structured transition systems, where properties can be decided on a finite prefix of the computation tree. For systems of bounded breadth, we show Turing completeness. Inspired by the decidability result, we aim at recovering a Petri net translation for systems of bounded depth. The approach is to 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.