On Yen's Path Logic for Petri Nets

In [13], Yen defines a class of formulas for paths in Petri nets and claims that its satisfiability problem is EXPSPACE-complete. In this paper, we show that in fact the satisfiability problem for this class of formulas is as hard as the reachability problem for Petri nets. Moreover, we salvage almost all of Yen’s results by defining a fragment of this class of formulas for which the satisfiability problem is EXPSPACE-complete by adapting his proof.

• Type: Conference
• Year: 2009
• Where: RP
• Authors: Mohamed Faouzi Atig, Peter Habermehl
• Keywords: Control Systems, Formulas, Petri Nets, RP 2009, Satisfiability Problem