Generalised soundness of workflow nets is decidable

M. Voorhoeve, K.M. Hee, van, N. Sidorova

Research output: Book/ReportReportAcademic

81 Downloads (Pure)

Abstract

Abstract. We investigate the decidability of the problem of generalised soundness for Workflow nets: "Every marking reachable from an initial marking with k tokens on the initial place terminates properly, i.e. it can reach a marking with k tokens on the final place, for an arbitrary natural number k". We start with considering simple correctness criteria for Workflow nets and reduce them to the check of structural properties formulated in terms of traps and siphons, which can be easily checked. We call the nets that possess those properties Batch Workflow nets (BWF-nets). We show that every WF-net is either not sound or it can be transformed to a BWF-net with the same behaviour. Then we use algebraic methods to prove that generalized soundness is decidable for BWF-nets and give a decision procedure. Keywords: Petri nets; workflows; verification; soundness, decidability.
Original languageEnglish
Place of PublicationEindhoven
PublisherTechnische Universiteit Eindhoven
Number of pages18
Publication statusPublished - 2003

Publication series

NameComputer science reports
Volume0315
ISSN (Print)0926-4515

Fingerprint Dive into the research topics of 'Generalised soundness of workflow nets is decidable'. Together they form a unique fingerprint.

  • Cite this

    Voorhoeve, M., Hee, van, K. M., & Sidorova, N. (2003). Generalised soundness of workflow nets is decidable. (Computer science reports; Vol. 0315). Technische Universiteit Eindhoven.