English

Abstract Processes in the Absence of Conflicts in General Place/Transition Systems

Logic in Computer Science 2022-07-12 v1

Abstract

Goltz and Reisig generalised Petri's concept of processes of one-safe Petri nets to general nets where places carry multiple tokens. BD-processes are equivalence classes of Goltz-Reisig processes connected through the swapping transformation of Best and Devillers; they can be considered as an alternative representation of runs of nets. Here we present an order respecting bijection between the BD-processes and the FS-processes of a countable net, the latter being defined -- in an analogous way -- as equivalence classes of firing sequences. Using this, we show that a countable net without binary conflicts has a (unique) largest BD-process.

Keywords

Cite

@article{arxiv.2207.04362,
  title  = {Abstract Processes in the Absence of Conflicts in General Place/Transition Systems},
  author = {Rob van Glabbeek and Ursula Goltz and Jens-Wolfhard Schicke-Uffmann},
  journal= {arXiv preprint arXiv:2207.04362},
  year   = {2022}
}

Comments

The above result appeared already in our technical report arXiv:2103.00729, although formulated and proven differently, since there we didn't have the preorder $\sqsubseteq_1^\infty$, introduced in arXiv:2103.01490. Our revised proofs are conceptually simpler, as they avoid the auxiliary concepts of BD-runs and FS-runs