Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis

• The listed research topics are infinite-state model checking, SMT, backward reachability, and invariant synthesis.Source: LOGICAL METHODSl IN COMPUTER SCIENCE · p. 1
• The paper extends with all proofs and adapts materials from to make the account self-contained.Source: LOGICAL METHODSl IN COMPUTER SCIENCE · p. 1
• The publication information gives DOI 10.2168/LMCS-6 (4:10) 2010.Source: LOGICAL METHODSl IN COMPUTER SCIENCE · p. 1

1. Introduction

• Backward reachability repeatedly computes symbolic pre-images of unsafe states and halts on an initial-state intersection or a fix-point.For some infinite-state system classes, a well-quasi-ordering establishes termination and decidability of safety checking.Source: §1 · p. 3

1.1. Array-based systems and symbolic backward reachability.

• Array-based systems declaratively specify topology and data through theories, while first-order formulae represent sets of states for symbolic backward reachability.The approach requires expressive formula classes closed under pre-image computation, with safety and fix-point checks reducible to decidable logical problems.Source: §1.1 · p. 3
• Sufficient theory conditions yield termination, with well-quasi-orders derived uniformly from substructures and embeddings.This framework supports decidability results for the safety problems of the covered system classes.Source: §1.1 · p. 4

1.2. Symbolic backward reachability and Invariant synthesis.

• Interleaving invariant synthesis with pre-image computation can eagerly prune search, and the synthesis method finds an invariant whenever one exists under suitable hypotheses.The well-quasi-ordering finitely characterizes candidate invariants; the hypotheses hold for important classes including mutual-exclusion algorithms and cache-coherence protocols.Source: §1.2 · p. 5

How to read the paper.

• The paper presents symbolic and semantic reading tracks, covering mechanization and experiments on one track and termination and synthesis proofs on the other.Source: How to read the paper · p. 6

2. Formal Preliminaries

• The preliminaries adopt standard first-order syntax and semantics, including signatures, terms, formulae, structures, satisfiability, and validity.Source: §2 · p. 7
• A theory is a signature paired with a class of structures, and SMT(T) asks whether quantifier-free formulae are satisfiable in that class.Quantifier elimination means computing an equivalent quantifier-free formula; linear and real arithmetic, acyclic lists, and enumerated data-type theories are cited as examples.Source: §2 · p. 7
• Local finiteness means finitely many representative terms suffice for terms over any finite variable set, with effective computability required here.Any theory with a relational or quasi-relational signature is locally finite.Source: §2 · p. 7
• Enumerated data-type theories have a single finite model whose elements are named by constants, and can model process control locations.Source: §2 · p. 7

2.1. Case Defined Functions.

• A case-defined extension adds functions whose values are selected by a finite partition, and its formulae can be translated back into the original theory.The extension is conservative for satisfiability in the original signature.Source: §2.1 · pp. 7–8

2.2. Embeddings.

• Embeddings are injective homomorphisms that preserve and reflect predicates; substructures inherit operations and relations through inclusion.Universal sentences persist through substructures, while existential sentences persist through superstructures.Source: §2.2 · p. 8

2.3. A many-sorted framework.

• The many-sorted framework combines index and element theories with arrays interpreted as total functions from indexes to elements.The notation specifies variable sorts and uses a[i] for the tuple of array values at index tuple i.Source: §2.3 · p. 9

3.1. Array-based Systems.

• Following, array-based systems use a universally quantified initial condition and guarded transitions that update the array through a functional form.Each transition has an existentially chosen index, a local guard, and a global component defining the next array values.Source: §3 · p. 9, §3.1 · p. 9

3.2. Backward Reachable States.

• Backward reachability iteratively computes pre-images of unsafe states, checking at each step whether the initial states intersect them or a fix-point has been reached.At a safety fix-point, the accumulated formula describes the states backward reachable from the unsafe states.Source: §3.2 · p. 11
• A major bottleneck is that each pre-image can enlarge the existential-variable prefix, making safety and fix-point checks computationally expensive.The passage identifies handling quantified variables in ∃I-formulas as the source of this growth.Source: §3.2 · p. 12
• Safety and fix-point checks reduce to ∃A,I∀I-sentences, whose satisfiability is decidable when the index theory is locally finite and substructure-closed and both component SMT problems are decidable.Under these hypotheses, satisfiability is equivalent to satisfiability in a finite-index model.Source: §3.2 · p. 12
• The satisfiability procedure skolemizes array and index variables, instantiates universally quantified indices with representative terms, and passes purified constraints to the component theory solvers.Heuristics are needed to control the potential combinatorial explosion from index instantiation.Source: §3.2 · pp. 12–13

