Target-oriented Petri Net Synthesis

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.

Download Full-text

PETRI NETS AND STEP TRANSITION SYSTEMS

International Journal of Foundations of Computer Science ◽

10.1142/s0129054192000231 ◽

1992 ◽

Vol 03 (04) ◽

pp. 443-478 ◽

Cited By ~ 76

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.

Download Full-text

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

Fundamenta Informaticae ◽

10.3233/fi-2021-2080 ◽

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.

Download Full-text

Labelled transition system approach to distributed computing systems

Journal of Computer Science and Cybernetics ◽

10.15625/1813-9663/8/3/8272 ◽

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.

Download Full-text

Foundations of Modular SOS

BRICS Report Series ◽

10.7146/brics.v6i54.20124 ◽

1999 ◽

Vol 6 (54) ◽

Cited By ~ 8

Author(s):

Peter D. Mosses

Keyword(s):

Programming Languages ◽

Transition System ◽

Transition Systems ◽

Labelled Transition System

A novel form of labelled transition system is proposed, where the labels are the arrows of a category, and adjacent labels in computations are required to be composable. Such transition systems provide the foundations for modular SOS descriptions of programming languages. Three fundamental ways of transforming label categories, analogous to monad transformers, are provided, and it is shown that their applications preserve computations in modular SOS. The approach is illustrated with fragments taken from a modular SOS for ML concurrency primitives.

Download Full-text

Transition System Models for Concurrency

DAIMI Report Series ◽

10.7146/dpb.v21i399.6633 ◽

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

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 step transition systems, called PN-transition systems, which describe the behaviour of Petri nets.This correspondence is formally described in terms of a coreflection between a category of PN-transition systems and a category of Petri nets.In this paper, we show that we can define subcategories of PN-transition systems whose objects are safe PN-transition systems and elementary PN-transition systems 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.We also prove that our category of elementary PN-transition systems is equivalent to the category of (sequential) elementary transition systems 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 PN-transition system and a subcategory of asynchronous transition systems which has been shown by Winskel and Nielsen to be closely linked to safe nets.

Download Full-text

A domain equation for refinement of partial systems

Mathematical Structures in Computer Science ◽

10.1017/s0960129504004268 ◽

2004 ◽

Vol 14 (4) ◽

pp. 469-505 ◽

Cited By ~ 15

Author(s):

MICHAEL R. A. HUTH ◽

RADHA JAGADEESAN ◽

DAVID A. SCHMIDT

Keyword(s):

Transition System ◽

Reactive System ◽

Static Structure ◽

Transition Systems ◽

Temporal Properties ◽

Modal Transition Systems ◽

Partial Systems ◽

Partial Bisimulation ◽

Labelled Transition System ◽

Mixed Transition

A reactive system can be specified by a labelled transition system, which indicates static structure, along with temporal-logic formulas, which assert dynamic behaviour. But refining the former while preserving the latter can be difficult, because:(i) Labelled transition systems are ‘total’ – characterised up to bisimulation – meaning that no new transition structure can appear in a refinement.(ii) Alternatively, a refinement criterion not based on bisimulation might generate a refined transition system that violates the temporal properties.In response, Larsen and Thomson proposed modal transition systems, which are ‘partial’, and defined a refinement criterion that preserved formulas in Hennessy–Milner logic. We show that modal transition systems are, up to a saturation condition, exactly the mixed transition systems of Dams that meet a mix condition, and we extend such systems to non-flat state sets. We then solve a domain equation over the mixed powerdomain whose solution is a bifinite domain that is universal for all saturated modal transition systems and is itself fully abstract when considered as a modal transition system. We demonstrate that many frameworks of partial systems can be translated into the domain: partial Kripke structures, partial bisimulation structures, Kripke modal transition systems, and pointer-shape-analysis graphs.

Download Full-text

A Comparison of Petri Net Semantics under the Collective Token Philosophy

BRICS Report Series ◽

10.7146/brics.v5i17.19423 ◽

1998 ◽

Vol 5 (17) ◽

Cited By ~ 2

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.

Download Full-text

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

Artificial Intelligence and Law ◽

10.1007/s10506-020-09279-9 ◽

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.

Download Full-text

Liveness and boundedness analysis of Petri net synthesis

Mathematical Structures in Computer Science ◽

10.1017/s0960129512000515 ◽

2014 ◽

Vol 24 (5) ◽

Author(s):

CHUANLIANG XIA

Keyword(s):

Petri Nets ◽

Petri Net ◽

Flexible Manufacturing ◽

Manufacturing System ◽

Flexible Manufacturing System ◽

Dynamic Properties ◽

Synthesis Method ◽

Sufficient Conditions ◽

Sufficient And Necessary Conditions ◽

Petri Net Synthesis

We provide motivation for and then study the synthesis of Petri nets. Synthesis can avoid the state exploration problem by guaranteeing correctness for the Petri net. We propose conditions to be imposed on a synthesis shared pb-type subnet for systems specified in Petri nets that ensure the preservation of the liveness and boundedness structural properties. Specifically, we propose a group of sufficient conditions, or both sufficient and necessary conditions, for liveness preservation and boundedness preservation. Possible applications of this synthesis method are illustrated through an example in the form of a flexible manufacturing system. These results are useful for studying the static and dynamic properties of Petri nets for analysing the properties of large complex systems.

Download Full-text