As pointed out in Section 1.4, given a Maude system module, we can distinguish two levels of specification:
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 [11]; we focus on linear temporal logic [53,11], because of its intuitive appeal, widespread use, and well-developed proof methods and decision procedures.