An all-path reachability (APR, for short) predicate is a pair of a source set and a target set, which are subsets of an object set. APR predicates have been defined for abstract reduction systems (ARSs, for short) and then extended to logically constrained term rewrite systems (LCTRSs, for short) 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, and thus there is a gap between the inference rules for partial validity w.r.t. 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 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, showing how to apply APR analysis to liveness verification.

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