Reference:

M. Koutny, J. Esparza, and E. Best. Operational semantics for the Petri box calculus. In B. Jonsson and J. Parrow, editors, Proceedings of CONCUR '94, number 836 in Lecture Notes in Computer Science, pages 210–225, 1994.

Abstract:

The Petri Box Calculus (PBC), based on Milner's CCS, has been developed to provide a compositional sematics of high level programming constructs in terms of class of Petri nets with interfaces, called Petri Boxes. In this paper we present a structural operational semantics for Box expressions which provide the syntax for the PBC. We show that the use of equations in addition to action rules leads to a uniform theory consisting essentially of a single action rule, a set of context rules, and a set of equations. To capture what is basically the standard Petri net transition rule, we introduce an overbarring and underbarring technique which is related to that used in the event systems due to Boudol and Castellani. We define step sequence rules and show their consistency and completeness with respect to the counterparts from net theory. The result hold also for expressions involving unguaranted recursion.

Suggested BibTeX entry:

@inproceedings{KEB94,
    author = {M. Koutny and J. Esparza and E. Best},
    booktitle = {Proceedings of CONCUR '94},
    editor = {B. Jonsson and J. Parrow},
    number = {836},
    pages = {210-225},
    series = {{Lecture Notes in Computer Science}},
    title = {Operational Semantics for the {P}etri Box Calculus},
    year = {1994}
}