CTL* Verification and Synthesis using Existential Horn Clauses
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911674583220224 |
|---|---|
| author | Carelli, Mishel Grumberg, Orna |
| author_facet | Carelli, Mishel Grumberg, Orna |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2408_11502 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | CTL* Verification and Synthesis using Existential Horn Clauses Carelli, Mishel Grumberg, Orna Logic in Computer Science 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. |
| title | CTL* Verification and Synthesis using Existential Horn Clauses |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2408.11502 |