CTL* Verification and Synthesis using Existential Horn Clauses
<|reference_start|>CTL* Verification and Synthesis using Existential Horn Clauses: 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 $\phi$, builds a set of EHCs which is satisfiable iff $P$ satisfies $\phi$. 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.<|reference_end|>
@article{carelli2024ctl*,
    title={CTL* Verification and Synthesis using Existential Horn Clauses},
    author={Mishel Carelli and Orna Grumberg},
    journal={arXiv preprint arXiv:2408.11502},
    year={2024},
    archivePrefix={arXiv},
    eprint={2408.11502},
    primaryClass={cs.LO}
}