Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

CTL* Verification and Synthesis using Existential Horn Clauses

Mishel Carelli, Orna Grumberg

TL;DR

This work develops a translation-based framework that verifies and synthesizes infinite-state reactive programs against $CTL^*$ specifications by translating problems into Existential Horn Clauses and solving with the $E$-HSF solver. The core contribution is the translation system $\textsf{Trans}$, which converts a program $P$ and a $CTL^*$ formula $\phi$ into a satisfiability problem over $EHC$s such that satisfiability corresponds to $P\models\phi$, and a synthesis approach that fills holes in partial programs by introducing uninterpreted predicates and reducing synthesis to $EHC$ satisfiability. The paper proves soundness and relative completeness for both verification and synthesis, and demonstrates practical applicability through case studies on robot systems and bank–client interactions. The results enable verification and synthesis for infinite-state systems with first-order $CTL^*$ specifications, independent of the underlying $EHC$ solver, and suggest pathways for integrating with broader formalisms like pfwCSP in future work.

Abstract

This work proposes a novel approach for automatic verification and synthesis of infinite-state reactive programs with respect to ${CTL}^*$ specifications, based on translation to Existential Horn Clauses (EHCs). $CTL^*$ is a powerful temporal logic, which subsumes the temporal logics LTL and CTL, both widely used in specification, verification, and synthesis of complex systems. EHCs with its solver E-HSF, is an extension of Constrained Horn Clauses, which includes existential quantification as well as the power of handling well-foundedness. We develop the translation system \textit{Trans}, which given a verification problem consisting of a program $P$ and a specification $φ$, builds a set of EHCs which is satisfiable iff $P$ satisfies $φ$. We also develop a synthesis algorithm that given a program with holes in conditions and assignments, fills the holes so that the synthesized program satisfies the given $CTL^*$ specification. We prove that our verification and synthesis algorithms are both sound and relative complete. Finally, we present case studies to demonstrate the applicability of our algorithms for $CTL^*$ verification and synthesis.

CTL* Verification and Synthesis using Existential Horn Clauses

TL;DR

This work develops a translation-based framework that verifies and synthesizes infinite-state reactive programs against specifications by translating problems into Existential Horn Clauses and solving with the -HSF solver. The core contribution is the translation system , which converts a program and a formula into a satisfiability problem over s such that satisfiability corresponds to , and a synthesis approach that fills holes in partial programs by introducing uninterpreted predicates and reducing synthesis to satisfiability. The paper proves soundness and relative completeness for both verification and synthesis, and demonstrates practical applicability through case studies on robot systems and bank–client interactions. The results enable verification and synthesis for infinite-state systems with first-order specifications, independent of the underlying solver, and suggest pathways for integrating with broader formalisms like pfwCSP in future work.

Abstract

This work proposes a novel approach for automatic verification and synthesis of infinite-state reactive programs with respect to specifications, based on translation to Existential Horn Clauses (EHCs). is a powerful temporal logic, which subsumes the temporal logics LTL and CTL, both widely used in specification, verification, and synthesis of complex systems. EHCs with its solver E-HSF, is an extension of Constrained Horn Clauses, which includes existential quantification as well as the power of handling well-foundedness. We develop the translation system \textit{Trans}, which given a verification problem consisting of a program and a specification , builds a set of EHCs which is satisfiable iff satisfies . We also develop a synthesis algorithm that given a program with holes in conditions and assignments, fills the holes so that the synthesized program satisfies the given specification. We prove that our verification and synthesis algorithms are both sound and relative complete. Finally, we present case studies to demonstrate the applicability of our algorithms for verification and synthesis.
Paper Structure (19 sections, 10 theorems, 45 equations, 2 figures)

This paper contains 19 sections, 10 theorems, 45 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Related work
  3. Preliminaries
  4. Forall-exists Horn-like clauses (EHC)
  5. $CTL^*$ verification
  6. Reduction of $CTL^*$ verification problem to EHC satisfiability
  7. Soundness
  8. Relative completeness
  9. Case study 1: $CTL^*$ verification of a robot system
  10. $CTL^*$ synthesis from partial programs
  11. Reduction of $CTL^*$ synthesis to EHC satisfiability
  12. Case study 2: Synthesizing a bank-client interaction
  13. Conclusion
  14. Appendix
  15. Proof of complexity theorem
  16. ...and 4 more sections

Key Result

theorem thmcountertheorem

Let $(D,\phi)$ be a verification problem, with a program of size $m$, with $k$ fairness conditions, and a specification formula of size $n$. Then ${\textsf{Trans}}\xspace$ produces a set $Clauses(D,\phi)$ consisting of $O(n(n+k))$ clauses with a total size of $O(n(n+k)(n+m))$.

Figures (2)

  • Figure 1: Robots program R
  • Figure 2: Synthesizing bank-client interaction

Theorems & Definitions (19)

  • definition thmcounterdefinition
  • remark thmcounterremark
  • theorem thmcountertheorem: complexity
  • theorem thmcountertheorem: soundness
  • proof
  • theorem thmcountertheorem: relative completeness
  • proof
  • theorem thmcountertheorem: soundness
  • theorem thmcountertheorem: Relative completeness
  • theorem thmcountertheorem: complexity
  • ...and 9 more