Skip to main navigation Skip to search Skip to main content

Verifying generalized soundness for workflow nets

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Downloads (Pure)

Abstract

We improve the decision procedure from [10] for the problem of generalized soundness of workflow nets. A workflow net is generalized sound iff 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. Our new decision procedure not only reports whether the net is sound or not, but also returns a counterexample in case the workflow net is not generalized sound. We report on experimental results obtained with the prototype we made and explain how the procedure can be used for the compositional verification of large workflows.
Original languageEnglish
Title of host publicationProceedings of the 6th International Andrei Ershov Memorial Conference : Perspectives of Systems Informatics (PSI 2006) 27-30 June 2006, Novosibirsk, Russia
EditorsI. Virbitskaite, A. Voronkov
PublisherSpringer
Pages235-247
ISBN (Print)3-540-70880-4
DOIs
Publication statusPublished - 2007
Eventconference; PSI 2006, Novosibirsk, Russia; 2006-06-27; 2006-06-30 -
Duration: 27 Jun 200630 Jun 2006

Publication series

NameLecture Notes in Computer Science
Volume4378
ISSN (Print)0302-9743

Conference

Conferenceconference; PSI 2006, Novosibirsk, Russia; 2006-06-27; 2006-06-30
Period27/06/0630/06/06
OtherPSI 2006, Novosibirsk, Russia

Fingerprint

Dive into the research topics of 'Verifying generalized soundness for workflow nets'. Together they form a unique fingerprint.

Cite this