Linear Temporal Logic Specification of Bounded Counter Machines

This article revises the results of work devoted to representing the behavior of a program system as a set of formulae of linear temporal logic (LTL), followed by the use of this representation to verify the satisfiability of the program properties of the system by proving the validity of logical inferences expressed in terms of the LTL. This logic is applied to bounded Minsky counter machines considered as program systems whose behavior must be specified. Earlier on, a special pseudooperator was introduced for referring to previous values of variables used in elementary propositions when working with the LTL temporal logic as a program logic. Even though this pseudooperator is easy to implement in the Cadence SMV verifier when proving the validity of logical LTL inferences, the classical definition of the LTL does not imply its presence. This article will use only binary variables to build the LTL specification for the behavior of a bounded counter machine. Previous values of these variables will be tracked through the appropriate formulas exclusively within the LTL itself.