scholarly journals Hereditary History Preserving Bisimilarity is Undecidable

1999 ◽  
Vol 6 (19) ◽  
Author(s):  
Marcin Jurdzinski ◽  
Mogens Nielsen
Keyword(s):  
Petri Nets ◽  
Transition Systems ◽  
Halting Problem ◽  
Proper Subclass ◽  
Intermediate Problem ◽  
Tiling Systems ◽  
Counter Machines ◽  
Undecidability Result

We show undecidability of hereditary history preserving bisimilarity<br />for finite asynchronous transition systems by a reduction from the halting<br />problem of deterministic 2-counter machines. To make the proof more<br />transparent we introduce an intermediate problem of checking domino<br />bisimilarity for origin constrained tiling systems. First we reduce the<br />halting problem of deterministic 2-counter machines to origin constrained<br />domino bisimilarity. Then we show how to model domino bisimulations as<br />hereditary history preserving bisimulations for finite asynchronous transitions<br />systems. We also argue that the undecidability result holds for<br />finite 1-safe Petri nets, which can be seen as a proper subclass of finite<br />asynchronous transition systems.

scholarly journals Hereditary History Preserving Simulation is Undecidable

1999 ◽  
Vol 6 (1) ◽  
Author(s):  
Marcin Jurdzinski ◽  
Mogens Nielsen
Keyword(s):  
Simulation Game ◽  
Turing Machines ◽  
Transition Systems ◽  
Halting Problem ◽  
Intermediate Problem

We show undecidability of hereditary history preserving simulation<br />for finite asynchronous transition systems by a reduction from the halting<br />problem of deterministic Turing machines. To make the proof more<br />transparent we introduce an intermediate problem of deciding the winner<br />in domino snake games. First we reduce the halting problem of deterministic<br />Turing machines to domino snake games. Then we show how to<br />model a domino snake game by a hereditary history simulation game on<br />a pair of finite asynchronous transition systems.

scholarly journals Bisimulation from Open Maps

1994 ◽  
Vol 1 (7) ◽  
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.

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.

scholarly journals Well (and Better) Quasi-Ordered Transition Systems

2010 ◽  
Vol 16 (4) ◽  
pp. 457-515 ◽  
Author(s):  
Parosh Aziz Abdulla
Keyword(s):  
Petri Nets ◽  
Timed Automata ◽  
Timed Petri Nets ◽  
Transition Systems ◽  
State Spaces ◽  
Rewriting Systems ◽  
Symbolic Representations ◽  
Infinite State ◽  
Lossy Channel ◽  
Quasi Ordering

AbstractIn this paper, we give a step by step introduction to the theory ofwell quasi-orderedtransition systems. The framework combines two concepts, namely (i) transition systems which aremonotonicwrt. awell-quasi ordering; and (ii) a scheme for symbolicbackwardreachability analysis. We describe several models with infinite-state spaces, which can be analyzed within the framework, e.g., Petri nets, lossy channel systems, timed automata, timed Petri nets, and multiset rewriting systems. We will also presentbetter quasi-orderedtransition systems which allow the design of efficient symbolic representations of infinite sets of states.

scholarly journals Transition systems, link graphs and Petri nets

2006 ◽  
Vol 16 (06) ◽  
pp. 989 ◽  
Author(s):  
JAMES J. LEIFER ◽  
ROBIN MILNER
Keyword(s):  
Petri Nets ◽  
Transition Systems

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 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 ◽  
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.

Sign in / Sign up

Export Citation Format

Share Document