---
_id: '14259'
abstract:
- lang: eng
  text: "We provide a learning-based technique for guessing a winning strategy in
    a parity game originating from an LTL synthesis problem. A cheaply obtained guess
    can be useful in several applications. Not only can the guessed strategy be applied
    as best-effort in cases where the game’s huge size prohibits rigorous approaches,
    but it can also increase the scalability of rigorous LTL synthesis in several
    ways. Firstly, checking whether a guessed strategy is winning is easier than constructing
    one. Secondly, even if the guess is wrong in some places, it can be fixed by strategy
    iteration faster than constructing one from scratch. Thirdly, the guess can be
    used in on-the-fly approaches to prioritize exploration in the most fruitful directions.\r\nIn
    contrast to previous works, we (i) reflect the highly structured logical information
    in game’s states, the so-called semantic labelling, coming from the recent LTL-to-automata
    translations, and (ii) learn to reflect it properly by learning from previously
    solved games, bringing the solving process closer to human-like reasoning."
acknowledgement: This research was funded in part by the German Research Foundation
  (DFG) project 427755713 Group-By Objectives in Probabilistic Verification (GOPro).
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Jan
  full_name: Kretinsky, Jan
  id: 44CEF464-F248-11E8-B48F-1D18A9856A87
  last_name: Kretinsky
  orcid: 0000-0002-8122-2881
- first_name: Tobias
  full_name: Meggendorfer, Tobias
  id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
  last_name: Meggendorfer
  orcid: 0000-0002-1712-2165
- first_name: Maximilian
  full_name: Prokop, Maximilian
  last_name: Prokop
- first_name: Sabine
  full_name: Rieder, Sabine
  last_name: Rieder
citation:
  ama: 'Kretinsky J, Meggendorfer T, Prokop M, Rieder S. Guessing winning policies
    in LTL synthesis by semantic learning. In: <i>35th International Conference on
    Computer Aided Verification</i>. Vol 13964. Springer Nature; 2023:390-414. doi:<a
    href="https://doi.org/10.1007/978-3-031-37706-8_20">10.1007/978-3-031-37706-8_20</a>'
  apa: 'Kretinsky, J., Meggendorfer, T., Prokop, M., &#38; Rieder, S. (2023). Guessing
    winning policies in LTL synthesis by semantic learning. In <i>35th International
    Conference on Computer Aided Verification</i> (Vol. 13964, pp. 390–414). Paris,
    France: Springer Nature. <a href="https://doi.org/10.1007/978-3-031-37706-8_20">https://doi.org/10.1007/978-3-031-37706-8_20</a>'
  chicago: Kretinsky, Jan, Tobias Meggendorfer, Maximilian Prokop, and Sabine Rieder.
    “Guessing Winning Policies in LTL Synthesis by Semantic Learning.” In <i>35th
    International Conference on Computer Aided Verification</i>, 13964:390–414. Springer
    Nature, 2023. <a href="https://doi.org/10.1007/978-3-031-37706-8_20">https://doi.org/10.1007/978-3-031-37706-8_20</a>.
  ieee: J. Kretinsky, T. Meggendorfer, M. Prokop, and S. Rieder, “Guessing winning
    policies in LTL synthesis by semantic learning,” in <i>35th International Conference
    on Computer Aided Verification</i>, Paris, France, 2023, vol. 13964, pp. 390–414.
  ista: 'Kretinsky J, Meggendorfer T, Prokop M, Rieder S. 2023. Guessing winning policies
    in LTL synthesis by semantic learning. 35th International Conference on Computer
    Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13964, 390–414.'
  mla: Kretinsky, Jan, et al. “Guessing Winning Policies in LTL Synthesis by Semantic
    Learning.” <i>35th International Conference on Computer Aided Verification</i>,
    vol. 13964, Springer Nature, 2023, pp. 390–414, doi:<a href="https://doi.org/10.1007/978-3-031-37706-8_20">10.1007/978-3-031-37706-8_20</a>.
  short: J. Kretinsky, T. Meggendorfer, M. Prokop, S. Rieder, in:, 35th International
    Conference on Computer Aided Verification, Springer Nature, 2023, pp. 390–414.
conference:
  end_date: 2023-07-22
  location: Paris, France
  name: 'CAV: Computer Aided Verification'
  start_date: 2023-07-17
das_tickbox: '1'
date_created: 2023-09-03T22:01:16Z
date_published: 2023-07-17T00:00:00Z
date_updated: 2026-07-07T13:39:23Z
day: '17'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-37706-8_20
external_id:
  isi:
  - '001310786500020'
file:
- access_level: open_access
  checksum: ed66278b61bb869e1baba3d9b9081271
  content_type: application/pdf
  creator: dernst
  date_created: 2023-09-06T08:25:50Z
  date_updated: 2023-09-06T08:25:50Z
  file_id: '14276'
  file_name: 2023_LNCS_CAV_Kretinsky.pdf
  file_size: 428354
  relation: main_file
  success: 1
file_date_updated: 2023-09-06T08:25:50Z
fulldoi: https://doi.org/10.1007/978-3-031-37706-8_20
has_accepted_license: '1'
intvolume: '     13964'
isi: 1
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '07'
oa: 1
oa_version: Published Version
page: 390-414
publication: 35th International Conference on Computer Aided Verification
publication_identifier:
  eissn:
  - 1611-3349
  isbn:
  - '9783031377051'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Guessing winning policies in LTL synthesis by semantic learning
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13964
year: '2023'
...