A Note on Model Cheking the Modal v-calculus

Abstract

This note presents a straightforward algorithm for checking whether or not a state of a labelled transition system satisfies an assertion in the modal upsilon-calculus and nu-calculus. The algorithm improves on those of Larsen, and Stirling and Walker in that its presentation lays bare the mechanism behind ''local model checking'', and leads to a streamlined proof of the correctness and termination of the model-checking algorithm.