Option for synthesizing free-choice Petri Net

[NotANumberYang]

Hi,

Thank you very much for developing this tool! We would like to use this tool in our research for Petri Net synthesis. We'd like to know if it is possible to produce free-choice solutions with this tool. If so, which options do we need to use? If not, would it be possible to add this option?

Thanks in advance and looking forward to your reply!

Kind regards, Nan

[psychon]

Hi!

just so that we are on the same page: What is a free-choice Petri net for you? Does https://github.com/CvO-Theory/apt/blob/f705554f6ba2bc96aed911bbddd74a17a86226ac/src/module/uniol/apt/analysis/fc/FreeChoice.java#L32-L33 describe what you mean?

In words: for every pair of transitions, if the sets of places from which they consume token is not disjoint, then they must be equal (and additionally the net must be plain, i.e. no arc weights; this is additionally checked in line 46 in that file).

Looking at https://uol.de/f/2/dept/informatik/thesis_Schlachter.pdf?v=1547718953, I find section 4.1.2 talking about equal-conflict petri nets. Please check definition 4.1.1 on what exactly equal-conflict means. APT seems to call the same property "weighted free choice". If I read all of this correctly, free-choice is the same as equal-conflict plus plain. If so, Petri net synthesis (module "synthesize") with properties equal-conflict,plain should work.

But please double-check this thought process. I might have made "a wrong turn" along the way.

[wytseoortwijn]

Thanks for the detailed reply!

We are actually looking for a slightly more basic variant of free-choice, namely one where for every arc/flow (p,t) it holds that either it is the only outgoing flow out of place p or the only incoming flow into transition t. I believe the definition as described in the code fragment is commonly referred to as extended free-choice. In the thesis it seems to be called weighted free-choice.

Nevertheless, it seems possible to transform extended/weighted free-choice Petri Nets to (ordinary) free-choice Petri Nets by introducing auxiliary join/merge patterns where needed. So in that sense I think the suggested definition would work.

[psychon]

for every arc/flow (p,t) it holds that either it is the only outgoing flow out of place p or the only incoming flow into transition t

Okay, so in pseudo-latex: \forall (p, t)\in F: p\bullet = {t} \lor \bullet t = {p}.

A quick thought would be "that doesn't easily fit into the synthesis framework". "Only one transition consumes from a place" is possible and is called (place-)output-nonbranching (well, that actually is "at most"). The second case is not that easy, I fear.

The problem is that the approach for Petri net synthesis assumes that places are independent and can be added to the Petri net solution without causing problems. But "a transition needs tokens from only one place" breaks this property. Perhaps the introduction in section 4.1.2 explains this problem better, dunno. There, "equal-conflict" works out, because a property of the lts can be used to deduce the necessary presets (events always being enabled together). I don't immediately see whether your definition of free-choice allows something like it and I don't think APT has anything implemented for that.

[wytseoortwijn]

Thanks for explaining that our definition of free-choice doesn't directly befit the synthesis framework. However, I think it might still be possible to synthesize Petri nets that satisfy this property, by using things that are supported.

In particular:

• We are interested in synthesizing elementary nets, i.e., Petri nets that are plain and safe.
• If we synthesize Petri nets that are additionally also equal-conflict, than we get elementary ones satisfying the 'extended/weighted free-choice' property as defined in the code snippet.
• It seems possible to transform such 'extended/weighted free-choice' Petri nets to ones satisfying the more free-choice property we are looking for, by means of some postprocessing (e.g., adding join patterns).

[psychon]

Sure, if that works for you, feel free and good luck!

However, that sounds like a proof sketch for "if a aplain,safe,equal-conflict solution is found, then what you actually want exists". What would you do if APT says no plain,safe,equal-conflict solution exists? Can you be sure that no "solution you actually want" exists?

If that's not an issue for you, then great. I just wanted to point out that this might be a problem.

[wytseoortwijn]

Thanks for pointing that out! I assumed (perhaps wrongly) that a solution would always exist. We will try it out and see if it works for us.

[psychon]

