Generalized linear equations with unordered data

Prelegent(ci)

Piotr Hofman

Afiliacja

Uniwersytet Warszawski

Termin

29 stycznia 2020 14:15

Pokój

p. 5050

Tytuł w języku angielskim

joint work with Jakub Różycki

Seminarium

Seminarium „Teoria automatów”

---

Consider a Petri net in which every token carries a k-element set of data, and whenever we fire a transition
then data from consumed and produced tokens are compared for equality and disequality. Such an extension
of Petri Nets allows more precise modeling than normal Petri Nets. Of course, comparing to Patri nets the analysis
of data nets is harder and natural problems become undecidable, but not all of them. In this work, we prove that so-called
integer reachability, useful as a witness of nonreachability in standard sens, is in NEexpTime.
The case when k=1 was considered in the paper published at LICS 2017.
During the talk, I will focus on the cases when k=1 and k=2, to illustrate developed techniques.

---