{
  "annotation_id": "3b595d4f-e3ad-4270-972a-a5ee9b644175",
  "date_created": "2026-02-17T05:53:26.426000Z",
  "date_modified": "2026-02-17T05:53:26.426000Z",
  "file_hash": "11ab931070a2f8ca2f4482d2593468cea96ac438091a174e3327fb7cfe252e68",
  "private": false,
  "record": {
    "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.",
    "arxiv_id": "2601.10651",
    "authors": [
      "Christoph Weinhuber",
      "Yannik Schnitzer",
      "Alessandro Abate",
      "David Parker",
      "Giuseppe De Giacomo",
      "Moshe Y. Vardi"
    ],
    "categories": [
      "cs.AI",
      "cs.LO"
    ],
    "license": "http://creativecommons.org/licenses/by/4.0/",
    "title": "Multi-Property Synthesis",
    "url": "https://arxiv.org/abs/2601.10651",
    "version": "v1"
  },
  "schema_id": "dorsal/arxiv",
  "source": {
    "execution_id": "cef0d3fc-1f55-4403-b9e2-336b5c69aeb3",
    "id": "arXiv Dataset",
    "type": "Model",
    "variant": "snapshot-2026-01-17",
    "version": "0.1.0"
  },
  "user_id": 1000002
}