An all-path reachability (APR) predicate over an object set is a pair of a source set and a target set, which are subsets of the object set. APR predicates have been defined for abstract reduction systems (ARSs) and then extended to logically constrained term rewrite systems (LCTRSs) as pairs of constrained terms that represent sets of terms modeling configurations, states, etc. An APR predicate is said to be partially (or demonically) valid w.r.t. a rewrite system if every finite maximal reduction sequence of the system starting from any element in the source set includes an element in the target set. Partial validity of APR predicates w.r.t. ARSs is defined by means of two inference rules, which can be considered a proof system to construct (possibly infinite) derivation trees for partial validity. On the other hand, a proof system for LCTRSs consists of four inference rules, leaving a gap between the inference rules for ARSs and LCTRSs. In this paper, we revisit the framework for APR analysis and adapt it to verification of not only safety but also liveness properties. To this end, we first reformulate an abstract framework for partial validity w.r.t. ARSs so that there is a one-to-one correspondence between the inference rules for partial validity w.r.t. ARSs and LCTRSs. Secondly, we show how to apply APR analysis to safety verification. Thirdly, to apply APR analysis to liveness verification, we introduce a novel stronger validity of APR predicates, called total validity, which requires not only finite but also infinite execution paths to reach target sets. Finally, for a partially valid APR predicate with a cyclic-proof tree, we show a necessary and sufficient condition for the tree to ensure total validity. The condition implies that if there exists a cyclic-proof tree for an APR predicate, the proof graph of which is acyclic, then the APR predicate is totally valid.

翻译：对象集上的全路径可达性（APR）谓词由源集与目标集构成，二者均为该对象集的子集。APR谓词最初为抽象归约系统（ARS）定义，随后被扩展至逻辑约束项重写系统（LCTRS），以约束项对的形式表示建模配置、状态等的项集合。若系统从源集中任意元素出发的每个有限极大归约序列均包含目标集中的元素，则称该APR谓词相对于该重写系统是部分（或确定性）有效的。ARS中APR谓词的部分有效性通过两条推理规则定义，可将其视为构建部分有效性（可能无限）推导树的证明系统。另一方面，LCTRS的证明系统包含四条推理规则，导致ARS与LCTRS的推理规则之间存在差异。本文重新审视APR分析框架，将其适配至安全性及活性性质的验证。为此，我们首先重构ARS部分有效性的抽象框架，使ARS与LCTRS的部分有效性推理规则形成一一对应关系。其次，阐述如何将APR分析应用于安全性验证。再次，为将APR分析应用于活性验证，我们引入一种更强的新型APR谓词有效性——完全有效性，其要求有限与无限执行路径均需抵达目标集。最后，针对具有循环证明树的部分有效APR谓词，我们给出了该树确保完全有效性的充要条件。该条件表明：若存在某APR谓词的循环证明树，且其证明图是非循环的，则该APR谓词具有完全有效性。