A framework for efficiently deciding language inclusion for sound unlabelled WF-nets

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

1 Citation (Scopus)

Abstract

We present a framework to efficiently check language inclusion between two sound unlabelled WF-nets. That is, to efficiently check whether every successfully terminating transition sequence of one sound unlabelled WF-net also is a successfully terminating transition sequence of a second sound unlabelled WF-net. Existing approaches for checking language inclusion are typically based on the underlying transition systems of both nets, and hence are subject to the well-known state-explosion problem. As a result, these approaches cannot check language inclusion on sound unlabelled WF-nets in polynomial time. Our framework allows for efficient language inclusion checks even if parallelism is present, by comparing specific net abstractions that can be computed and compared in polynomial time. For sound unlabelled WF-nets that are free-choice and do not contain loops, we prove that our approach is complete.
Original languageEnglish
Title of host publicationInternational Workshop on Petri Nets and Software Engineering (PNSE'13, Milano, Italy, June 24-25, 2013)
EditorsD. Moldt, H. Rölke
PublisherCEUR-WS.org
Pages135-154
Publication statusPublished - 2013
EventInternational Workshop on Petri Nets and Software Engineering 2013 (PNSE '13), June 24-25, 2013, Milan, Italy - Milan, Italy
Duration: 24 Jun 201325 Jun 2013

Publication series

NameCEUR Workshop Proceedings
Volume989
ISSN (Print)1613-0073

Workshop

WorkshopInternational Workshop on Petri Nets and Software Engineering 2013 (PNSE '13), June 24-25, 2013, Milan, Italy
Abbreviated titlePNSE '13
CountryItaly
CityMilan
Period24/06/1325/06/13
OtherWorkshop co-located with the 34th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2013)

Fingerprint

Dive into the research topics of 'A framework for efficiently deciding language inclusion for sound unlabelled WF-nets'. Together they form a unique fingerprint.

Cite this