Operational semantics for Petri net components

Jan Friso Groote; Marc Voorhoeve

doi:10.1016/j.tcs.2007.01.003

Operational semantics for Petri net components

Jan Friso Groote
, Marc Voorhoeve

Formal System Analysis

Research output: Contribution to journal › Article › Academic › peer-review

9 Citations (Scopus)

Abstract

We propose a calculus for marked labelled nets (components), with places and transitions as atoms and merge, addition, fusion and relabelling as operators. The operators are defined using graph-based transformations; each net can be represented by a term. Next, we define both a step semantics for nets and a Plotkin-style SOS semantics for net terms and show their equivalence. In the semantics, both state-oriented and event-oriented properties of components can be expressed. We give a few rules for reducing components to smaller equivalent ones. Keywords: Semantics; Petri nets; Process algebra; Bisimulation; Modelling; Verification

Original language	English
Pages (from-to)	1-19
Number of pages	19
Journal	Theoretical Computer Science
Volume	379
Issue number	1-2
DOIs	https://doi.org/10.1016/j.tcs.2007.01.003
Publication status	Published - 2007

Access to Document

10.1016/j.tcs.2007.01.003

Cite this

@article{4ef81bed39c24e3c9c6ccdcda77a1382,

title = "Operational semantics for Petri net components",

abstract = "We propose a calculus for marked labelled nets (components), with places and transitions as atoms and merge, addition, fusion and relabelling as operators. The operators are defined using graph-based transformations; each net can be represented by a term. Next, we define both a step semantics for nets and a Plotkin-style SOS semantics for net terms and show their equivalence. In the semantics, both state-oriented and event-oriented properties of components can be expressed. We give a few rules for reducing components to smaller equivalent ones. Keywords: Semantics; Petri nets; Process algebra; Bisimulation; Modelling; Verification",

author = "Groote, \{Jan Friso\} and Marc Voorhoeve",

year = "2007",

doi = "10.1016/j.tcs.2007.01.003",

language = "English",

volume = "379",

pages = "1--19",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier B.V.",

number = "1-2",

}

TY - JOUR

T1 - Operational semantics for Petri net components

AU - Groote, Jan Friso

AU - Voorhoeve, Marc

PY - 2007

Y1 - 2007

N2 - We propose a calculus for marked labelled nets (components), with places and transitions as atoms and merge, addition, fusion and relabelling as operators. The operators are defined using graph-based transformations; each net can be represented by a term. Next, we define both a step semantics for nets and a Plotkin-style SOS semantics for net terms and show their equivalence. In the semantics, both state-oriented and event-oriented properties of components can be expressed. We give a few rules for reducing components to smaller equivalent ones. Keywords: Semantics; Petri nets; Process algebra; Bisimulation; Modelling; Verification

AB - We propose a calculus for marked labelled nets (components), with places and transitions as atoms and merge, addition, fusion and relabelling as operators. The operators are defined using graph-based transformations; each net can be represented by a term. Next, we define both a step semantics for nets and a Plotkin-style SOS semantics for net terms and show their equivalence. In the semantics, both state-oriented and event-oriented properties of components can be expressed. We give a few rules for reducing components to smaller equivalent ones. Keywords: Semantics; Petri nets; Process algebra; Bisimulation; Modelling; Verification

U2 - 10.1016/j.tcs.2007.01.003

DO - 10.1016/j.tcs.2007.01.003

M3 - Article

SN - 0304-3975

VL - 379

SP - 1

EP - 19

JO - Theoretical Computer Science

JF - Theoretical Computer Science

IS - 1-2

ER -

Operational semantics for Petri net components

Abstract

Access to Document

Fingerprint

Cite this