Reference:

J. Esparza. Decidability and complexity of Petri net problems – an introduction. In G. Rozenberg and W. Reisig, editors, Lectures on Petri Nets I: Basic Models. Advances in Petri Nets, number 1491 in Lecture Notes in Computer Science, pages 374–428, 1998. Section 8 presents a logic for Petri nets, due to Yen, having an EXPSPACE model-checking problem. Unfortunately, Yen's paper has a mistake. For a description of the mistake and a partial correction see "On Yen's Path Logic for Petri Nets" by Faouzi and Habermehl, Workshop on Reachability Problems 2009.

Suggested BibTeX entry:

@inproceedings{Esp98a,
    author = {J. Esparza},
    booktitle = {Lectures on {P}etri Nets I: Basic Models. Advances in Petri Nets},
    editor = {G.~Rozenberg and W.~Reisig},
    note = {Section 8 presents a logic for Petri nets, due to Yen, having an EXPSPACE model-checking problem. Unfortunately, Yen's paper has a mistake. For a description of the mistake and a partial correction see "On Yen's Path Logic for Petri Nets" by Faouzi and Habermehl, Workshop on Reachability Problems 2009.},
    number = {1491},
    pages = {374--428},
    series = {Lecture Notes in Computer Science},
    title = {Decidability and Complexity of {P}etri Net Problems -- an Introduction},
    year = {1998}
}