There are surprisingly simple LTS that cannot be synthesised into a Petri net. See e.g. Figure 2.13 and the text on page 30 of https://uol.de/f/2/dept/informatik/erocha18.pdf?v=1551094285. It shows that no Petri net exists that generates just the word "abbaa" and nothing else. The Petri net must always at least also generate the sequence "aba". Since this holds for general Petri nets, this also holds for all classes of nets, e.g. plain,safe,equal-conflict (but such classes likely have simpler examples for unsolvable structures).

Perhaps worth pointing out: We are understanding "Petri net synthesis" as "there is only a single transition that generates a letter a". Put differently: There are no labels on transitions. This in contrast to e.g. the usual understanding of the workflow community.

[psychon]

Perhaps also worth pointing: APT has an overapproximate_synthesize module. This is basically "if the given LTS cannot generated by a Petri net, find the minimally larger LTS that can be solved". "Minimally larger" here means: The LTS / reachability graph can have some of its states merged into one (e.g. imagine two states s1 and s2 with arrows labelled with a in both directions between them; that's not possible in a Petri net and s1,s2 must be merged into a single state) and can have new states added (in the above example: the LTS describing the word "abbaa" would need an extra state to also allow the word "aba").

If you are looking for safe nets (at most one token on a place at any time), this algorithm also works fine when combining this with any other property supported by APT. So, this would be available for your case.

[wytseoortwijn]

The overapproximate_synthesize module sounds potentially useful indeed. Does the synthesized Petri net then still come with equivalence guarantees despite being an overapproximation, like (its reachability graph) being bisimilar to the original input LTS?

The example in Figure 2.13 helps, thanks! In our case the input LTSs have certain properties that might help (not sure). For example, they are strongly connected (i.e., there is a path between any pair of states). I couldn't directly find this in the thesis, but do you happen to know by chance if the situation is different for strongly connected inputs?

[psychon]

Does the synthesized Petri net then still come with equivalence guarantees despite being an overapproximation, like (its reachability graph) being bisimilar to the original input LTS?

For details of the overapproximation, look at chapter 5 of https://uol.de/f/2/dept/informatik/thesis_Schlachter.pdf?v=1547718953 On page 38, figure 5.2 shows an example for parts of the algorithm. Here, state merging happens (the sequences "ab" and "ba" must always reach the same marking in a Petri net, but the example does not have this property). This example is a counter-example to bisimilarity: Previously, the sequence "bac" was not possible, but it becomes possible after state merging.

Adding new states and new outgoing edges (adding "aba" to the "abbaa" example I mentioned above) also directly violates bisimilarity.

So, sorry, but I don't know about any equivalence that is preserved by this operation. (Well, both the original input and the reachability graph of the resulting Petri net have the same "minimal Petri net over-approximation", but I doubt this property is useful. ;-) )

do you happen to know by chance if the situation is different for strongly connected inputs?

The example s0 -a-> s1, s1 -a->s0 (two states forming a circle via a-labelled edges) is strongly connected, but not Petri net solvable (well, up-to isomorphism; obviously this is e.g. solvable up to language equivalence). If firing a changes the marking of the Petri net, firing a again cannot return to the original marking.

For a more complicated example, take the example from figure 5.2 that I mentioned above and make it strongly connected by adding new events e and f that each return from one the final states back to the initial state. I think (but have not checked) that this does not change anything about the over-approximation.

Also, from the top of my head, I don't know about many "completeness" result like you are asking for ("if I my input has properties X, Y, Z, then it is surely PN solvable"). In fact, only one comes to my mind:

Eike Best and Raymond R. Devillers. ‘Characterisation of the State Spaces of Live and Bounded Marked Graph Petri Nets’, LATA 2014, LNCS 8370, http://dx.doi.org/10.1007/978-3-319-04921-2_13

They derive some necessary and sufficient structural conditions for marked graph Petri nets. This algorithm is implemented in APT and is the only implementation that doesn't use an inequality system solver (think: ILP, SMT) or some set-theoretic problem. The conditions are (if you want, I can explain their meaning in detail, but I feel like that's not really what you are interested in right now):

