Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

SAT-based Learning of Computation Tree Logic

Adrien Pommellet, Daniel Stan, Simon Scatton

TL;DR

This work tackles the problem of learning Computation Tree Logic (CTL) formulas that distinguish between positive and negative state samples within finite Kripke structures. It introduces a SAT-based encoding for learning a CTL formula of bounded size, along with a bottom-up strategy to guarantee minimality, and provides optimizations such as embedding negations and approximating the recurrence diameter to reduce computational burden. An explicit separating formula is shown to exist with provable size bounds, and a prototype tool LearnCTL demonstrates practical feasibility by learning separating CTL formulas from mutated higher-level models and program graphs. The results indicate that the proposed optimizations substantially improve performance and that the framework can scale to realistic KS sizes, enabling explanation generation and model-differentiation in software verification contexts.

Abstract

The CTL learning problem consists in finding for a given sample of positive and negative Kripke structures a distinguishing CTL formula that is verified by the former but not by the latter. Further constraints may bound the size and shape of the desired formula or even ask for its minimality in terms of syntactic size. This synthesis problem is motivated by explanation generation for dissimilar models, e.g. comparing a faulty implementation with the original protocol. We devise a SAT-based encoding for a fixed size CTL formula, then provide an incremental approach that guarantees minimality. We further report on a prototype implementation whose contribution is twofold: first, it allows us to assess the efficiency of various output fragments and optimizations. Secondly, we can experimentally evaluate this tool by randomly mutating Kripke structures or syntactically introducing errors in higher-level models, then learning CTL distinguishing formulas.

SAT-based Learning of Computation Tree Logic

TL;DR

This work tackles the problem of learning Computation Tree Logic (CTL) formulas that distinguish between positive and negative state samples within finite Kripke structures. It introduces a SAT-based encoding for learning a CTL formula of bounded size, along with a bottom-up strategy to guarantee minimality, and provides optimizations such as embedding negations and approximating the recurrence diameter to reduce computational burden. An explicit separating formula is shown to exist with provable size bounds, and a prototype tool LearnCTL demonstrates practical feasibility by learning separating CTL formulas from mutated higher-level models and program graphs. The results indicate that the proposed optimizations substantially improve performance and that the framework can scale to realistic KS sizes, enabling explanation generation and model-differentiation in software verification contexts.

Abstract

The CTL learning problem consists in finding for a given sample of positive and negative Kripke structures a distinguishing CTL formula that is verified by the former but not by the latter. Further constraints may bound the size and shape of the desired formula or even ask for its minimality in terms of syntactic size. This synthesis problem is motivated by explanation generation for dissimilar models, e.g. comparing a faulty implementation with the original protocol. We devise a SAT-based encoding for a fixed size CTL formula, then provide an incremental approach that guarantees minimality. We further report on a prototype implementation whose contribution is twofold: first, it allows us to assess the efficiency of various output fragments and optimizations. Secondly, we can experimentally evaluate this tool by randomly mutating Kripke structures or syntactically introducing errors in higher-level models, then learning CTL distinguishing formulas.
Paper Structure (38 sections, 7 theorems, 18 equations, 9 figures, 1 algorithm)

This paper contains 38 sections, 7 theorems, 18 equations, 9 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related work.
  3. Preliminary Definitions
  4. Kripke structures
  5. Computation Tree Logic
  6. Bounded semantics
  7. The Learning Problem
  8. Introducing the problem
  9. An explicit solution
  10. SAT-based Learning
  11. Modelling the formula
  12. Applying the formula to the sample
  13. Solving the SAT instance
  14. Algorithms for the Minimal Learning Problem
  15. A bottom-up algorithm
  16. ...and 23 more sections

Key Result

theorem 1

Given a KS $\mathcal{K}$, there exists $i_0 \in \mathbb{N}$ such that $\forall \, i \geq i_0$, ${\sim} = {\sim_i}$. The smallest integer $i_0$ verifying that property is known as the characteristic number$\mathcal{C}_\mathcal{K}$ of $\mathcal{K}$.

Figures (9)

  • Figure 1: The syntactic tree and indexed DAG of the CTL formula $\neg a \land \mathop{\mathrm{\forall\mathsf{X}}}\nolimits a$.
  • Figure 2: The syntactic DAG of $\neg \exists \, \top \mathop{\mathrm{\mathsf{U}}}\nolimits \neg \mathop{\mathrm{\forall\mathsf{X}}}\nolimits \neg a$, before and after embedding negations.
  • Figure 3: An approximation $\beta$ of the recurrence diameter $\alpha$ relying on SCC decomposition that improves upon the coarse upper bound $\alpha(q) \leq |Q|-1 = 6$.
  • Figure 4: Peterson's mutual exclusion protocol in PROMELA and learnt formulas for each deleted instruction.
  • Figure 5: Number of timeouts at ten minutes | arithmetic mean (in milliseconds) on the 178 samples that never timed out of various options and fragments.
  • ...and 4 more figures

Theorems & Definitions (18)

  • definition 1: Kripke Structure
  • definition 2: Bisimulation relation
  • theorem 1: Characteristic number
  • definition 3: Computation Tree Logic
  • definition 4: Semantics of ${\mathop{\mathrm{\forall\mathsf{U}}}\nolimits,\mathop{\mathrm{\exists\mathsf{U}}}\nolimits}$
  • theorem 2: Browne et al. Browne88
  • definition 5: Bounded semantics of CTL
  • theorem 3
  • definition 6: Sample
  • definition 7: Consistent formula
  • ...and 8 more