Local model checking for infinite state spaces

Julian Bradfield, Colin Stirling

Research output: Contribution to journalArticlepeer-review


We present a sound and complete tableau proof system for establishing whether a set of elements of an arbitrary transition system model has a property expressed in (a slight extension of) the modal mu-calculus. The proof system, we believe, offers a very general verification method applicable to a wide range of computational systems.
Original languageEnglish
Pages (from-to)157 - 174
JournalTheoretical Computer Science
Issue number1
Publication statusPublished - 1992

Fingerprint Dive into the research topics of 'Local model checking for infinite state spaces'. Together they form a unique fingerprint.

Cite this