CTL* synthesis via LTL synthesis

Roderick Bloem
Sven Schewe
Ayrat Khalimov

We reduce synthesis for CTL* properties to synthesis for LTL. In the context of model checking this is impossible — CTL* is more expressive than LTL. Yet, in synthesis we have knowledge of the system structure and we can add new outputs. These outputs can be used to encode witnesses of the satisfaction of CTL* subformulas directly into the system. This way, we construct an LTL formula, over old and new outputs and original inputs, which is realisable if, and only if, the original CTL* formula is realisable. The CTL*-via-LTL synthesis approach preserves the problem complexity, although it might increase the minimal system size. We implemented the reduction, and evaluated the CTL*-via-LTL synthesiser on several examples.

In Dana Fisman and Swen Jacobs: Proceedings Sixth Workshop on Synthesis (SYNT 2017), Heidelberg, Germany, 22nd July 2017, Electronic Proceedings in Theoretical Computer Science 260, pp. 4–22.
Published: 28th November 2017.

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