Simulating Liveness by Reduction Strategies

We define a general framework to handle liveness and related properties by reduction strategies in abstract reduction and term rewriting. Classically, reduction strategies in rewriting are used to simulate the evaluation process in programming languages. The aim of our work is to use reduction strategies to also study liveness questions which are of high importance in practice (e.g., in protocol verification for distributed processes). In particular, we show how the problem of verifying liveness is related to termination of term rewrite systems (TRSs). Using our results, techniques for proving termination of TRSs can be used to verify liveness properties