BEGIN:VCALENDAR
VERSION:2.0
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
SUMMARY:
Finite Representations for Reconfigurable Systems
STATUS:CONFIRMED
ATTENDEE;CN="Roland Meyer
":
MAILTO:no@spam.com
DESCRIPTION:
To bridge the gap to existing automated verification techniq
ues\, we present finite representations for reconfigurable s
ystems (RS). Despite an unbounded number of components and c
onnections\, a large class of RS exhibits only finitely many
connection patterns at runtime; a property called structura
l stationarity. We propose a translation of structurally sta
tionary systems into finite place/transition Petri nets\, wh
ich 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 b
readth. The breadth of a RS corresponds to the connection de
gree of the components\, while the depth measures their inte
rdependence. Investigating these larger classes\, we find th
at systems of bounded depth are well-structured. Therefore\,
properties can be decided on a finite prefix of the computa
tion tree. For systems of bounded breadth\, we show Turing c
ompleteness. To recover a Petri net translation for systems
of bounded depth\, we combine the newly developed structural
semantics with classical concurrency semantics. Although th
e resulting mixed translation generalises the previous appro
aches\, it does not cover the full class of depth bounded sy
stems. An undecidability proof for reachability shows that a
translation into finite nets does not exist for the full cl
ass.
DTSTART;TZID=Europe/Paris:20091124T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200911241
100
UID:LSVsemLSV.200911241100@lsv.ens-cachan.fr
LOCATION:Salle de ConfĂ©rence (Pavillon des Jardins)
END:VEVENT
END:VCALENDAR