Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings

Raz Lotan, Neta Elad, Oded Padon, Sharon Shoham

TL;DR

This work addresses the verification of first-order temporal properties over infinite-state systems by reducing FO-LTL to termination through a timer-based augmentation that tracks property violations. It introduces prophecy timer variables and a timer transition system, then combines this with an extended implicit-ranking framework to prove termination automatically via SMT solving, without requiring fairness assumptions. The authors implement the approach and demonstrate its applicability across challenging temporal-verification tasks, including distributed protocols and program termination, showing intuitive, formal proofs within a unified framework. The method broadens the scope of automated verification for FO-LTL properties in infinite domains and offers a practical, solver-assisted pathway for verifying complex temporal properties in real systems.

Abstract

We present a unified deductive verification framework for first-order temporal properties based on well-founded rankings, where verification conditions are discharged using SMT solvers. To that end, we introduce a novel reduction from verification of arbitrary temporal properties to verification of termination. Our reduction augments the system with prophecy timer variables that predict the number of steps along a trace until the next time certain temporal formulas, including the negated property, hold. In contrast to standard tableaux-based reductions, which reduce the problem to fair termination, our reduction does not introduce fairness assumptions. To verify termination of the augmented system, we follow the traditional approach of assigning each state a rank from a well-founded set and showing that the rank decreases in every transition. We leverage the recently proposed formalism of implicit rankings to express and automatically verify the decrease of rank using SMT solvers, even when the rank is not expressible in first-order logic. We extend implicit rankings from finite to infinite domains, enabling verification of more general systems and making them applicable to the augmented systems generated by our reduction, which allows us to exploit the decrease of timers in termination proofs. We evaluate our technique on a range of temporal verification tasks from previous works, giving simple, intuitive proofs for them within our framework.

Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings

TL;DR

This work addresses the verification of first-order temporal properties over infinite-state systems by reducing FO-LTL to termination through a timer-based augmentation that tracks property violations. It introduces prophecy timer variables and a timer transition system, then combines this with an extended implicit-ranking framework to prove termination automatically via SMT solving, without requiring fairness assumptions. The authors implement the approach and demonstrate its applicability across challenging temporal-verification tasks, including distributed protocols and program termination, showing intuitive, formal proofs within a unified framework. The method broadens the scope of automated verification for FO-LTL properties in infinite domains and offers a practical, solver-assisted pathway for verifying complex temporal properties in real systems.

Abstract

We present a unified deductive verification framework for first-order temporal properties based on well-founded rankings, where verification conditions are discharged using SMT solvers. To that end, we introduce a novel reduction from verification of arbitrary temporal properties to verification of termination. Our reduction augments the system with prophecy timer variables that predict the number of steps along a trace until the next time certain temporal formulas, including the negated property, hold. In contrast to standard tableaux-based reductions, which reduce the problem to fair termination, our reduction does not introduce fairness assumptions. To verify termination of the augmented system, we follow the traditional approach of assigning each state a rank from a well-founded set and showing that the rank decreases in every transition. We leverage the recently proposed formalism of implicit rankings to express and automatically verify the decrease of rank using SMT solvers, even when the rank is not expressible in first-order logic. We extend implicit rankings from finite to infinite domains, enabling verification of more general systems and making them applicable to the augmented systems generated by our reduction, which allows us to exploit the decrease of timers in termination proofs. We evaluate our technique on a range of temporal verification tasks from previous works, giving simple, intuitive proofs for them within our framework.
Paper Structure (39 sections, 5 theorems, 10 equations, 1 figure, 2 tables)

This paper contains 39 sections, 5 theorems, 10 equations, 1 figure, 2 tables.

Table of Contents

  1. Introduction
  2. Contributions.
  3. Running Example
  4. Preliminaries
  5. First-Order Logic.
  6. Specifying Transition Systems in First-Order Logic.
  7. First-Order Linear Temporal Logic.
  8. Timers
  9. The Timer Transition System
  10. The Timer Reduction
  11. Rankings
  12. Verifying Termination with Implicit Rankings
  13. Constructors of Implicit Rankings
  14. Validating Decrease of Rank and Soundness Conditions
  15. Implementation and Evaluation
  16. ...and 24 more sections

Key Result

lemma 1

Let $\hat{\pi} = (\hat{s}_i)_{i=0}^\infty$ be a trace of $\mathcal{T}_{\varphi}(\mathcal{S}_\mathrm{time})$ with domain $D$, $\psi(\vec{x})\in A({\varphi})$, $v\in\mathop{\mathrm{assign}}\nolimits(\vec{x},D)$ and $i\in\mathbb{N}$. Then $\hat{s}_i,v \models (t_{\psi}(\vec{x}) = 0)$ if and only if $\h

Figures (1)

  • Figure 1: Ticket Protocol

Theorems & Definitions (19)

  • definition 1
  • remark 1
  • remark 2
  • lemma 1
  • lemma 2
  • remark 3
  • theorem 1
  • definition 2: Closed Implicit Ranking
  • theorem 2
  • definition 3: Implicit Ranking
  • ...and 9 more