3.3. Tableaux-like Implementation of Backward Reachability.

• A tableaux-like implementation rewrites existential formulas into disjunctions of primitive differentiated formulas and expands nodes by applying pre-image rules.A node’s label represents backward reachable states, and the disjunction of labels represents the reachable-state formulas accumulated by the basic procedure.Source: §3.3 · pp. 13–14
• Tableau branches close when a node is unsatisfiable, when the safety test finds an error trace, or when the fix-point test shows its states are covered by earlier nodes.These tests are effective under the decidability result for the relevant formulae.Source: §3.3 · p. 14
• The framework’s fully declarative representation includes system topology, and MCMT usually visits fewer tableau nodes than approaches that encode topology in an ad hoc data structure.Source: §3.3 · p. 15
• MCMT solves the problem in about 0.02 seconds with 7 generated nodes, while PFS takes about 4 minutes and generates thousands of constraints.MCMT can represent partial information about process positions; PFS needs to specify the relative positions of all involved processes.Source: §3.3 · p. 15
• Coupled with appropriate heuristics, MCMT’s fully declarative approach should enable verification of systems with more complex topologies than other tools can handle.Source: §3.3 · p. 15

4.1. Configurations.

• A configuration pairs an array with a finite-index model, providing the state objects ordered in the termination analysis.The paper associates index- and element-structure views with each configuration.Source: §4.1 · p. 16

4.2. Undecidability of the safety problem.

• Safety for array-based systems is undecidable in general, even when the element theory is locally finite.The proof reduces from the reachability problem of Minsky machines.Source: §4.2 · p. 16

4.3. Decidability of the safety problem: sufficient conditions.

• The paper represents configurations through embeddings between their index and element structures, defining the pre-order used in its termination analysis.Finitely generated upsets of configurations can be represented by existential array formulas under suitable assumptions.Source: §4.3 · p. 16
• Under local finiteness of the element theory, backward reachability terminates for a safe formula exactly when its backward-reachable configurations form a finitely generated upset.The reachable set is an upset but need not be finitely generated, even if it is a union of finitely generated upsets.Source: §4.3 · p. 19
• If the configuration pre-order is a well-quasi-ordering, backward reachability always terminates.In a well-quasi-order, every upset is finitely generated.Source: §4.3 · pp. 19–20
• Some decidable classes still have very poor computational behavior, with only a non-primitive-recursive lower bound known.Source: §4.3 · p. 20
• Examples apply standard well-quasi-ordering results to finite-data systems, lossy channel systems, and systems with rational-valued elements.The cited results include Dickson’s, Higman’s, and Kruskal’s theorems.Source: §4.3 · p. 20

5.1. Safety Invariants.

• A safety invariant can be checked fully automatically, and if one exists for the unsafe formula, the system is safe with respect to it.Checking the invariant conditions reduces to a decidable satisfiability problem.Source: §5.1 · p. 21
• When BReach terminates with safe, the complement of its returned reachable-state formula is a safety invariant; the converse fails, as an example shows divergence despite an invariant.For that example, an augmented safety problem yields an invariant, and mcmt can find it automatically when invariant synthesis is enabled.Source: §5.1 · pp. 21–23

5.2. Invariant Synthesis.

