Specifying fairness constraints and model checking with non-intensional strategies

Abstract

Strategies are a natural way of specifying constraints in a rewriting-based model. They are often expressed as executable programs in some strategy language that intensionally filter the possible next rewrites. Hence, they cannot capture restrictions of the model involving unbounded delays, like fairness, which are useful in many verification scenarios.

In this paper, we propose a variation to the semantics of the Maude strategy language that allows expressing non-intensional strategies without recursion, in a way amenable for verification. Then we present an LTL model checker for this kind of strategies and discuss the corresponding problem for other logics.