Soundness for Workflows with Reset Arcs

Prelegent(ci)

Piotr Hofman

Afiliacja

University of Warsaw

Język referatu

angielski

Termin

30 października 2024 14:15

Pokój

p. 5440

Tytuł w języku polskim

Soundness for Workflows with Reset Arcs

Seminarium

Seminarium „Teoria automatów”

---

Workflows are a subclass of Petri nets designed to model business processes. Various definitions of soundness for workflows have been proposed, with the two most prominent being "soundness" and the stronger "generalized soundness." We begin by recalling these fundamental definitions and their justification.

Some aspects of business processes cannot be modeled using pure Petri nets and require more expressive formalisms, such as Petri nets with reset arcs. While it is known that soundness is undecidable for workflows with reset arcs, the status of generalized soundness remained an open problem.

Although generalized soundness is undecidable, in collaboration with Michael Blondin, Alain Finkel, Filip Mazowiecki, and Philip Offtermatt, we almost proved its decidability. This almost-proof led us to define a new notion of decidable soundness, which lies between soundness and generalized soundness. In this talk, I will present elements of the "almost proof," discuss both undecidability results, and explain this intermediate notion of soundness.

The talk is based on joint work with Michael Blondin, Alain Finkel, Piotr Hofman, Filip Mazowiecki, and Philip Offtermatt: Soundness of Reset Workflow Nets. LICS 2024: 13:1-13:14

---