Portal de Periódicos da CAPES

On Yen’s Path Logic for Petri Nets

2009; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-642-04420-5_7

1611-3349

Mohamed Faouzi Atig, Peter Habermehl,

Logic, Reasoning, and Knowledge

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.