Tag Archives: Difficulty 6

Non-Liveness of Free Choice Petri Nets

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.

Programs With Formally Recursive Procedures

This is the last of the “Program Optimization” problems, and the next section is the last one on “Miscellaneous” problems, which has 19 problems in it.  So, unless some diversion into a problem not in the book happens, we’re on the countdown through the last 20 problems!  The end is in sight!

The problem: Programs with Formally Recursive Procedures.  This is problem PO20 in the Appendix.

The description: Given a set of function definitions and a program that makes a sequence of function calls using those definitions (the paper by Winklmann uses Algol because he wrote it in 1982.  But any language that allows recursion should work).   Are any of the procedures in the program formally recursive?  For our purposes, “formally recursive” means that there exists a chain of calls that has a call to a function higher in the chain (not necessarily a parent, any ancestor will do).

My first instinct was to wonder if this problem was actually undecidable.  It’s not because we will have some fixed # of procedures d, and so any call chain needs to be checked only to depth d+1- if we get that far, we must have a repeat someplace.  If we never get that far, we can back up and check other call chains, eventually checking all of the paths through the call tree exhaustively.  The proof that the problem is in NP is in the paper, but it involves representing the call tree as a DAG so we can use one vertex for two equivalent paths.  Winklmann says that if you do that the number of vertices is “bounded” by the number of procedures in the program (he doesn’t say what that bound is, though).

Example: It’s hard to make a small example that’s not obvious.  How about this:

E(){
  E();
}

D(){
}

C(){
 A();
}

B(){
 D();
}

A(){
 B();
 F
}

main(){
  A()
}

If “F” is replaced by a call to C, the program is formally recursive, because the call chain main->A->C->A has a repeat.  If we replace that F with another call to B the program is not formally recursive because even though recursive functions like E exist (and even though B gets called twice in two different chains), there is no call chain that will start at main and hit E (or anything) more than once.

Reduction: Winklmann uses 3SAT.  So we start with a formula B with m clauses and n variables.  We’ll write some functions:

AssignXi(c1..cm): generates two calls to AssignXi+1. The function has one parameter for each clause.  The first call simulates setting variable Xi to true by passing a “true” value in all parameters that represent clauses that have variable Xi represented positively.  The second call simulates setting variable Xi to false by passing a “true” value in all parameters that represent clauses that have variable Xi returning negatively.  In all other cases, the function passes on the ci parameter it was given.

AssignXn(c1..cm): once we reach the end of the variables, we have to stop.  This function calls the “Check” function we’ll be defining in a minute twice, once reflecting setting variable Xn to true, one reflecting setting it to false.

Truej(cj+1..cm):There is one “true” function for each clause, each one has a parameter for all clauses with larger numbers. The paper writes this function a little weirdly, but I think a good definition is:

if(cj+1 is true){
Truej+1(cj+2..cm);
else
Falsej+1(cj+2...cm);
}

So, as long as the parameters are true, we’ll continue calling down through the  true functions to the end.  The last True function is what will make us formally recursive:

Truem(): Calls Assign1(False, False, ...False). Our main program will begin with a call to Assign1 with these exact parameters, so if we can get here, we will have found our recursive call.

The False functions end a call chain:

Falsej(cj+1..cm){
// do nothing
}

The Check function’s job is to start the appropriate call to True or False:

Check(c1..cm){
if(c1 is true)
True1(c2..cm);
else
False1(c2..cm);
}

Our main program is just a call to Assign1(False, False..False).  It’ll go through all of the various AssignXifuntions trying to assign variables (and thus clauses) to true. Each assignment will be checked, and each check will either hit a False function (meaning a clause wasn’t satisfied, and so we will backtrack and try an alternate assignment) or the final True function, which will generate our recursive call.  So this program has a recursive call chain if and only if the formula was satisfiable.

Notice that while the run of this program might take exponential time, that’s ok because reductions are concerned with the time it takes to create the new problem instance, and there are “just” 2m+n+1 functions to create.

Difficulty: 6.  This is a neat problem and reduction- I think the “write a backtracking program to try all combinations” is pretty gettable.  The hard part is the check and true/false functions at the end.  We can’t really use loops because loops make programs undecidable (you can’t show the problem is in NP by going down d+1 calls if you might have an infinite loop someplace and won’t get through all of those calls).  So we have to build a chain of recursive calls instead, with dead-ends to force the backtracking.

Protected: Inequivalence of Simple Functions

This content is password protected. To view it please enter your password below:

Protected: Inequivalence of Programs with Arrays, Inequivalence of Programs with Assignments

This content is password protected. To view it please enter your password below:

Protected: Ensemble Computation

This content is password protected. To view it please enter your password below:

Protected: Code Generation With Unlimited Registers

This content is password protected. To view it please enter your password below:

Protected: Code Generation on a One-Register Machine

This content is password protected. To view it please enter your password below:

Protected: ETOL Language Membership

This content is password protected. To view it please enter your password below:

Protected: Structural Inequivalence for Linear Grammars

This content is password protected. To view it please enter your password below:

Protected: Two-Way Finite State Automaton Non-Emptiness

This content is password protected. To view it please enter your password below: