PETRI NETS AND STEP TRANSITION SYSTEMS

1992 ◽  
Vol 03 (04) ◽  
pp. 443-478 ◽  
Author(s):  
MADHAVAN MUKUND
Keyword(s):  
Petri Nets ◽  
Petri Net ◽  
Transition System ◽  
Computing Systems ◽  
Transition Systems ◽  
Labelled Transition Systems ◽  
Natural Sense ◽  
Step Transition ◽  
Operational Behaviour ◽  
Natural Way

Labelled transition systems are a simple yet powerful formalism for describing the operational behaviour of computing systems. They can be extended to model concurrency faithfully by permitting transitions between states to be labelled by a collection of actions, denoting a concurrent step. Petri nets (or Place/Transition nets) give rise to such step transition systems in a natural way—the marking diagram of a Petri net is the canonical transition system associated with it. In this paper, we characterize the class of PN-transition systems, which are precisely those step transition systems generated by Petri nets. We express the correspondence between PN-transition systems and Petri nets in terms of an adjunction between a category of PN-transition systems and a category of Petri nets in which the associated morphisms are behaviour-preserving in a strong and natural sense.

scholarly journals Transition System Models for Concurrency

1992 ◽  
Vol 21 (399) ◽  
Author(s):  
Madhavan Mukund
Keyword(s):  
Petri Nets ◽  
Transition System ◽  
Transition Systems ◽  
Labelled Transition Systems ◽  
System Models ◽  
Elementary Transition ◽  
Step Transition ◽  
Sequential Behaviour

<p>Labelled transition systems can be extended to faithfully model concurrency by permitting transitions between states to be labelled by a collection of actions, denoting a concurrent step, We can characterize a subclass of these <em>step transition systems</em>, called PN-transition systems, which describe the behaviour of Petri nets.</p><p>This correspondence is formally described in terms of a coreflection between a category of <em>PN</em>-transition systems and a category of Petri nets.</p><p>In this paper, we show that we can define subcategories of <em>PN</em>-transition systems whose objects are <em> safe PN-transition systems and elementary PN-transition systems</em> such that there is a coreflection between these subcategories and subcategories of our category of Petri nets corresponding to safe nets and elementary net systems.</p><p>We also prove that our category of elementary <em>PN</em>-transition systems is equivalent to the category of (sequential) <em> elementary transition systems</em> defined by Nielsen, Rozenberg and Thiagarajan, thereby establishing that the concurrent behaviour of an elementary net system can be completely recovered from a description of its sequential behaviour. Finally, we establish a coreflection between our category of safe <em>PN</em>-transition system and a subcategory of <em>asynchronous transition systems</em> which has been shown by Winskel and Nielsen to be closely linked to safe nets.</p>

Target-oriented Petri Net Synthesis

2020 ◽  
Author(s):  
Eike Best ◽  
Raymond Devillers ◽  
Evgeny Erofeev ◽  
Harro Wimmel
Keyword(s):  
Petri Nets ◽  
Petri Net ◽  
Transition System ◽  
Efficient Synthesis ◽  
Transition Systems ◽  
Np Complete ◽  
Full Class ◽  
Petri Net Synthesis ◽  
Labelled Transition System ◽  
Additional Constraints

When a Petri net is synthesised from a labelled transition system, it is frequently desirable that certain additional constraints are fulfilled. For example, in circuit design, one is often interested in constructing safe Petri nets. Targeting such subclasses of Petri nets is not necessarily computationally more efficient than targeting the whole class. For example, targeting safe nets is known to be NP-complete while targeting the full class of place/transition nets is polynomial, in the size of the transition system. In this paper, several classes of Petri nets are examined, and their suitability for being targeted through efficient synthesis from labelled transition systems is studied and assessed. The focus is on choice-free Petri nets and some of their subclasses. It is described how they can be synthesised efficiently from persistent transition systems, summarising and streamlining in tutorial style some of the authors’ and their groups’ work over the past few years.

Target-oriented Petri Net Synthesis