• If TE is locally finite and a safety invariant exists, finitely many configurations sub-reachable from U suffice to form a disjunction whose complement is also a safety invariant.The theorem constructs this invariant from configurations in the bases of the relevant formulae.Source: §5.2 · p. 25
• The synthesis theorem can find a finitely representable superset of backward-reachable states whose complement is an invariant, even when the backward-reachable set itself is not finitely representable.The construction may need to enlarge the backward-reachable set to obtain a finitely representable one.Source: §5.2 · p. 26
• A practical search can replace basis configurations with sub-configurations at each iteration; it is guaranteed to find an invariant if one exists, but may diverge otherwise.Under local finiteness, the sub-reachable search space is finite at any fixed number of steps, but infinite without a step bound.Source: §5.2 · p. 26
• The symbolic refinement uses a formula to identify tuples that generate configurations in a formula’s basis, since tuple satisfaction alone does not establish basis minimality.The Min characterization holds when the tuple satisfies the formula and the generated configuration belongs to the basis.Source: §5.2 · pp. 26–27
• For locally finite T_E, only finitely many formulas K up to array-equivalence satisfy K ≤ L, and all such formulas can be effectively computed.The proof bounds the existential-prefix lengths, making the candidate search finite.Source: §5.2 · p. 29
• Under local finiteness of T_E, a safety invariant exists for U iff SInv returns one for a suitable ChooseCover function.SInv builds the search from existential-index formulas that cover U and successive predecessor formulas.Source: §5.2 · p. 31
• SInv uses ChooseCover(L) to select an existential-index formula covering L, providing a symbolic substitute for the non-symbolic function γ.The paper states the correctness of this procedure under the local-finiteness condition.Source: §5.2 · p. 31
• When ChooseCover is the identity, SInv is the exact dual of BReach and can return only the negation of a symbolic representation of all backward-reachable states as a safety invariant.This choice uses L itself as a cover of L.Source: §5.2 · p. 32

6. Pragmatics of Invariant Synthesis and Experiments

• Because exhaustive search for a safety invariant may be infeasible, the approach finds invariants generally and uses them to prune backward reachability.Exhaustively choosing formulas to cover an ∃I-formula would make a concrete implementation impractical.Source: §6 · p. 32

6.1. Integrating Invariant Synthesis within Backward Reachability.

• BReach+Inv prunes by adding negations of validated candidate invariants to B, preserving correct safety answers, but is incomplete despite deterministic, parallelizable execution.It may not terminate even when a safety invariant exists; candidate invariants are checked before they are used for pruning.Source: §6.1 · pp. 32–33, §6.3 · p. 35

6.2. Index Abstraction.

• Index abstraction removes selected index variables to form candidate invariants, using maximal index-theory literals when decomposing the quantified indices.Coarse approximations are acceptable because a candidate is used for pruning only after being proved a real invariant.Source: §6.2 · p. 34

6.3. Signature Abstraction.

• Signature abstraction eliminates literals containing selected array variables from pre-image disjuncts, using quantifier elimination whenever possible.The selected variable subset may be user-suggested or dynamically derived from the current pre-image disjunct.Source: §6.3 · p. 34

6.4. Experiments.

• The evaluation uses default and experimentally tuned settings, records tableau and solver measures and runtime, and marks runs stopped after repeated transition loops as timeouts.The authors note that the reported best settings may not be optimal for every problem.Source: §6.4 · pp. 35–36
• Invariant synthesis reduces solving time for larger mutual-exclusion examples, has negligible effect on cache-coherence protocols, and helps mcmt terminate on almost all imperative programs.Signature abstraction is a crucial ingredient for the imperative-program results; the benchmark set is more representative for the first two categories than for the latter two.Source: §6.4 · pp. 35–36
• On problems from the PFS and Undip distributions, mcmt performs better or outperforms those tools on the largest benchmarks.PFS and Undip cannot handle some considered problems, including imperative programs, because their input syntax and theoretical frameworks are too restrictive.Source: §6.4 · p. 37

7. Discussion

• The approach represents topology and local data with theories, supporting varied system classes while keeping pre-image computation within a fixed set of logical operations.The authors contrast this with approaches that use topology-specific data structures and require modifications to pre-image algorithms when topology changes.Source: §7 · pp. 37–38
• Sufficient theory conditions support termination and safety decidability, while invariant synthesis is complete under suitable index- and element-theory hypotheses and can be interleaved with backward reachability.The authors report implementing and evaluating these techniques on benchmarks from varied sources, with experimental results confirming efficiency and flexibility.Source: §7 · p. 38

7.1. Related work.

