Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

LTLf Synthesis Under Unreliable Input

Christian Hagemeier, Giuseppe de Giacomo, Moshe Y. Vardi

TL;DR

This work addresses synthesizing LTLf goals when some environment inputs may be unreliable and must be guarded by a backup specification. It formalizes a two-arena model and proves the problem is $2EXPTIME$-complete, then presents three solution techniques: a Direct Automata method, a Belief-State DFA method, and a MSO/QLTLf-based method, with the latter leveraging second-order quantified finite-trace logics. Each method has distinct theoretical guarantees: $2EXPTIME$-complete for the direct approach, $3EXPTIME$ for belief-state, and $2EXPTIME$ for the MSO/QLTLf route, the MSO variant being implementable via MONA. Empirically, the MSO method tends to outperform the others, challenging the perceived hardness implied by worst-case bounds, and the paper also extends synthesis to arbitrary $qltl_f$ specifications. The results offer a practical, scalable suite of techniques for safety-critical settings where input unreliability must be accounted for without relying on probabilistic models.

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.

LTLf Synthesis Under Unreliable Input

TL;DR

This work addresses synthesizing LTLf goals when some environment inputs may be unreliable and must be guarded by a backup specification. It formalizes a two-arena model and proves the problem is -complete, then presents three solution techniques: a Direct Automata method, a Belief-State DFA method, and a MSO/QLTLf-based method, with the latter leveraging second-order quantified finite-trace logics. Each method has distinct theoretical guarantees: -complete for the direct approach, for belief-state, and for the MSO/QLTLf route, the MSO variant being implementable via MONA. Empirically, the MSO method tends to outperform the others, challenging the perceived hardness implied by worst-case bounds, and the paper also extends synthesis to arbitrary specifications. The results offer a practical, scalable suite of techniques for safety-critical settings where input unreliability must be accounted for without relying on probabilistic models.

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.

Paper Structure

This paper contains 33 sections, 27 theorems, 17 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. ltl$_f$ Synthesis under Unreliable Input
  4. Technique 1: Direct Automata
  5. Technique 2: Belief-States
  6. Quantified ltl$_f$ Synthesis
  7. Technique 3: MSO Encoding
  8. Empirical Evaluation
  9. Related Work
  10. Conclusion
  11. Proofs
  12. Direct Approach
  13. Belief State Approach
  14. Translation of Quantified ltl$_f$ to MSO
  15. Quantified LTLf Synthesis
  16. ...and 18 more sections

Key Result

Theorem 9

Solving synthesis for the synchronous product of the ltl$_f$-automaton for $\varphi_m$, $A_{\varphi_m}$, and the automaton $\overline{\mathcal{D}((\mathcal{A}_{\lnot \varphi})_{\exists U_1, \dots, U_n})}$ solves synthesis under unreliable input.

Figures (4)

  • Figure 1: Runtime for the sheep and hiker examples.
  • Figure 2: Runtime for the trap examples.
  • Figure 3: Boxplot of ratio of MSO solution for synthesis under unreliable input
  • Figure 4: Overhead on tests

Theorems & Definitions (65)

  • Definition 1
  • Definition 2: ltl$_f$ semantics
  • Definition 3: ltl$_f$ synthesis under unreliable input
  • Example 4: Sheep
  • Example 5: Trap
  • Example 6: Hiker
  • Definition 7: Synchronous Product of DFAs
  • Definition 8
  • Theorem 9
  • proof
  • ...and 55 more