Model Checking Strategies from Synthesis Over Finite Traces

TL;DR

This paper investigates the complexity of model checking strategies derived from LTLf synthesis, revealing that terminating transducers are significantly easier to verify than non-terminating ones, guiding future synthesis tool design.

Contribution

It demonstrates that LTLf model checking is exponentially harder for non-terminating transducers and advocates for synthesizing terminating transducers for feasible verification.

Findings

Non-terminating transducers are EXPSPACE-complete to verify.

Terminating transducers are PSPACE-complete to verify.

Verifying terminating transducers is exponentially easier than non-terminating ones.

Abstract

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 \emph{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 \emph{first} evidence to use one transducer over the other in LTLf synthesis.