BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//labri.fr//NONSGML kigkonsult.se iCalcreator 2.41.92//
CALSCALE:GREGORIAN
METHOD:PUBLISH
UID:e5b6bbb1-638f-4686-899a-c7f50559c599
X-WR-CALNAME:[MTV] Chana Weil-Kennedy (IMDEA) - Observation Petri Nets
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
TZUNTIL:20250330T010000Z
BEGIN:STANDARD
TZNAME:CET
DTSTART:20221030T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RDATE:20231029T030000
RDATE:20241027T030000
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20230326T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RDATE:20240331T020000
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:e5b6bbb1-638f-4686-899a-c7f50559c599
DTSTAMP:20260517T180202Z
CLASS:PUBLIC
DESCRIPTION:This talk presents the work I did during my thesis\, which I co
 mpleted in March. Petri nets are a classic formal model for concurrent sys
 tems\, extensively studied and used since the 1970s. They model fundamenta
 l features of concurrent systems such as choice\, communication\, and proc
 ess creation. Many subclasses of Petri nets have been defined by forbiddin
 g one or more of these features (e.g. marked graphs\, free-choice nets\, c
 ommunication-free nets). In our work\, we introduce a feature of Petri net
 s called observation\, which is a restricted form of communication. We giv
 e a syntactic definition of a class of Petri nets in which the only possib
 le form of synchronization is observation. We study the complexity of anal
 ysis problems for this class\, called observation Petri nets\, and in part
 icular we consider verification problems parameterized by the number of to
 kens (or processes) in the Petri net. The main analysis problems we study 
 are the class of generalized reachability problems. This class extends rea
 chability queries to possibly infinite sets of markings (or configurations
 ). It includes the cube-reachability problem\, which given two sets asks i
 f there is a marking in the first set which can reach a marking in the sec
 ond set. We show that this class of problems can be decided in polynomial 
 space for observation Petri nets. The classic reachability problem asking 
 if a marking can reach another is also in polynomial space for our observa
 tion Petri nets (versus non primitive recursive for general Petri nets). S
 o our results show that it is not harder to check reachability between sin
 gle markings than it is to check reachability between possibly infinite se
 ts of markings. Thus the observation feature captures a non-trivial proper
 ty of Petri nets that is particularly interesting for parameterized verifi
 cation.
DTSTART;TZID=Europe/Paris:20230525T130000
DTEND;TZID=Europe/Paris:20230525T140000
LOCATION:salle 178\, zoom: https://bordeaux-inp-fr.zoom.us/j/89508306159
SEQUENCE:0
SUMMARY:[MTV] Chana Weil-Kennedy (IMDEA) - Observation Petri Nets
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR
