We look in detail at the structural liveness problem (SLP) for subclasses of Petri nets, namely immediate observation nets (IO nets) and their generalized variant called branching immediate multi-observation nets (BIMO nets), that were recently introduced by Esparza, Raskin, and Weil-Kennedy. We show that SLP is PSPACE-hard for IO nets and in PSPACE for BIMO nets. In particular, we discuss the (small) bounds on the token numbers in net places that are decisive for a marking to be (non)live.
2
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
Petri nets are a popular formalism for modeling and analyzing distributed systems. Tokens in Petri net models can represent the control flow state or resources produced/consumed by transition firings. We define a resource as a part (a submultiset) of Petri net markings and call two resources equivalent when replacing one of them with another in any marking does not change the observable Petri net behavior. We consider resource similarity and resource bisimilarity, two congruent restrictions of bisimulation equivalence on Petri net markings. Previously it was proved that resource similarity (the largest congruence included in bisimulation equivalence) is undecidable. Here we present an algorithm for checking resource bisimilarity, thereby proving that this relation (the largest congruence included in bisimulation equivalence that is a bisimulation) is decidable. We also give an example of two resources in a Petri net that are similar but not bisimilar.
3
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
The boundedness problem is a well-known exponential-space complete problem for vector addition systems with states (or Petri nets); it asks if the reachability set (for a given initial configuration) is finite. Here we consider a dual problem, the co-finiteness problem that asks if the complement of the reachability set is finite; by restricting the question we get the co-emptiness (or universality) problem that asks if all configurations are reachable. We show that both the co-finiteness problem and the co-emptiness problem are exponential-space complete. While the lower bounds are obtained by a straightforward reduction from coverability, getting the upper bounds is more involved; in particular we use the bounds derived for reversible reachability by Leroux (2013). The studied problems were motivated by a result for structural liveness of Petri nets; this problem was shown decidable by Jančar (2017), without clarifying its complexity. The structural liveness problem is tightly related to a generalization of the co-emptiness problem, where the sets of initial configurations are (possibly infinite) downward closed sets instead of just singletons. We formulate the problems even more generally, for semilinear sets of initial configurations; in this case we show that the co-emptiness problem is decidable (without giving an upper complexity bound), and we formulate a conjecture under which the co-finiteness problem is also decidable.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.