LTL Model Checking

As pointed out in Section 1.4, given a Maude system module, we can distinguish two levels of specification:

a

system specification

level, provided by the rewrite theory specified by that system module which defines the behavior of the system, and

a

property specification

level, given by some property (or properties)

φ

that we want to state and prove about our module.

This chapter discusses how a specific property specification logic,

linear temporal logic

(LTL), and a decision procedure for it,

model checking

, can be used to prove properties when the set of states reachable from an initial state in a system module is finite. It also explains how this is supported in Maude by its

MODEL-CHECKER

module, and other related modules, including the

SAT-SOLVER

module that can be used to check both satisfiability of an LTL formula and LTL tautologies. These modules are found in the file

model-checker.maude

.

Temporal logic allows specification of properties such as safety properties (ensuring that something bad never happens) and liveness properties (ensuring that something good eventually happens). These properties are related to the

infinite behavior

of a system. There are different temporal logics [54]; we focus on linear temporal logic [194, 54], because of its intuitive appeal, widespread use, and well-developed proof methods and decision procedures.