Operational semantics for the Petri box calculus

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

23 Scopus citations

Abstract

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.

Original languageEnglish
Title of host publicationCONCUR 1994
Subtitle of host publicationConcurrency Theory - 5th International Conference, Proceedings
EditorsBengt Jonsson, Joachim Parrow
PublisherSpringer Verlag
Pages210-225
Number of pages16
ISBN (Print)9783540583295
DOIs
StatePublished - 1994
Externally publishedYes
Event5th International Conference on Concurrency Theory, CONCUR 1994 - Uppsala, Sweden
Duration: 22 Aug 199425 Aug 1994

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume836 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference5th International Conference on Concurrency Theory, CONCUR 1994
Country/TerritorySweden
CityUppsala
Period22/08/9425/08/94

Keywords

  • Petri nets
  • Process algebra
  • Step sequences
  • Structured operational semantics

Fingerprint

Dive into the research topics of 'Operational semantics for the Petri box calculus'. Together they form a unique fingerprint.

Cite this