Abstract Framework for All-Path Reachability Analysis

TL;DR

The paper addresses all-path reachability analysis for concurrent systems modeled as ARSs and LCTRSs, with a focus on both safety and liveness verification. It reformulates the APR framework so ARS and LCTRS proof rules correspond one-to-one and introduces total validity to handle infinite execution paths, enabling liveness reasoning. A cyclic-proof approach for ARSs is developed, including buds/companions and proof graphs, with an acyclic proof graph offering a sufficient condition for total validity. As a practical outcome, safety properties are reduced to APR predicates, providing a unified method for verifying runtime-errors alongside liveness properties in APR-based models.

Abstract

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.

Figures (5)

• Figure 1: Inference rules of $\mathsf{DVP}$CL18 for partial validity of APR predicates w.r.t. an an ARS $\mathcal{A}=(A,\to_{\mathcal{A}})$, where $\partial(P) = \{ t' \in A \mid \exists t \in P.\ t \to_{\mathcal{A}} t' \}$.
• Figure 2: Inference rules of $\mathsf{DCC}$CL18 for partial validity of APR predicates (in $G$) of an LCTRS $\mathcal{R}$.
• Figure 3: Rules of $\mathsf{DVP}_+$ for proving partial validity of APR predicates of an ARS $\mathcal{A}$.
• Figure 4: An APR pre-proof and its proof graph for the APR predicate $\{\mathsf{a}\} \Rightarrow \{\mathsf{c},\mathsf{d}\}$.
• Figure 5: An APR pre-proof for $\{\mathsf{a}\} \Rightarrow \{\mathsf{c}\}$, which is an APR disproof

Theorems & Definitions (21)

• Definition 1: execution path CL18
• Definition 2: APR predicate CL18
• Definition 3: partial validity CL18
• Proposition 4
• Example 5
• Definition 6: $\mathsf{DVP}_+$
• Proposition 6
• Theorem 7
• Proposition 8
• Definition 9: $\mathsf{DVP}_\bot$