Hierarchy of persistence with respect to the length of action's disability

TL;DR

This paper introduces a hierarchy of persistence notions in concurrency theory, analyzing how actions disable each other over time, and proves their decidability and computability properties.

Contribution

It defines a new precise notion, e/l-k-persistence, and explores its hierarchy, proving key properties and decision problems are decidable.

Findings

The hierarchy of e/l-k persistencies is well-structured.

Disabling actions cannot be postponed indefinitely.

Decision problems for e/l-k persistencies are decidable.

Abstract

The notion of persistence, based on the rule "no action can disable another one" is one of the classical notions in concurrency theory. It is also one of the issues discussed in the Petri net theory. We recall two ways of generalization of this notion: the first is "no action can kill another one" (called l/l-persistence) and the second "no action can kill another enabled one" (called the delayed persistence, or shortly e/l-persistence). Afterwards we introduce a more precise notion, called e/l-k-persistence, in which one action disables another one for no longer than a specified number k of single sequential steps. Then we consider an infinite hie\-rarchy of such e/l-k persistencies. We prove that if an action is disabled, and not killed, by another one, it can not be postponed indefinitely. Afterwards, we investigate the set of markings in which two actions are enabled simultaneously, and also the set of reachable markings with that feature. We show that the minimum of the latter is finite and effectively computable. Finally we deal with decision problems about e/l-k persistencies. We show that all the kinds of e/l-k persistencies are decidable with respect to steps, markings and nets.