Decidability of model checking for infinite-state concurrent systems (Q1920224)

We study the model checking problem for linear and branching logics and two models of concurrent computation: Petri nets and basic parallel processes. While Petri nets are a rather powerful model, which can be used to represent and analyse a large variety of systems, basic parallel processes are rather limited. The main results of the paper are that the model checking problem is decidable for an expressive linear time logic (the linear time mu-calculus) and Petri nets, but undecidable for a weak branching time logic (a fragment of UB) and basic parallel processes.