The next couple of problems talk about “Petri Nets”, which I hadn’t heard of before. I found a decent explanation here, and the Wikipedia article also has a good explanation, though I found it pretty dense. I also took some definitions from a nicely explained paper by Murata.
The problem: Non-liveness of Free Choice Petri Nets. This is problem MS3 in the appendix.
The description: Given a Petri Net, with the “free choice” property (which means every “place” node either goes to one transition or has input from 1 transition), is it not live? A Petri Net is live if, after any sequence of transitions, each transition remains potentially firable by some future sequence of transitions. So we are asking- is there a set of transitions that will create a situation where at least one transition will no longer be able to fire?
Example: Here is a live Petri Net from Murata’s paper:
Notice how whatever sequence of transitions we do from the initial state, we will be able to “reset” the net and get to any transition.
Notice that this net is also not “Free choice”, because place P1 gets inputs from 2 transitions, and also feeds into 2 transitions (The 10¢ and 25¢ places also violate this property)
Here is a non-live one from the same paper:
This is not live because even though every transition is reachable from the start state, if we choose the t1 transition to start, we will not be able to ever fire t4. (In fact, we won’t be able to fire any other transitions).
Also notice that this second Net does have the Free choice property, since each circle has either indegree or outdegree 1 (or both).
Reduction: The reduction is in the paper by Jones, Landweber, and Lien, and it reduces from CNF-SAT. So we start with a formula that has n variables and k clauses. The Petri Net we build has three places for each variable xi:
- A place xi associated with the positive setting of the variable
- A place ~xi associated with the negative setting of the variable,
- A third place Ai, which will be used to link the two.
For each literal li in clause Cj, we have a place associated with the negation of the literal in the clause (the setting that does not make the clause true). So, for example, if xi was in clause Cj, we’d have a place (~xi, Cj)
We will also have one last place “F”, which will mean the formula is not true (because some clause was not true)
Our net will have 1 token for each variable, starting in the “A” places, one for each variable.
We will have transitions between:
- Each Ai and its xi and ~xi
- Each xi and all of the places corresponding to literals that hold the negation of that variable. So a transition between xi and places like (~xi, Cj)
- A transition straight to F for each clause if all of the “literal” places for a clause have tokens.
- A transition from F to each Ai
The idea here is that the places for literals will gather tokens if their variables are set in a way to not make the clause true. If none of the literals in the clause are set to make the clause true, then the clause is false, all of their places will have a token, and F will fire. F will then enable the firing of all of the A places, and we will go around again.
So, let’s suppose the formula is satisfiable. The tokens start in each Ai, which has transitions to xi and ~xi. Pick the transition that corresponds to how we set xi in the satisfying assignment of the formula. This will enable some transitions in clauses with xi in it to fire- the literals that have the opposite settings of the variable. But since every clause is satisfiable, there will not be enough firings to enable the transition to F to fire, and the net will be dead (no more firings will happen after those).
On the other hand, if the formula is not satisfiable, then all assignments of variables make at least one clause false. So no matter how we decide to make the Ai transition go (to the xi or to the ~xi), some clause will not be satisfied, and that clause will be able to fire its transition to F. Firing F puts a token at each Ai, enabling all transitions to start again.
Difficulty: 6. Obviously, this only works if you’ve discussed Petri Nets previously, since learning about them is a separate involved discussion. But outside of that, the idea of a transition firing on a clause being false is a pretty cool one, and makes sense, because we are looking for non- liveliness, so a Satisfiable formula means we want dead transitions.
Also, I want to commend the Jones, Landweber, and Lien paper for having a very nice example explaining how a formula turns into a Petri Net complete with transitions and explanations working through how what fires and why. I don’t get that in every paper, and it was nice of them to think about people like me coming along 45 years later.