Efficient CTL Verification via Horn Constraints Solving

TL;DR

This paper introduces a novel approach for CTL property verification in reactive systems by encoding the problem as Horn constraints, leveraging existing solvers to improve efficiency and effectiveness over current methods.

Contribution

The paper presents a new method that encodes CTL verification as Horn constraints, enabling the use of off-the-shelf solvers and outperforming existing specialized techniques.

Findings

Outperforms state-of-the-art CTL verification methods

Successfully applied to challenging examples

Utilizes Horn constraint solving for efficient verification

Abstract

The use of temporal logics has long been recognised as a fundamental approach to the formal specification and verification of reactive systems. In this paper, we take on the problem of automatically verifying a temporal property, given by a CTL formula, for a given (possibly infinite-state) program. We propose a method based on encoding the problem as a set of Horn constraints. The method takes a program, modeled as a transition system, and a property given by a CTL formula as input. It first generates a set of forall-exists quantified Horn constraints and well-foundedness constraints by exploiting the syntactic structure of the CTL formula. Then, the generated set of constraints are solved by applying an off-the-shelf Horn constraints solving engine. The program is said to satisfy the property if and only if the generated set of constraints has a solution. We demonstrate the practical promises of the method by applying it on a set of challenging examples. Although our method is based on a generic Horn constraint solving engine, it is able to outperform state-of-art methods specialised for CTL verification.