Soundness for Workflows with Reset Arcs

Speaker(s)

Piotr Hofman

Affiliation

University of Warsaw

Language of the talk

English

Date

Oct. 30, 2024, 2:15 p.m.

Room

room 5440

Title in Polish

Soundness for Workflows with Reset Arcs

Seminar

Seminar Automata Theory

---

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

---