Reference:

J. Esparza. Decidability of model-checking for infinite-state concurrent systems. Acta Informatica, 34:85–107, 1997.

Abstract:

We study the decidability of the model checking problem for linear and branching time logics, and two models of concurrent computation, namely Petri nets and Basic Parallel Processes

Suggested BibTeX entry:

@article{Esp97b,
    author = {J. Esparza},
    journal = {Acta Informatica},
    pages = {85--107},
    title = {Decidability of Model-checking for Infinite-state Concurrent Systems},
    volume = {34},
    year = {1997}
}