• MCMT’s first-order representation makes fix-point checks SMT problems with universally quantified variables, recapturing embeddings through model theory and enabling broader applications than the cited well-structured-system implementations,.Those implementations rely on costly exhaustive embedding enumeration and topology-specific pre-image and embedding algorithms; MCMT can still soundly use incomplete quantifier instantiation with richer theories.Source: §7.1 · p. 39
• Predicate abstraction must handle universally quantified variables and proof obligations; MCMT computes backward reachable states precisely and uses abstraction to guess candidate invariants for pruning.The paper says MCMT’s current predicate-abstraction form is primitive signature abstraction, while its quantifier instantiation is extensive and includes completeness-preserving heuristics.Source: §7.1 · pp. 39–40

7.2. Future work.

• The authors plan to improve signature abstraction and abstraction refinement, expand experiments across system classes, and investigate verification of a subclass of liveness properties.They cite preliminary work on parametrised timed automata and experiments on fault-tolerant distributed algorithms.Source: §7.2 · p. 41

Decidability of restricted satisfiability checking.

• The sentence (A.1) is decidable, and its index-theory satisfiability is equivalent to satisfiability in a finite index model and to satisfiability of the representative-term formula (A.2).The result concerns formulas of the displayed existential-universal form, with existential array variables, index and element variables, and quantification over index variables.Source: Decidability of restricted… · p. 44
• The proof restricts the index domain to the substructure generated by assigned index variables, yielding a finite model under the stated local-finiteness condition.The passage states that the index theory is closed under substructures and that the restricted structure remains a model of that theory.Source: Decidability of restricted… · p. 44
• After replacing representative index terms with fresh variables, disjoint index and element signatures let the decision procedure guess index equalities and check satisfiability separately in each theory.For each guessed equivalence relation, the procedure checks index literals with the corresponding equalities and inequalities, then checks element literals with equalities induced by that relation.Source: Decidability of restricted… · p. 45
• The proof states that the resulting procedure is sound and complete.It returns unsatisfiable only when every possible equivalence-relation guess fails one of the two theory checks.Source: Decidability of restricted… · p. 45

Undecidability of backward reachability.

• The construction uses index structures with an injective partial successor relation and element values from a finite datatype encoding machine locations and register markers.The index and element theories are locally finite; the index theory is closed under substructures, and the element theory admits quantifier elimination.Source: Undecidability of backward reachability · p. 46
• Array configurations encode a machine location and register contents through marked positions along an index chain, with the initial formula representing the zero-register start configuration.The encoding conditions define when an array configuration bi-simulates a machine configuration, and the transition formula simulates machine steps.Source: Undecidability of backward reachability · p. 46
• The transition relation is a disjunction of theory formulas for the machine instructions, updating array values to simulate their configuration transformations.The section describes formulas for instruction kinds and says the remaining kinds are defined accordingly.Source: Undecidability of backward reachability · p. 47
• A machine reaches configuration (q, m, n) if and only if the constructed array-based system is unsafe with respect to Uq,m,n, establishing undecidability of backward reachability.The proof reduces from the undecidable two-register Minsky-machine reachability problem.Source: Undecidability of backward reachability · pp. 46–47

Undecidability of unrestricted satisfiability checking

• A Minsky-machine reachability reduction shows Hypothesis (I) cannot be removed from Theorem 3.3 or Theorem A.1.The argument is similar to the reduction used for the safety-problem undecidability result.Source: Undecidability of unrestricted… · p. 47
• The example uses non-locally-finite natural-number indexes and transitions over array elements drawn from Q×N×N.The transition cases update one of the two numeric components or change the control state.Source: Undecidability of unrestricted… · pp. 47–48
• Satisfiability of ∃A,I∀I-formulae can be undecidable even when SMT(TI) and SMT(TE) are decidable, because the array encodes a reachable computation.The formula is satisfiable iff the target configuration is reachable.Source: Undecidability of unrestricted… · p. 48
• Even with local finiteness, dropping closure under substructures leaves a counterexample, so both conditions of Hypothesis (I) are needed.Replacing the successor function with a relation restores local finiteness, while proper substructures must still be excluded.Source: Undecidability of unrestricted… · p. 48