Hasse Diagram Generators and Petri Nets

Hasse Diagram Generators and Petri Nets,10.1007/978-3-642-02424-5_12,Mateus De Oliveira Oliveira

Hasse Diagram Generators and Petri Nets  
BibTex | RIS | RefWorks Download
In (LJ06) Lorenz and Juhas 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 lan- guage of any bounded p/t net. We prove as well that it is decidable both whether the (possible infinite) family of partial orders represented by a given Hasse diagram generator is included on 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. When dealing with the development and analysis of concurrent systems, some ques- tions may arise naturally. We may want to know, for example, whether the behavior of a given system subsumes a specified collection of desired scenarios or whether it contains some, out of a collection of undesired scenarios. Given two systems A and B, we could ask as well whether the behavior of A is included in the behavior of B. Finally, we could be interested in synthesizing a system whose behavior minimally includes a given set of scenarios. In this paper, we address these questions under an unifying perspective. We formalize our systems by means of p/t-nets and our scenarios by means of partial orders. In order to finitely represent possible infinite families of partial orders, we in- troduce Hasse diagram generators. With this aim, we define slices as the building blocks of directed acyclic graphs (DAGs). We specify languages over slices by means of what we call slice graphs. Composing the slices on the strings of these languages, we get infinite families of DAGs, the transitive closure of which, gives rise to in- finite families of partial orders. A Hasse diagram generator is a slice graph which generates exclusively transitive reduced DAGs. For this special type of slice graph, each generated DAG is the Hasse diagram of the partial order it induces. Partial orders can be associated to p/t-nets via the notion of Petri net process (GR83,BW00). They may carry two possible semantics. The causal and the execution semantics. Accordingly to the causal semantics, a vertex v is connected to a vertex
Conference: Application and Theory of Petri Nets - APN , pp. 183-203, 2009
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.