LTLf Synthesis Under Unreliable Input

TL;DR

This paper addresses the synthesis of strategies for LTLf goals under unreliable inputs, proposing three methods with different complexity and evaluating their practical performance.

Contribution

It introduces three novel solution techniques for LTLf synthesis with unreliable inputs, including a new QLTLf-based approach and a general synthesis procedure.

Findings

MSO technique performs best empirically

Belief construction is more efficient than direct automata manipulation

All methods are theoretically 2EXPTIME or higher in worst-case complexity

Abstract

We study the problem of realizing strategies for an LTLf goal specification while ensuring that at least an LTLf backup specification is satisfied in case of unreliability of certain input variables. We formally define the problem and characterize its worst-case complexity as 2EXPTIME-complete, like standard LTLf synthesis. Then we devise three different solution techniques: one based on direct automata manipulation, which is 2EXPTIME, one disregarding unreliable input variables by adopting a belief construction, which is 3EXPTIME, and one leveraging second-order quantified LTLf (QLTLf), which is 2EXPTIME and allows for a direct encoding into monadic second-order logic, which in turn is worst-case nonelementary. We prove their correctness and evaluate them against each other empirically. Interestingly, theoretical worst-case bounds do not translate into observed performance; the MSO technique performs best, followed by belief construction and direct automata manipulation. As a byproduct of our study, we provide a general synthesis procedure for arbitrary QLTLf specifications.