Open AccessA Note on Model Cheking the Modal v-calculus
Author(s) -
Glynn Winskel
Publication year - 1990
Publication title -
daimi pb
Language(s) - English
Resource type - Journals
eISSN - 2245-9316
pISSN - 0105-8517
DOI - 10.7146/dpb.v18i279.6656
Subject(s) - correctness , modal , calculus (dental) , assertion , model checking , mathematics , computer science , algorithm , programming language , medicine , chemistry , dentistry , polymer chemistry
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.