Wyniki wyszukiwania - BazTech

1

Investigating Reversibility of Steps in Petri Nets

de Frutos Escrig David, Koutny Maciej, Mikulski Łukasz

Fundamenta Informaticae

|

2021

|

Vol. 183, nr 1-2

67--96

EN

In reversible computations one is interested in the development of mechanisms allowing to undo the effects of executed actions. The past research has been concerned mainly with reversing single actions. In this paper, we consider the problem of reversing the effect of the execution of groups of actions (steps). Using Petri nets as a system model, we introduce concepts related to this new scenario, generalising notions used in the single action case. We then present properties arising when reverse actions are allowed in place/transition nets (PT-nets). We obtain both positive and negative results, showing that allowing steps makes reversibility more problematic than in the interleaving/sequential case. In particular, we demonstrate that there is a crucial difference between reversing steps which are sets and those which are true multisets. Moreover, in contrast to sequential semantics, splitting reverses does not lead to a general method for reversing bounded PT-nets. We then show that a suitable solution can be obtained by combining split reverses with weighted read arcs.

2

Persistent and Nonviolent Steps and the Design of GALS Systems

Fernandes J., Koutny M., Mikulski Ł, Pietkiewicz-Koutny M., Sokolov D., Yakovlev A.

Fundamenta Informaticae

|

2015

|

Vol. 137, nr 1

143--170

EN

A concurrent system is persistent if throughout its operation no activity which became enabled can subsequently be prevented from being executed by any other activity. This is often a highly desirable (or even necessary) property; in particular, if the system is to be implemented in hardware. Over the past 40 years, persistence has been investigated and applied in practical implementations assuming that each activity is a single atomic action which can be represented, for example, by a single transition of a Petri net. In this paper we investigate the behaviour of GALS (Globally Asynchronous Locally Synchronous) systems in the context of VLSI circuits. The specification of a system is given in the form of a Petri net. Our aim is to re-design the system to optimise signal management, by grouping together concurrent events. Looking at the concurrent reachability graph of the given Petri net, we are interested in discovering events that appear in ‘bundles’, so that they all can be executed in a single clock tick. The best candidates for bundles are sets of events that appear and re-appear over and over again in the same configurations, forming ‘persistent’ sets of events. Persistence was considered so far only in the context of sequential semantics. In this paper, we move to the realm of step based execution and consider not only steps which are persistent and cannot be disabled by other steps, but also steps which are nonviolent and cannot disable other steps. We then introduce a formal definition of a bundle and propose an algorithm to prune the behaviour of a system, so that only bundled steps remain. The pruned reachability graph represents the behaviour of a re-engineered system, which in turn can be implemented in a new Petri net using the standard techniques of net synthesis. The proposed algorithm prunes reachability graphs of persistent and safe nets leaving bundles that represent maximally concurrent steps.

3

An Operational Petri Net Semantics for A2CCS

Gorrieri R., Versari C.

Fundamenta Informaticae

|

2011

|

Vol. 109, nr 2

135-160

EN

A2CCS is a conservative extension of CCS, enriched with an operator of strong prefixing, enabling the modeling of atomic sequences and multi-party synchronization (realized as an atomic sequence of binary synchronizations); the classic dining philosophers problem is used to illustrate the approach. A step semantics for A2CCS is also presented directly as a labeled transition system. A safe Petri net semantics for this language is presented, following the approach of Degano, De Nicola, Montanari and Olderog. We prove that a process p and its associated net Net(p) are interleaving bisimilar (Theorem 5.1). Moreover, to support the claim that the intended concurrency is wellrepresented in the net, we also prove that a process p and its associated net Net(p) are step bisimilar (Theorem 5.2).

4

Comparing truly concurrent semantics for contextual Place/Transition nets with inhibitor and read arcs

Busi N., Pinna G.M.

Fundamenta Informaticae

|

2000

|

Vol. 44, Nr 3

209-244

EN

The paper is centered around the study and comparison of truly concurrent semantics for P/T nets with inhibitor and read arcs (called henceforth contextual P/T nets). We start proposing a causal semantics for P/T nets, that we prove to be equivalent to history preserving bisimulation defined on nonsequential processes. Then we develop a conservative extension of the causal semantics to contextual P/T nets and we prove this one to be finer than step semantics. Finally, a comparison of causal semantics with the process based semantics for contextual P/T systems proposed in [7] is carried out.

5

Process semantics for Place/Transition nets with inhibitor and read arcs

Busi N., Pinna G.M.

Fundamenta Informaticae

|

1999

|

Vol. 40, Nr 2,3

165-197

EN

In this paper we introduce a truly concurrent semantics for P/T nets with inhibitor and read arcs, called henceforth Contextual P/T nets. The semantics is based on a proper extension of the notion of process to cope with read and inhibitor arcs: we show that most of the properties enjoined by the classical process semantics for P/T nets continue to hold and we substantiate the adequateness of our notion by comparing it with the step semantics.