Date/Time
Date(s) - 31/05/2013
3:00 pm - 4:00 pm
Location
SHSC Conference & Training Centre, Edinburgh
I will talk about two algebras of Petri Nets: one of C/E nets (where there is at most one token on each place) and one for general P/T nets. The algebras are examples of PROPs and each consists of a “wiring algebra” for transitions together with a simple “place algebra” for places. The wiring algebras themselves are generated by two different commutative monoid-cocommutative comonoid structures that interact in diverse ways according to the model of nets considered.
The algebras give a compositional account of the semantics of nets and thus suggest divide-and-conquer approaches to model checking Petri nets, as well asynchronous concurrent systems in general. I will illustrate this with some recent work that harnesses the algebraic approach for checking reachability in C/E nets.
