Improved verification of linear-time properties within fairness: weakly continuation-closed behaviour abstractions computed from trace reductions

摘要

The satisfaction of linear-time temporal properties within fairness introduces an implicit fairness constraint to the verification process. To be applied to practical verification tasks, weakly continuation-closed abstractions preserve properties satisfied within fairness. Being defined on the complete behaviour of a distributed system, weakly continuation-closed abstractions require, in principle, an exhaustive state space construction prior to abstraction. Constructing the state space of a practically relevant specification exhaustively, however, is usually not feasible. Based on the notion of traces, i.e. certain equivalence classes of behaviours, trace reductions are defined in this paper. Trace reduction is a particular partial-order reduction based on the persistent-set selective search technique. It is shown that a trace reduction can be used on behalf of the complete behaviour of a distributed system in order to compute abstractions as well as to check whether the abstractions are weakly continuation closed. Thus, trace reductions allow one, in the discussed context, to overcome the requirement of an exhaustive state-space construction prior to abstraction.