Minimizing Finite Complete Prefixes

Reference:

Keijo Heljanko. Minimizing finite complete prefixes. In H.-D. Burkhard, L. Czaja, H.-S. Nguyen, and P. Starke, editors, Proceedings of the Workshop Concurrency, Specification & Programming 1999, pages 83–95, Warsaw, Poland, September 1999. Warsaw University.

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 from 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.

Keywords:

Petri nets, unfoldings, finite complete prefixes

Suggested BibTeX entry:

@inproceedings{Heljanko:CSP99,
    address = {Warsaw, Poland},
    author = {Keijo Heljanko},
    booktitle = {Proceedings of the Workshop Concurrency, Specification \& Programming 1999},
    editor = {H.-D. Burkhard and L. Czaja and H.-S. Nguyen and P. Starke},
    month = {September},
    pages = {83--95},
    publisher = {Warsaw University},
    title = {Minimizing Finite Complete Prefixes},
    year = {1999},
}