Lookup NU author(s): Professor Maciej Koutny,
Dr Lukasz Mikulski
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License (CC BY-NC 4.0).
Petri nets are a general formal model of concurrent systems which supports both action-based and state-based modelling and reasoning. One of important behavioural properties investigated in the context of Petri nets has beenreversibility, understood as the possibility of returning to the initial marking from any reachable net marking. Thus reversibility in Petri nets is a global property. Reversible computation, on the other hand, is typically a local mechanism using which a system can undo some of the executed actions. This paper is concerned with the modelling of reversible computation within Petri nets. A key idea behind the proposed construction is to add `reverse' versions of selected transitions. Since such a modification can severely impact on the behavior of the system, it is crucial, in particular, to be able to determine whether the modified system has a similar set of states as the original one. We first prove that the problem of establishing whether the two nets have the same reachable markings is undecidable even in the restricted case discussed in this paper. We then show that the problem of checking whether the reachability sets of the two nets cover the same markings is decidable.
Author(s): Barylska K, Koutny M, Mikulski L, Piatkowski M
Editor(s): Devitt, S; Lanese, I
Publication type: Conference Proceedings (inc. Abstract)
Publication status: Published
Conference Name: 8th Conference on Reversible Computation
Year of Conference: 2016
Print publication date: 19/07/2016
Online publication date: 30/06/2016
Acceptance date: 21/03/2011
Date deposited: 10/04/2016
Library holdings: Search Newcastle University Library for this item
Series Title: Lecture Notes in Computer Science