This paper presents compact regions to synthesize a Petri net from a partial language. We synthesize a Petri net using the theory of regions. Let there be a partial language, every region definition provides an inequality system and a solution of this system is called a region. Every region defines a valid place where a place is valid if it enables every word of the partial language. The new compact region definition relies on compact tokenflows. Compact tokenflows are a very efficient behavioral model for the partial language of Petri nets [3, 4]. Compact regions will lead to faster synthesis algorithms computing smaller Petri nets solving the synthesis problem.
We synthesize a place/transition net (p/t-net) from a partial language, i.e. a set of labeled
partial orders (lpos) using the theory of regions [
A place of a Petri net is valid for a specified language if it enables all words of the language. If we execute the language in the net, the firing rule is always satisfied for every valid place. Fix some type of behavioral model, fix a place, and fix a language: there is an inequality system so that there is a solution of this system if and only if the place is valid. The main idea of region theory is to consider the place as a variable in this inequality system. All at once, we are able to solve the synthesis problem, because we are able to calculate the set of all valid places.
The main steps of a region based synthesis algorithm are: Let there be a language over a set of labels and build a transition for every label. Choose a behavioral model and build the corresponding inequality system to check if an arbitrary place is valid. Consider the place to be a variable and calculate the basis of the solution space. For every solution in the basis add a place (and its arcs) to the set of transitions. The resulting net solves the synthesis problem, because of two arguments: First, every place of the constructed net is valid so that the Petri net enables all words of the language. Second, every additional place (not in the net) is either a linear combination of added places or is not valid. Altogether, the constructed net acts as specified or there is no such net.
In this synthesis algorithm, different behavioral models result in different inequality
systems describing valid places. The run-time, as well as the size of the calculated Petri
net, are mainly determined by the size of this inequality system. In the literature, there
are two different types of regions considering partial order behavior of Petri nets. Both
definitions have plenty disadvantages in most examples and applications. A transition
region [
In practical applications, partial languages have many cuts and many arcs. The
enabled cuts inequality system as well as the tokenflow inequality system is huge.
Therefore, both existing synthesis algorithms have impracticable run-time. Paper [
In this short paper we present a new definition of compact region. This definition
is related to the most recent behavioral model for partial languages presented in [
Let f be a function and B be a subset of its domain A. We write f jB to denote the
restriction of f to B. A function m : A ! N is called a multiset. We write m =
Pa2A m(a) a to denote multiplicities of elements in m. Let m0 : A ! N be another
multiset. We write m m0 if 8a 2 A : m(a) m0(a) holds. We denote the transitive
closure of an acyclic and finite relation by . We denote the skeleton of by .
The skeleton of is the smallest relation / so that / = holds. We model concurrent
or distributed systems by place/transition nets [
Definition 1. A place/transition net (p/t-net) is a tuple (P; T; W ) where P is a finite set of places, T is a finite set of transitions so that P \ T = ; holds, and W : (P T ) [ (T P ) ! N is a multiset of arcs. A marking of (P; T; W ) is a multiset m : P ! N. Let m0 be a marking. We call N = (P; T; W; m0) a marked p/t-net and m0 the initial marking of N .
Let t be a transition. We denote t = Pp2P W (p; t) p the weighted preset of t.
We denote t = Pp2P W (t; p) p the weighted postset of t. A transition t can fire at
marking m if m t holds. If t fires, m changes to m0 = m t + t . The most
famous behavioral model for partial order behavior of Petri nets is a process [
Definition 2. A process net is a tuple O = (C; E; F ) where C is a finite set of conditions, E is a finite set of events so that C \ E = ; holds, and F (C E) [ (E C) is a set of arcs. The graph (C [ E; F ) is acyclic and does not branch at conditions, i.e. every condition has at most one predecessor and at most one successor.
Let N = (P; T; W; m0) be a marked p/t-net. A process is a pair (O; ) where O = (C; E; F ) is a process net and : (C [ E) ! (P [ T ) is a labeling function. (O; ) is a process of N iff the following conditions hold: (1) (C) (2) 8e 2 E : (3) 8e 2 E : (e) = Pp2P jf(e; c) 2 F j (c) = pgj p,
P , (E) T ,
(e) = Pp2P jf(c; e) 2 F j (c) = pgj p, (4) 8p 2 P : jfc 2 Cj8e 2 E : (e; c) 62 F; (c) = pgj = m0(p).
Every process of a Petri net N relates to a labeled partial order. The set of labeled partial orders induced by all processes of N is the partial language of N . Definition 3. A labeled partial order (lpo) is a triple lpo = (V; <; l) where V is a finite set of events, < V V is a transitive and irreflexive relation, and the labeling function l : V ! T assigns a label to every event.
Definition 4. Let K = (C; E; F; ) be a process of a marked p/t-net N . The lpo (E; F jE E ; jE ) is the process lpo of K. Let N be a marked p/t-net and L (N ) be the set of all process lpos of N . L(N ) = f(E; <; l)j(E; <; l) an lpo; (E; ; l) 2 L (N ); <g is the partial language of N .
We specify behavior of a system by example runs. An example run is a set of events with an acyclic relation. Of course, every example run relates to an lpo and we can extend the partial language of Petri nets to example runs.
Definition 5. A triple run = (V; ; l) is an example run if (V; ; l) is a labeled partial order. A finite set of example runs is a specification. Let run = (V; ; l) be an example run. We define run = (V; ; l) the lpo and run = (V; ; l) the compact lpo (cpo) of run.
Definition 6. Let N be a marked p/t-net and S = frun1; : : : ; runng be a specification. We write S L(N ) iff frun1; : : : ; runng L(N ) holds.
Synthesis is to construct a Petri net so that its behavior matches the specification. If there is no such net, we construct a net so that its behavior includes the specification and has minimal additional behavior.
Definition 7. Let S be a specification, the synthesis problem is to compute a marked p/t-net N so that the following conditions hold: S L(N ) and for all marked p/t-nets N 0 : L(N )nL(N 0) 6= ; =) S 6 L(N 0). 3
We synthesize a p/t-net from a partial language applying the theory of regions. We construct a transition for every label of the specification and get a p/t-net without places. The language of this net includes arbitrary behavior. Obviously, we need to add places and arcs to restrict the behavior of such an initial net. Of course, we only add places that do not prohibit the specification. Definition 8. Let S be a specification and N = (P; T; W; m0) be a marked p/t-net. A place p 2 P is called feasible for S iff S L((fpg; T; W j(fpg T )[(T fpg); m0(p))).
Let S be a specification and N = (fpg; T; W; m0) be a marked one-place p/t-net. We call N a feasible p/t-net for S if p is feasible for S.
Corollary 1. Let S be a specification and T be its set of labels. Let f(fp1g; T; W1; m1); : : : ; (fpng; T; Wn; mn)g be a set of feasible p/t-nets and N = (Si pi; T; Si Wi; Si mi) be their union. Of course, every place of N is feasible and S L(N ) holds.
In region theory it is well known that the following theorem holds [
To discover feasible places, we use compact tokenflows as behavioral model [
W (p; l(v)) + W (l(v); p), run is compact valid for N iff there is a compact valid tokenflow for every p 2 P .
Papers [
Theorem 2. The language of a marked p/t-net is its set of compact valid example runs.
At this point we are able to state the main contribution of this short paper. We take advantage of compact tokenflows and define the notion of a compact region. Definition 10. Let S = f(V1; 1; l1); : : : ; (Vn; n; ln)g be a specification, T be its set of labels, and p be a place. We denote i = /i .
A function r : (Si(Vi [ /i) [ (T fpg) [ (fpg T ) [ fpg) ! N is a compact region for S iff 8i 2 N : rjfVi[/ig is compact valid for p in (fpg; T; rj(T fpg)[(fpg T ); r(p)). Theorem 3. Let S be a specification and T be its set of labels. Every compact region r for S defines a feasible p/t-net Nr = (fpg; T; W; m0) and vice versa. Proof. Let r be a compact region. For every example run in S there is a valid compact tokenflow rjfVi[/ig of p in Nr = (fpg; T; rj(T fpg)[(fpg T ); r(p)). Of course, S L(Nr) holds and Nr is feasible.
Let N = (fpg; T; W; m0) be a feasible p/t-net so that S L(Nr) holds. There is a valid compact tokenflow ri for every example run of S. Obviously, the union r = Si ri [ W [ m0 is a compact region.
Altogether, we are able to express the set of all feasible p/t-nets by a single inequality system. In this system there is a variable for every element in the domain of a compact region, i.e. one variable for every event, another variable for every skeleton arc, two variables for every label, and a single variable for the initial marking. The complete inequality system is built from the inequalities defined in Definition 9. According to (i) and (ii) there are two inequalities for every event of the specification. According to (iii) there is another inequality for every example run. The set of positive integer solutions of this inequality system is the set of all feasible nets. We call this inequality system the compact region inequality system. The union of positive integer basis solutions of the compact region inequality system is a solution of the synthesis problem.
The transition region inequality system [