A unified approach for deciding the existence of certain petri net paths.

*(English)*Zbl 0753.68078An elegant unified approach for deriving complexity results for a number of Petri net problems is developed. First, the author defines a class of Petri net path formulas, each of which consisting of marking variables, variables for transition sequences, terms, transition predicates and marking predicates. It is shown that the satisfiability problem for such formulas is solvable in \({\mathcal O}(2^{d\times n\times\log n})\) space in the size of the Petri net and the formula (i.e., \(n\)), for some constant \(d\). Consequently, the satisfiability problem is EXPSPACE complete. The usefulness of this result is that many Petri net problems, some of which were previously unsolved, can be reduced to the satisfiability problem and hence they can be solvable in EXPSPACE.

Reviewer: F.-L.Tiplea (Iaşi)

##### MSC:

68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |

68Q15 | Complexity classes (hierarchies, relations among complexity classes, etc.) |

Full Text:
DOI

##### References:

[1] | Araki, T.; Kasami, T., Decidable problems on the strong connectivity of Petri net reachability sets, Theoret. comput. sci., 4, 97, (1977) |

[2] | Best, E.; Merceron, A., Frozen tokens and d-continuity: A study in relating system properties to process properties, (), 48-61 |

[3] | Borosh, I.; Treybis, L., Bounds on positive integral solutions of linear Diophantine equations, (), 299 · Zbl 0291.10014 |

[4] | Chan, T., On two way weak counter machines, Math. systems theory, 20, 31, (1987) · Zbl 0629.68055 |

[5] | Crespi-Reghizzi, S.; Mandrioli, D., A decidability theorem for a class of vector addition systems, Inform. process. lett., 3, 78, (1975) · Zbl 0302.68065 |

[6] | Finkel, A., A generalization of the procedure of karp and Miller to well structured transition systems, (), 499-508, to appear |

[7] | Ginzburg, A.; Yoeli, M., Vector addition systems and regular languages, J. comput. system sci., 20, 277, (1980) · Zbl 0446.68043 |

[8] | Hopcroft, J.; Pansiot, J., On the reachability problem for 5-dimensional vector addition systems, Theoret. comput. sci., 8, 135, (1979) · Zbl 0466.68048 |

[9] | Howell, R.; Rosier, L., Completeness results for conflict-free vector replacement systems, J. comput. system sci., 37, 349, (1988) · Zbl 0661.68061 |

[10] | \scHowell, R., and Rosier, L. (1989), personal communication. |

[11] | Howell, R.; Rosier, L.; Yen, H., A taxonomy of fairness and temporal logic problems for Petri nets, Theoret. comput. sci., 82, 341, (1991) · Zbl 0728.68090 |

[12] | Howell, R.; Rosier, L.; Yen, H., Normal and sinkless Petri nets, (), 234-243, to appear · Zbl 0756.68082 |

[13] | Howell, R.; Rosier, L.; Huynh, D.; Yen, H., Some complexity bounds for problems concerning finite and 2-dimensional vector addition systems, Theoret. comput. sci., 46, 107, (1986) · Zbl 0633.68029 |

[14] | Huynh, D., The complexity of the equivalence problem for commutative semigroups and symmetric vector addition systems, (), 405 |

[15] | Jancar, P., Decidability of weak fairness in Petri nets, (), 446 |

[16] | Karp, R.; Miller, R., Parallel program schemata, J. comput. system sci., 3, 147, (1969) · Zbl 0198.32603 |

[17] | Landweber, L.; Robertson, E., Properties of conflict-free and persistent Petri nets, J. assoc. comput. Mach., 25, 352, (1978) · Zbl 0384.68062 |

[18] | Lipton, R., (), Technical Report 62 |

[19] | Mayr, E., Persistence of vector replacement systems is decidable, Acta inform., 15, 309, (1981) · Zbl 0454.68048 |

[20] | Mayr, E., An algorithm for the general Petri net reachability problem, SIAM J. comput., 13, 441, (1984) · Zbl 0563.68057 |

[21] | Muller, H., Decidability of reachability in persistent vector replacement systems, (), 426 |

[22] | Rackoff, C., The covering and boundedness problems for vector addition systems, Theoret. comput. sci., 6, 223, (1978) · Zbl 0368.68054 |

[23] | Ramchandani, C., Analysis of asynchronous concurrent systems by Petri nets, () |

[24] | Rosier, L.; Yen, H., A multiparameter analysis of the boundedness problem for vector addition systems, J. comput. system. sci., 32, 105, (1986) · Zbl 0614.68048 |

[25] | Sistla, A.; German, S., Reasoning with many processes, (), 138 |

[26] | Suzuki, I.; Kasami, T., Three measures for synchronic dependence in Petri nets, Acta inform., 19, 325, (1983) · Zbl 0504.68032 |

[27] | Valk, R.; Jantzen, M., The residue of vector sets with applications to decidability problems in Petri nets, Acta inform., 21, 643, (1985) · Zbl 0545.68051 |

[28] | Valk, R.; Vidal-Naquet, G., Petri nets and regular languages, J. comput. system sci., 23, 299, (1982) · Zbl 0473.68057 |

[29] | Van Leeuwen, J., A partial solution to the reachability problem for vector addition systems, (), 303 |

[30] | Yamasaki, H., On weak persistency of Petri nets, Inform. process. lett., 13, 94, (1981) · Zbl 0473.68058 |

[31] | Yamasaki, H., Normal Petri nets, Theoret. comput. sci., 31, 307, (1984) · Zbl 0562.68047 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.