Efficient CTL Verification via Horn Constraints Solving

Tewodros A. Beyene
(fortiss GmbH, Munich, Germany)
Corneliu Popeea
(CQSE GmbH, Munich, Germany)
Andrey Rybalchenko
(Microsoft Research, Cambridge, UK)

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.

In John P. Gallagher and Philipp Rümmer: Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis (HCVS2016), Eindhoven, The Netherlands, 3rd April 2016, Electronic Proceedings in Theoretical Computer Science 219, pp. 1–14.
Published: 14th July 2016.

ArXived at: http://dx.doi.org/10.4204/EPTCS.219.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org