# Model Checking Strategies from Synthesis Over Finite Traces

arXiv: https://arxiv.org/abs/2305.08319 · HTML: https://mlsanity.com/paper/2305.08319/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 54 references that are in the map.
- First posted on arXiv 15 May 2023.

## Builds on (most cited first, 8 of 8)

- [Foundations for Restraining Bolts: Reinforcement Learning with LTLf/LDLf restraining specifications](https://mlsanity.com/paper/1807.06333/) (2018)
- [From Spot 2.0 to Spot 2.10: What's New?](https://mlsanity.com/paper/2206.11366/) (2022)
- [Symbolic LTLf Synthesis](https://mlsanity.com/paper/1705.08426/) (2017)
- [Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications](https://mlsanity.com/paper/1911.08145/) (2019)
- [LTLf Synthesis on Probabilistic Systems](https://mlsanity.com/paper/2009.10883/) (2020)
- [Forward LTLf Synthesis: DPLL At Work](https://mlsanity.com/paper/2302.13825/) (2023)
- [Synthesis of coordination programs from linear temporal logic](https://mlsanity.com/paper/1911.03807/) (2019)
- [The Temporal Logic Synthesis Format TLSF v1.2](https://mlsanity.com/paper/2303.03839/) (2023)

## Built on by (most cited first, 3 of 3)

- [LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces](https://mlsanity.com/paper/2411.09366/) (2024)
- [Monitoring Second-Order Hyperproperties](https://mlsanity.com/paper/2404.09652/) (2024)
- [Computational Grounding of Responsibility Attribution and Anticipation in LTLf](https://mlsanity.com/paper/2410.14544/) (2024)

## Abstract (arXiv)

The innovations in reactive synthesis from em Linear Temporal Logics over finite traces (LTLf) will be amplified by the ability to verify the correctness of the strategies generated by LTLf synthesis tools. This motivates our work on em LTLf model checking. LTLf model checking, however, is not straightforward. The strategies generated by LTLf synthesis may be represented using em terminating transducers or em non-terminating transducers where executions are of finite-but-unbounded length or infinite length, respectively. For synthesis, there is no evidence that one type of transducer is better than the other since they both demonstrate the same complexity and similar algorithms. In this work, we show that for model checking, the two types of transducers are fundamentally different. Our central result is that LTLf model checking of non-terminating transducers is exponentially harder than that of terminating transducers. We show that the problems are EXPSPACE-complete and PSPACE-complete, respectively. Hence, considering the feasibility of verification, LTLf synthesis tools should synthesize terminating transducers. This is, to the best of our knowledge, the first evidence to use one transducer over the other in LTLf synthesis.