Linear local and global model checking algorithms for a kernal temporal logic language

Finite transition systems play a central role as formal models for reactive and concurrent systems. A promising technique for automatically verifying transition systems is model checking. In the model-theoretic approach one mechanically determines whether a system ts meets a specification f (expressed as a formula of some temporal logic) by checking whether ts is a model for f. The authors present a kernel specification formalism BTL. They discuss efficient (linear-time) global and local model checking algorithms for BTL. The global algorithm will compute all states that satisfy a given formula whereas the local algorithm will only check a formula for one state (typically the initial system state). Both algorithms run in time linear in the size of the transition system and the length of the formula