A polynomial λ-bisimilar normalization for reset Petri nets

Reset Petri nets extend Petri nets by allowing transitions to empty places, in addition to the usual adding or removing of constants. A Reset Petri net is normalized if the flow function over the Petri arcs (labeled with integers) and the initial state are valuated into {0,1}. In this paper, we give...

Full description

Saved in:
Bibliographic Details
Published in:Theoretical computer science 1999-07, Vol.222 (1), p.187-194
Main Authors: Dufourd, Catherine, Finkel, Alain
Format: Article
Language:English
Subjects:
Algorithmics. Computability. Computer arithmetics
Applied sciences
Automata. Abstract machines. Turing machines
Computer science
control theory
systems
Concurrency
Equivalences
Exact sciences and technology
Petri nets
Theoretical computing
Verification
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Reset Petri nets extend Petri nets by allowing transitions to empty places, in addition to the usual adding or removing of constants. A Reset Petri net is normalized if the flow function over the Petri arcs (labeled with integers) and the initial state are valuated into {0,1}. In this paper, we give an efficient method to turn a general Reset Petri net into a λ-bisimilar normalized Reset Petri net. Our normalization preserves the main usually studied properties: boundedness, reachability, t-liveness and language (through a λ-labeling function). The main contribution is the improvement of the complexity: our algorithm takes a time in O(size( N) 2), for a Reset Petri net N, while other known normalizations require an exponential space and are presented for Petri nets only.
ISSN:0304-3975
1879-2294
DOI:10.1016/S0304-3975(98)00351-X