SearcharxivSearch

arXiv subjects

Eike Best

Publications and source records attributed to Eike Best.

4 recordsLinked to original sources

Well-Formed Free-Choice Petri Nets Revisited

The theory of free-choice Petri nets is an established field, initiated in the 1970s by F. Commoner and M. Hack. We revisit well-formed free-choice nets (those admitting markings that are both live and bounded) and provide a new characterisation by introducing semi-T-components. This notion is dual to that of semi-S-components, which in turn correspond to the well-known minimal siphons. By highlighting the symmetry between these dual concepts, we derive the classical coverability theorems for T- and S-components, as well as the duality theorem---stating that a free-choice net is well-formed if and only if its reverse-dual is also well-formed---using highly symmetric arguments.

cs.FL

Persistent Permutability in Choice Petri Nets

Persistence is a strong, global, behavioural property of a Petri net, meaning that no activity can disable a different activity. Persistent permutability is a weaker property, pertaining to individual interleavings of a Petri net and stating that a non-persistent sequence can be permuted into a persistent one. We identify Petri net classes for which persistent permutability already suffices to imply overall persistence. These classes generalise free-choice nets and are related to Petri's concept of ``confusion'', while they are distinguished from each other by diverse restrictions on the choice structure of a net. We prove Ochmanski's conjecture to be correct for these classes.

cs.FL

Analysis of Petri Nets and Transition Systems

This paper describes a stand-alone, no-frills tool supporting the analysis of (labelled) place/transition Petri nets and the synthesis of labelled transition systems into Petri nets. It is implemented as a collection of independent, dedicated algorithms which have been designed to operate modularly, portably, extensibly, and efficiently.

cs.LO

On the Decidability of Non Interference over Unbounded Petri Nets

Non-interference, in transitive or intransitive form, is defined here over unbounded (Place/Transition) Petri nets. The definitions are adaptations of similar, well-accepted definitions introduced earlier in the framework of labelled transition systems. The interpretation of intransitive non-interference which we propose for Petri nets is as follows. A Petri net represents the composition of a controlled and a controller systems, possibly sharing places and transitions. Low transitions represent local actions of the controlled system, high transitions represent local decisions of the controller, and downgrading transitions represent synchronized actions of both components. Intransitive non-interference means the impossibility for the controlled system to follow any local strategy that would force or dodge synchronized actions depending upon the decisions taken by the controller after the last synchronized action. The fact that both language equivalence and bisimulation equivalence are undecidable for unbounded labelled Petri nets might be seen as an indication that non-interference properties based on these equivalences cannot be decided. We prove the opposite, providing results of decidability of non-interference over a representative class of infinite state systems.

cs.CR