On the algorithmics of model checking with unfoldings

In 1981, Nielsen, Plotkin, and Winskel introduced a partial order semantics of Petri nets in terms of what we call today unfoldings, with the goal of giving Petri nets a denotational semantics a la Scott, based on domains. The approach was later extended to many other models of concurrency by different people.

However, this line of research had small impact on the verification community until, in 1992, McMillan proposed unfoldings as a way of attacking the state explosion problem. Since then, model-checking based on unfoldings has established itself as the probably most successful application of partial order semantics.

In this talk I'll introduce unfoldings for communicating sequential systems. I'll show that unfoldings generalise the well-known notion of unwinding of a transition system into a (possibly infinite) tree. I'll then discuss the algorithmic problems involved in using unfoldings as the basis of verification procedures.