CTL* synthesis via LTL synthesis
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 satisfact...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2017-11-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1711.10636v1 |