Semantics Club 02 11 2001

An unfolding approach to LTL Model Checking

Javier Esparza

Abstract

In an interleaving semantics, the automatic verification of finite state systems suffers from the explosion of states caused by the many possible permutations of concurrent events. In this talk I show how to use unfoldings, a partial order semantics of concurrent systems introduced by Nielsen, Plotkin, and Winskel in 1981, to avoid this problem.