The Recursive Equivalence of the Reachability Problem and the Liveness Problem for Petri Nets and Vector Addition Systems,

摘要

In 1967, R. Karp and R. Miller introduced a formalism called Vector Addition Systems to discuss decidability questions about their Parallel Program Schemata. That same year A. W. Holt introduced Petri Nets to model concurrent behavior in systems. Both formalisms have been used to model and analyze the structural behavior to asychronous and parallel systems. In 1972also, M. Rabin presented the Unsolvability of the Inclusion Problem for Reachability Sets in Vector Addition Systems in a talk at MIT. The Liveness Problem is the problem of deciding whether a system could possibly ever reach a deadlocked state from the initial state. The Inclusion Problem,which Rabin has shown to be undecidable is the question of whether one system's set of possible configurations include all possible configurations of another,which is related to whether one system can simulate another. This research has confirmed Keller's conjecture,and has also shown reducibility the other way,from which follows the main Theorem.