Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Multi-Property Synthesis

Christoph Weinhuber, Yannik Schnitzer, Alessandro Abate, David Parker, Giuseppe De Giacomo, Moshe Y. Vardi

TL;DR

A fully symbolic algorithm is developed that introduces Boolean goal variables and exploits monotonicity to represent exponentially many goal combinations compactly and substantially outperforms enumeration-based baselines.

Abstract

We study LTLf synthesis with multiple properties, where satisfying all properties may be impossible. Instead of enumerating subsets of properties, we compute in one fixed-point computation the relation between product-game states and the goal sets that are realizable from them, and we synthesize strategies achieving maximal realizable sets. We develop a fully symbolic algorithm that introduces Boolean goal variables and exploits monotonicity to represent exponentially many goal combinations compactly. Our approach substantially outperforms enumeration-based baselines, with speedups of up to two orders of magnitude.

Multi-Property Synthesis

TL;DR

A fully symbolic algorithm is developed that introduces Boolean goal variables and exploits monotonicity to represent exponentially many goal combinations compactly and substantially outperforms enumeration-based baselines.

Abstract

We study LTLf synthesis with multiple properties, where satisfying all properties may be impossible. Instead of enumerating subsets of properties, we compute in one fixed-point computation the relation between product-game states and the goal sets that are realizable from them, and we synthesize strategies achieving maximal realizable sets. We develop a fully symbolic algorithm that introduces Boolean goal variables and exploits monotonicity to represent exponentially many goal combinations compactly. Our approach substantially outperforms enumeration-based baselines, with speedups of up to two orders of magnitude.
Paper Structure (35 sections, 11 theorems, 28 equations, 2 figures, 2 tables)

This paper contains 35 sections, 11 theorems, 28 equations, 2 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. Multi-property Verification.
  4. Maximum-realizability Synthesis
  5. Over-subscription and Planning with Preferences.
  6. Preliminaries
  7. Linear Temporal Logic over finite traces
  8. $\text{LTL}_f$ Synthesis and DFA Games
  9. Multi-property $\text{LTL}_f$ Synthesis
  10. Solving Multi-property Games
  11. Maximal Multi-Property Synthesis
  12. Symbolic Synthesis
  13. Symbolic Single-Property Synthesis
  14. Symbolic Multi-Property Synthesis
  15. Experiments
  16. ...and 20 more sections

Key Result

Theorem 1

The fixed point $\mathsf{WinM}$ characterizes multi-property realizability: for all $s\in S^\times$ and $C\subseteq \Phi$,

Figures (2)

  • Figure 1: Illustration of our synthesis procedures on a problem with $2^\mathcal{Y}=\{y_1,y_2\}$, $2^\mathcal{X}=\{x_1,x_2\}$, and properties $\Phi=\{\varphi_1,\varphi_2,\varphi_3\}$. (a) and (b) depict the resulting winning relation $\mathsf{WinM}$ projected onto states: each state is annotated with the goal sets that are realizable from it. (a) shows the explicit multi-property fixed point that tracks all realizable goal sets (Section \ref{['sec:solving-multi-property-games']}) and (b) shows the maximal variant (Section \ref{['sec:maximal_multi-prop']}). (c) illustrates the symbolic variant (Section \ref{['sec:symbolic']}), where the winning relation is represented compactly as a Boolean formula.
  • Figure 2: Runtime comparison between our multi-property synthesis and enumeration baseline across all benchmark instances. Each point represents one instance, with color indicating state space size.

Theorems & Definitions (28)

  • Definition 1: $\text{LTL}_f$ Synthesis
  • Definition 2: DFA Game Arena
  • Definition 3: Multi-property $\text{LTL}_f$ Synthesis
  • Definition 4: Multi-property Game Arena
  • Definition 5: Multi-Property Satisfaction
  • Theorem 1
  • Theorem 2
  • Theorem 3
  • Example 1
  • Theorem 4
  • ...and 18 more