Fundamenta Informaticae

Partially ordered sets (posets), and among them occurrence nets, are a natural formal tool for studying concurrent processes. In a poset, the concurrency relation between elements is explicit. Starting from this relation, and applying standard techniques of lattice theory, one can build a complete lattice whose elements are subsets of the given poset. We study structural properties of such closed subsets, and of the lattice they form. In particular, we show that, if a poset is N-dense, then the lattice of closed subsets is orthomodular. A characterization of K-density, valid for posets, is given on the basis of a relation between lines, or chains, and closed sets. In the case of occurrence nets, we give a characterization of the closed subsets, and define the related notion of “causally closed subset”; a constructive characterization of such subsets is given, which justifies their interpretation as causally closed subprocesses of the occurrence net. We show that, for K-dense occurrence nets, closed subsets and causally closed subsets coincide. By using causally closed subsets, we give another characterization of K-density, related to the algebraicity of the lattice of closed sets.

Consider a Markovian Petri net with race policy. The marking process has a “product form” stationary distribution if the probability of viewing a given marking can be decomposed as the product over places of terms depending only on the local marking. First we observe that the Deficiency Zero Theorem of Feinberg, developed for chemical reaction networks, provides a structural and simple sufficient condition for the existence of a product form. In view of this, we study the classical subclass of free-choice nets. Roughly, we show that the only Petri nets of this class which have a product form are the state machines, which can alternatively be viewed as Jackson networks.

In [18] Lorenz and Juhás raised the question of whether there exists a suitable formalism for the representation of infinite families of partial orders generated by Petri nets. Restricting ourselves to bounded p/t-nets, we propose Hasse diagram generators as an answer. We show that Hasse diagram generators are expressive enough to represent the partial order language of any bounded p/t net. We prove as well that it is decidable both whether the (possibly infinite) family of partial orders represented by a given Hasse diagram generator is included in the partial order language of a given p/t-net and whether their intersection is empty. Based on this decidability result, we prove that the partial order languages of two given Petri nets can be effectively compared with respect to inclusion. Finally we address the synthesis of k-safe p/t-nets from Hasse diagram generators.

In this paper we study decidability of several extensions of P/T nets with name creation and/or replication. In particular, we study how to restrict the models of RN systems (P/T nets extended with replication, for which reachability is undecidable) and ν-RN systems (RN extended with name creation, which are Turing-complete, so that coverability is undecidable), in order to obtain decidability of reachability and coverability, respectively. We prove that if we forbid synchronizations between the different components in a RN system, then reachability is still decidable. Similarly, if we forbid name communication between the different components in a ν-RN system, or restrict communication so that it is allowed only for a given finite set of names, we obtain decidability of coverability. Finally, we consider a polyadic version of ν-PN (P/T nets extended with name creation), that we call pν-PN, in which tokens are tuples of names. We prove that pν-PN are Turing complete, and discuss how the results obtained for ν-RN systems can be translated to them.

A new algorithm for bisimilarity minimization of labelled directed graphs is presented. Its time consumption is O(m log n), where n is the number of states and m is the number of transitions. Unlike earlier algorithms, it meets this bound even if the number of different labels of transitions is not fixed. It is based on refining a partition of states with respect to the labelled transitions. A splitter is a pair consisting of a label and a set in the partition. A transition belongs to a splitter, if and only if it has the same label and its end state is in the set. Earlier algorithms consume lots of time in scanning splitters that have no transitions. The new algorithm avoids this by maintaining also a partition of transitions. To facilitate this, a refinable partition data structure with amortized constant time operations is used. Detailed pseudocode of all nontrivial details is presented. Novel simplifications are applied that both reduce the practical memory consumption and shorten the program code.