Lookup NU author(s): Professor Maciej Koutny,
Professor Eike Best
Full text for this publication is not currently held within this repository. Alternative links are provided below where available.
The Petri Box Calculus (PBC), based on Milner's CCS, has been developed to provide a compositional semantics of high level programming constructs in terms of a 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 results hold also for expressions involving unguarded recursion.
Author(s): Koutny M, Esparza J, Best E
Editor(s): Jonsson, B., Parrow, J.
Publication type: Conference Proceedings (inc. Abstract)
Publication status: Published
Conference Name: 5th International Conference on Concurrency Theory (CONCUR)
Year of Conference: 1994
ISSN: 0302-9743 (Print) 1611-3349 (Online)
Notes: Work done within the Esprit Basic Research Action 3148 DEMON and the Esprit Basic Research Working Group 6067 CALIBAN.
Library holdings: Search Newcastle University Library for this item
Series Title: Lecture Notes in Computer Science