2020 ◽  
Vol 175 (1-4) ◽  
pp. 97-122
Author(s):  
Eike Best ◽  
Raymond Devillers ◽  
Evgeny Erofeev ◽  
Harro Wimmel
Keyword(s):  
Petri Nets ◽  
Circuit Design ◽  
Petri Net ◽  
Transition System ◽  
Transition Systems ◽  
Np Complete ◽  
Full Class ◽  
Petri Net Synthesis ◽  
Labelled Transition System ◽  
Additional Constraints

When a Petri net is synthesised from a labelled transition system, it is frequently desirable that certain additional constraints are fulfilled. For example, in circuit design, one is often interested in constructing safe Petri nets. Targeting such subclasses of Petri nets is not necessarily computationally more efficient than targeting the whole class. For example, targeting safe nets is known to be NP-complete while targeting the full class of place/transition nets is polynomial, in the size of the transition system. In this paper, several classes of Petri nets are examined, and their suitability for being targeted through efficient synthesis from labelled transition systems is studied and assessed. The focus is on choice-free Petri nets and some of their subclasses. It is described how they can be synthesised efficiently from persistent transition systems, summarising and streamlining in tutorial style some of the authors’ and their groups’ work over the past few years.

scholarly journals Articulations and Products of Transition Systems and their Applications to Petri Net Synthesis

2022 ◽  
Vol 183 (1-2) ◽  
pp. 1-31
Author(s):  
Raymond Devillers
Keyword(s):  
Petri Nets ◽  
Petri Net ◽  
Composition Operators ◽  
Original System ◽  
Divide And Conquer ◽  
Transition Systems ◽  
Structure Transition ◽  
Labelled Transition Systems ◽  
Speed Up ◽  
Petri Net Synthesis

In order to speed up the synthesis of Petri nets from labelled transition systems, a divide and conquer strategy consists in defining decompositions of labelled transition systems, such that each component is synthesisable iff so is the original system. Then corresponding Petri Net composition operators are searched to combine the solutions of the various components into a solution of the original system. The paper presents two such techniques, which may be combined: products and articulations. They may also be used to structure transition systems, and to analyse the performance of synthesis techniques when applied to such structures.

scholarly journals Model Checking Coloured Petri Nets - Exploiting Strongly Connected Components

1997 ◽  
Vol 26 (519) ◽  
Author(s):  
Allan Cheng ◽  
Søren Christensen ◽  
Kjeld Høyer Mortensen
Keyword(s):  
Model Checking ◽  
Petri Nets ◽  
The State ◽  
Connected Components ◽  
Coloured Petri Nets ◽  
Transition Systems ◽  
Strongly Connected Components ◽  
State Spaces ◽  
Labelled Transition Systems ◽  
Strongly Connected

In this paper we present a CTL-like logic which is interpreted over the state spaces of Coloured Petri Nets. The logic has been designed to express properties of both state and transition information. This is possible because the state spaces are labelled transition systems. We compare the expressiveness of our logic with CTL's. Then, we present a model checking algorithm which for efficiency reasons utilises strongly connected components and formula reduction rules. We present empirical results for non-trivial examples and compare the performance of our algorithm with that of Clarke, Emerson, and Sistla.

scholarly journals Labelled transition system approach to distributed computing systems

2016 ◽  
Vol 8 (3) ◽  
pp. 19-32
Author(s):  
Dang Van Hung
Keyword(s):  
Distributed Computing ◽  
System Approach ◽  
Transition System ◽  
Distributed Computing Systems ◽  
Computing Systems ◽  
Transition Systems ◽  
Local Process ◽  
Global Properties ◽  
Labelled Transition System

The present paper introduces the  notion of  distributed transition systems for modeling, designing and  understanding distributed computing systems. The concurrency can be expressed explicitly in the model. Some of  the  global properties of the  systems are discussed and determined. It is  shown in the paper that  by keeping knowledge of other processes in each process of a system, some of its global properties can be synthesized from only few local process states.

scholarly journals CCS, Locations and Asynchronous Transition Systems

