In: Lecture Notes in Computer Science, Vol. 1091; Proc. 17th International Conference in Application and Theory of Petri Nets (ICATPN'96), Osaka, Japan, pages 366-379. Springer-Verlag, June 1996.
Abstract: In this paper we present an O(|S| x |T|)-algorithm to decide if a given net is regular. The definition of regular nets refers to the linear algebraic representation of nets. Regularity is a sufficient condition for an ordinary net to be live and bounded. Live and bounded extended free choice nets (EFC-nets for short) are a proper subset of regular nets. It has been shown that regular marked nets are not just a technical generalization of EFC-nets but have in fact more expressive power. We reduce the problem of regularity to the problem of liveness and boundedness of EFC-nets. To decide the well-formedness of a given EFC-net we give an inductive criterion of well-formedness. To prove the soundness of our algorithm we give a theorem on covering of strongly connected EFC-nets by minimal deadlock. An O(|S| x |T|)-algorithm to decide the liveness of an initial marking for well-formed EFC-nets is given.