https://github.com/CvO-Theory/apt/blob/f705554f6ba2bc96aed911bbddd74a17a86226ac/src/module/uniol/apt/analysis/synthesize/separation/MarkedGraphSeparation.java#L81-L100

The same authors did similar research in several papers, but, as far as I know, this is the only result where they managed to get completely rid of the inequality systems.

By the way: Over-approximation of regular languages (ordered by inclusion) is mentioned in the thesis in section 5.5. This is possible with APT as well, but I'd have to check how exactly this can be called / used. If "synthesis up to language equivalence" is interesting to you, I can check the details.

[wytseoortwijn]

We are definitely interested in synthesis up to language/trace equivalence. This should be sufficient for us (and also seems the default in e.g. Petrify). We'd be interested in details on that, thanks.

[psychon]

Okay, sure. Time for me to find a computer with Java installed again. :-)

Let's start with synthesis from a regular expression. Why? Because regular expressions are well known.

APT has a module to generate an LTS from a regular expression (well, actually the prefix closure of the regular language since an LTS does not have final states). This is regular_language_to_lts. We can directly pipe its output to the synthesize module and (as I had to check since I wasn't sure about this), this directly offers the option to synthesise upto-language-equivalence. (Otherwise, I would have to... well, do some experiments).

So, here is a Petri net for (ab|ba)c:

$ java -jar apt.jar regular_language_to_lts '(ab|ba)c' - | java -jar apt.jar synthesize upto-language-equivalence,pure,safe,equal-conflict -
success: Yes
.name ""
.type LPN

.places
p0
p1
p2
p3

.transitions
a[label="a"]
b[label="b"]
c[label="c"]

.flows
a: {1*p3} -> {1*p2}
b: {1*p1} -> {1*p0}
c: {1*p2, 1*p0} -> {}

.initial_marking {1*p1, 1*p3}

A safe net cannot count to two, so here is a relative simple example of an unsolvable language:

$ java -jar apt.jar regular_language_to_lts '(aba)*' - | java -jar apt.jar synthesize upto-language-equivalence,pure,safe,equal-conflict -
success: No
failedStateSeparationProblems: []
failedEventStateSeparationProblems: {a=[s1], b=[s0, s2]}

The output here is not terribly useful since we do not know which state s1 really is. The output here is also not too useful, but whatever (it basically just says that "for any Petri net with the requested properties being able to fire the language (aba)*, also (aba)*b, (aba)*aa, and (aba)*abb must be possible, which is just a complicated way of saying that none of the "wrong continuations" can be prevented).

The same input becomes solvable if we remove safe from the requested properties.

(and also seems the default in e.g. Petrify).

Okay, since you know about petrify, one more thing from APT which I find cool: It can convert between file formats. Let's get the LTS for (aba)* in Petrify's file format:

$ java -jar apt.jar regular_language_to_lts '(aba)*' - | java -jar apt.jar lts_convert apt petrify -
.inputs a b 
.state graph
s0 a s1
s1 b s2
s2 a s0
.marking {s0}
.end

And if you want to look at something visually, there is also the option to produce input for graphviz and have graphviz render the result:

$ java -jar apt.jar regular_language_to_lts '(aba)*' - | java -jar apt.jar lts_convert apt dot - | dot -T png -o foo.png
$ java -jar apt.jar regular_language_to_lts '(aba)*' - | java -jar apt.jar synthesize upto-language-equivalence,pure,equal-conflict - - | java -jar apt.jar pn_convert apt dot - | dot -T png -o bar.png

[psychon]

The output here is not terribly useful since we do not know which state s1 really is.

...aaaand I just remembered that APT has a module that does basically the same thing, but provides (hopefully) more readable output:

$ java -jar apt.jar word_synthesize cycle,pure,safe,equal-conflict a,b,a
success: No
separationFailurePoints: [b] a, [a] b, [b] a
stateSeparationFailurePoints: 1 a, 1 b, 1 a

Without cycle it just tries the given word and not w^*. Here is the output for the abbaa example I mentioned above and it indicates that after ab another a must be possible / cannot be prevented:

$ java -jar apt.jar word_synthesize none a,b,b,a,a
success: No
separationFailurePoints: a, b, [a] b, a, a