1992 ◽  
Vol 21 (395) ◽  
Author(s):  
Madhavan Mukund ◽  
Mogens Nielsen
Keyword(s):  
Operational Semantics ◽  
Transition System ◽  
Additional Property ◽  
Close Correspondence ◽  
Transition Systems ◽  
Natural Way

<p>Our aim is to provide a simple non-interleaved operational semantics for CCS in terms of a model that is easy to understand - asynchronous transition systems. Our approach is guided by the requirement that the semantics should identify the concurrency present in the system in a natural way, in terms of events occurring at independent locations in the system.</p><p>We extend the standard interleaving transition system for CCS by introducing labels on the transitions with information about the locations of events. We then show that the resulting transition system is an asynchronous transition system which has the additional property of being <em>elementary</em>, which means that it can also be represented by a 1-safe net. We establish a close correspondence between our semantics and other approaches in terms of <em>foldings</em>.</p><p>We also introduce a notion of bisimulation on asynchronous transition systems which preserves independence. We conjecture that the induced equivalence on CCS processes coincides with the notion of <em>location equiualence</em> proposed by Boudol et al.</p>

scholarly journals A Comparison of Petri Net Semantics under the Collective Token Philosophy

1998 ◽  
Vol 5 (17) ◽  
Author(s):  
Roberto Bruni ◽  
José Meseguer ◽  
Ugo Montanari ◽  
Vladimiro Sassone
Keyword(s):  
Petri Nets ◽  
Petri Net ◽  
Equational Logic ◽  
Monoidal Categories ◽  
Transition Systems ◽  
Logical Description ◽  
Membership Equational Logic

In recent years, several semantics for place/transition Petri nets have been proposed that adopt the collective token philosophy. We investigate distinctions and similarities between three such models, namely configuration structures, concurrent transition systems, and (strictly) symmetric (strict) monoidal categories. We use the notion of adjunction to express each connection. We also present a purely logical description of the collective token interpretation of net behaviours in terms of theories and theory morphisms in partial membership equational logic.

scholarly journals Who is obliged when many are involved? Labelled transition system modelling of how obligation arises

2020 ◽  
Author(s):  
Piotr Kulicki ◽  
Robert Trypuz ◽  
Marek Sergot
Keyword(s):  
Freedom Of Expression ◽  
Transition System ◽  
The Other ◽  
System Modelling ◽  
Transition Systems ◽  
Labelled Transition Systems ◽  
Polish Law ◽  
The Right ◽  
Labelled Transition System

AbstractThe paper tackles the problem of the relation between rights and obligations. Two examples of situations in which such a relation occurs are discussed. One concerns the abortion regulations in Polish law, the other one—a clash between freedom of expression and freedom of enterprise occurring in the context of discrimination. The examples are analysed and formalised using labelled transition systems in the $$n\mathcal {C}+$$ n C + framework. Rights are introduced to the system as procedures allowing for their fulfilment. Obligations are based on the requirement of cooperation in the realisation of the goals of the agent that has a right. If the right of an agent cannot be fulfilled without an action of another agent, then that action is obligatory for that agent. If there are many potential contributors who are individually allowed to refuse, then the last of them is obliged to help when all the others have already refused. By means of formalisation this account of the relation under consideration is precisely expressed and shown consistent.

scholarly journals On the Power of Labels in Transition Systems

2001 ◽  
Vol 8 (19) ◽  
Author(s):  
Jirí Srba
Keyword(s):  
Model Checking ◽  
Petri Nets ◽  
Transition Systems ◽  
Labelled Transition Systems ◽  
Pushdown Automata ◽  
General Reduction

In this paper we discuss the role of labels in transition systems with regard to bisimilarity and model checking problems. We suggest a general reduction from labelled transition systems to unlabelled ones, preserving bisimilarity and satisfiability of mu-calculus formulas. We apply the reduction to the class of transition systems generated by Petri nets and pushdown automata, and obtain several decidability/complexity corollaries for unlabelled systems. Probably the most interesting result is undecidability of strong bisimilarity for unlabelled Petri nets.

Sign in / Sign up

Export Citation Format

Share Document