Transition Systems, Event Structures and Unfoldings

Elementary transition systems were introduced by the authors in DAIMI PB-310. They were proved to be, in a strong categorical sense, the transition system version of elementray net systems. The question arises whether the notion of a region and the axioms (mostly based on regions) imposed on ordinary transition systems to obtain elementray net systems. Stated differently, one colud ask whether elementray transition systems could also play a role in characterizing other models of concurrency. We show here that by smoothly stengthening the axioms of elementary transition systems one obtains a subclass called occurrence transitions systems which turn out to be categorically equivalent to the well-known model of concurrency called prime event structures. Next we show that occurrence transition systems are to elementry transition systems what occurrence nets are to elementary nets systems. We define an ''unfold'' operation on elementry transition systems which yields occurrence transistion systems. We then prove that this operation uniquely extends to a functor which is the right adjoint to the inclusion functor from (the full subcategory of) occurrence transition systems to (the category of) elementary transition systems. Thus the results of this paper also show that the semantic theory of elementray net systems has a nice counterpart in the more abstract world of transition systems.

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

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

Elementary transition systems

DAIMI Report Series ◽

10.7146/dpb.v19i310.6701 ◽

1990 ◽

Vol 19 (310) ◽

Cited By ~ 5

Author(s):

Mogens Nielsen ◽

Grzegorz Rozenberg ◽

P. S. Thiagarajan

Keyword(s):

Distributed Systems ◽

Transition Systems ◽

Common Framework ◽

Elementary Transition ◽

Models Of Concurrency ◽

Operational Behaviour

Transition systems are a simple and powerful formalism for explaining the operational behaviour of models of concurrency. They provide a common framework for investigating the interrelationships between different approaches to the study of distributed systems. Hence an important question to be answered is: which subclass of transition systems corresponds to a particular model of distributed systems? In this paper we provide an answer to this question for elementary net systems.

Download Full-text

Elementary Transition Systems and Refinement

DAIMI Report Series ◽

10.7146/dpb.v20i346.6576 ◽

1991 ◽

Vol 20 (346) ◽

Cited By ~ 3

Author(s):

Mogens Nielsen ◽

Grzegorz Rozenberg ◽

P. S. Thiagarajan

Keyword(s):

Transition System ◽

Local State ◽

Transition Systems ◽

Natural Properties ◽

Elementary Transition ◽

Abstract Level ◽

Standard Notion ◽

Definition Of ◽

Simple Notion

The model of Elementary Transition Systems has been introduced by the authors as an abstraction of Elementary Net Systems - with a formal embedding in terms of a categorical coreflection, keeping behavioural information like causality, concurrency and conflict, but forgetting the concrete programming of a particular behaviour over an event set using conditions. In this paper we give one example of the advantages of ETS over ENS, - the definition of local state refinement. We show that the well known problems in understanding within nets the simple notion of syntactic substitution of conditions by (sub) nets behaviourally, - these problems seem to disappear when moving to the more abstract level of ETS. Formally, we show that the ETS-version of condition-substitution does satisfy nice and natural properties, e.g., projection and compositionality results w.r.t. a standard notion of transition system morphisms.

Download Full-text

Transition-Systems, Event Structures, and Unfoldings

Information and Computation ◽

10.1006/inco.1995.1062 ◽

1995 ◽

Vol 118 (2) ◽

pp. 191-207 ◽

Cited By ~ 15

Author(s):

M. Nielsen ◽

G. Rozenberg ◽

P.S. Thiagarajan

Keyword(s):

Transition Systems ◽

Event Structures

Download Full-text

Bisimulation from Open Maps

BRICS Report Series ◽

10.7146/brics.v1i7.21663 ◽

1994 ◽

Vol 1 (7) ◽

Cited By ~ 6

Author(s):

André Joyal ◽

Mogens Nielsen ◽

Glynn Winskel

Keyword(s):

Petri Nets ◽

Parallel Computation ◽

Transition Systems ◽

New Model ◽

Event Structures ◽

Uniform Definition ◽

Refinement Operators ◽

Definition Of ◽

Open Maps

An abstract definition of bisimulation is presented. It enables a uniform definition of bisimulation across a range of different models for parallel computation presented as categories. As examples, transition systems, synchronisation trees, transition systems with independence (an abstraction from Petri nets) and labelled event structures are considered. On transition systems the abstract definition readily specialises to Milner's strong bisimulation. On event structures it explains and leads to a revision of history-preserving bisimulation of Rabinovitch and Traktenbrot, Goltz and van Glabeek. A tie-up with open maps in a (pre)topos, as they appear in the work of Joyal and Moerdijk, brings to light a promising new model, presheaves on categories of pomsets, into which the usual category of labelled event structures embeds fully and faithfully. As an indication of its promise, this new presheaf model has ``refinement'' operators, though further work is required to justify their appropriateness and understand their relation to previous attempts. The general approach yields a logic, generalising Hennessy-Milner logic, which is characteristic for the generalised notion of bisimulation.

Download Full-text

Target-oriented Petri Net Synthesis

A Mosaic of Computational Topics: from Classical to Novel ◽

10.3233/stal200007 ◽

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.

Download Full-text

Approximate Analyzing of Labeled Transition Systems

Mathematical Problems in Engineering ◽

10.1155/2015/963597 ◽

2015 ◽

Vol 2015 ◽

pp. 1-9

Author(s):

Qiong Yu ◽

Shihan Yang ◽

Jinzhao Wu

Keyword(s):

Control Systems ◽

Linear Systems ◽

Matrix Decomposition ◽

Transition System ◽

Formal Semantic ◽

Semantic Model ◽

Transition Systems ◽

State Space Explosion ◽

Normal Circumstance ◽

Time Linear

As the most important formal semantic model, labeled transition systems are widely used, which can describe the general concurrent systems or control systems without disturbance. However, under normal circumstance, transition systems are complex and difficult to use due to large amount of calculation and the state space explosion problems. In order to overcome these problems, approximate equivalent labeled transition systems are proposed by means of incomplete low-up matrix decomposition factorization. This technique can reduce the complexity of computation and calculate under the allowing errors. As for continuous-time linear systems, we develop a modeling method of approximated transition system based on the approximate solution of matrix, which provides a facility for approximately formal semantic modeling for linear systems and to effectively analyze errors. An example of application in the context of linear systems without disturbances is studied.

Download Full-text