The Tableau System

Abstract

In subsection 1.2.5 we described briefly the model checking technique used by Emerson, Clarke et al. An important feature of this technique is that it is ‘global’, that is, it constructs the entire state graph of the system and then traverses it—and in the original version [CES86] the system was traversed once for every subformula of the formula being checked. Clearly this causes difficulties as soon as systems become large, let alone infinite; but since one is more usually interested in whether a particular state satisfies a formula than whether such a state exists, this global traversal may not even be necessary, since the truth of a particular property at a particular state may depend only on a small neighbourhood of that state. Thus there are good reasons to look at ‘local’ model-checking, where checking that a property holds at a state is done by considering only the local behaviour of the system, so far as necessary.