Tag Archives: Linear Bounded Automaton Acceptance

Reachability for 1-Conservative Petri Nets

As promised, here is the next problem, also using Petri nets.  I’m not 100% convinced that my definition of “1-Conservative” is accurate, but it seems to work for this reduction.

The problem: Reachability for 1-Conservative Petri nets.  This is problem MS4 in the appendix.

The description: A “1-Conservative” Petri net has each transition preserve the number of tokens on each side of the transition, and has at most 1 token per edge.  Given such a Petri net and a state M, is there a sequence of transitions that can reach M from the starting state?

Example: I had a hard time finding a non-trivial example of a 1-conservative network.  But maybe that’s ok.  Here’s another figure from the Murata paper:

There are no tokens in this picture.  But notice that if we start with no tokens, no state with tokens is reachable.  If we start with a token in the left state, then both 1-token configurations are reachable, but we won’t be able to reach a configuration with 0 tokens or 2 tokens in it.

Reduction: This is Theorem 3.1 in the Jones, Landweber, and Lien paper.  The reduction is from Linear Bounded Automaton Acceptance.

So we start with a LBA M, with p tape symbols, and m states.  It has an input string $x1x2..xn$.  Our task is to build a 1-Conservative Petri Net.

The first set of places in the Petri net will be represented by Aij,  0 <= i <= n+1, 1 <= j <= p.  This will represent the tape.  Aij will have a token iff space i of the tape has symbol j.

We will also have places labeled Qij, 0 <= i <= n+1, 1 <= j <= m.  This will simulate the states.  Qij will have a token iff the head is over space i of the tape while the machine is in state j.

We’ll also have 2 special places C and D.  Tokens start in all of the Aij places corresponding to the input string of the tape, and in Q11 (the machine starts in state 1 over cell 1 of the tape).

The transitions in the net are based on the transitions in the machine.  If we have a transition from state qs and symbol at to state qr, writing a symbol al we add a transition Qis + Ait -> Qjr + Ail for all i.  “j” in the destination is either i, i+1, or i-1, depending on if the head stays, moves right, or moves left.

If we are in a final state qs, we add a transition Qis->C for all i.

We also add the transition C+Aij -> C+D.

Note that all transitions have 1 token per edge and preserve the number of tokens, so this is a 1-Conservative Petri net.

Our destination state is:

  • 1 token in C
  • N tokens in D
  • 1 token in each Ai1

Since all of these transitions simulate the movement in the LBA, if the LBA accepts the string, we follow all of the transitions to eventually put the token in C.  This allows us to do the last transition to put the tokens in D.

In the other direction, if we can reach the desired state, we must have put a token in C.  To get there, we must have gotten to a final state qf.  Thus, the LBA must have accepted the string (by following the transitions we took in the Petri Net to get to that qf state).

Difficulty:  7.  I like how they can represent all combinations of tape symbols and locations as places.  I’m a little worried because it looks like this assumes you’ll never go beyond the end of the input string, where I thought an LBA was allowed to use a linear multiple of the input string’s size.  Is there some kind of equivalence proof that says an LBA can only need its own input string’s space exactly?

Protected: Inequivalence of Finite Memory Programs

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

Protected: Context-Sensitive Language Membership

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

Protected: Linear Space Acceptance

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

Protected: Non-Erasing Stack Automaton Acceptance

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

Protected: Quasi-Realtime Automaton Acceptance, Quasi-Realtime Language Membership

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:

Protected: Safety of File Protection Systems

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

Protected: Linear Bounded Automaton Acceptance

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