In: Burkhard, H.-D.; Czaja, L.; Nguyen, H.-S.; Starke, P.: Proceedings of the CSP'99 Workshop, Warsaw, 28-30 September 1999, pages 83-95. 1999.
Abstract: Finite complete prefixes are used as a verification method for Petri nets and other formalisms where a similar notion of partial order behavior can be applied. They were introduced by McMillan, who also gave an algorithm to generate a finite complete prefix fro a system description given as a Petri net. Later Esparza, Römer and Vogler improved McMillan's prefix generation algorithm, which could sometimes create exponentially larger prefixes than required. In this work we refine the approach of Esparza et al. further, and define a refined cut-off criterion, which makes it sometimes possible to create much smaller finite complete prefixes. Experimental results from a prototype implementation, a prefix minimizer, are presented. The method can also be applied directly during prefix generation.