An O(|S|×|T|)-algorithm to verify liveness and boundedness in extended free choice nets

This paper presents an O(|S|×|T|)-algorithm to decide if a given EFC-net is live and bounded, which is a reduction by one order of magnitude, compared to the algorithm in Kemper (1994) (O(|S|²|T|)). Kemper´s algorithm is based on the rank theorem. This theorem is a slightly different version of the rank theorem of Esparza (1990). Two main steps of Kemper´s algorithm are: to find a cover of S-components and to compute the rank of incidence matrix. Finding a cover of S-components has been done in Kemper (1994) in O(|S|×|T|)-time. Since the calculation of a matrix rank requires O(|S|²|T|), the rank theorem can be checked in O(|S| ²|T|). Hence the calculation of the matrix rank dominates the complexity of the algorithm. To reduce the complexity one needs another criterion; well-formedness. In order to reduce the complexity of the decision algorithm the author combines the two approaches above. Since well-formedness is only a necessary condition for a net to be live and bounded, one needs to decide if a given initial marking of a well-formed net is live and bounded. An O(|S|×|T|)-algorithm to decide this problem is given