Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

5 Scopus citations

Abstract

We propose “semantic labelling” as a novel ingredient for solving games in the context of LTL synthesis. It exploits recent advances in the automata-based approach, yielding more information for each state of the generated parity game than the game graph can capture. We utilize this extra information to improve standard approaches as follows. (i) Compared to strategy improvement (SI) with random initial strategy, a more informed initialization often yields a winning strategy directly without any computation. (ii) This initialization makes SI also yield smaller solutions. (iii) While Q-learning on the game graph turns out not too efficient, Q-learning with the semantic information becomes competitive to SI. Since already the simplest heuristics achieve significant improvements the experimental results demonstrate the utility of semantic labelling. This extra information opens the door to more advanced learning approaches both for initialization and improvement of strategies.

Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis- 17th International Symposium, AVTA 2019, Proceedings
EditorsYu-Fang Chen, Chih-Hong Cheng, Javier Esparza
PublisherSpringer
Pages404-422
Number of pages19
ISBN (Print)9783030317836
DOIs
StatePublished - 2019
Event17th International Symposium on Automated Technology for Verification and Analysis, ATVA 2019 - Taipei, Taiwan, Province of China
Duration: 28 Oct 201931 Oct 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11781 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference17th International Symposium on Automated Technology for Verification and Analysis, ATVA 2019
Country/TerritoryTaiwan, Province of China
CityTaipei
Period28/10/1931/10/19

Fingerprint

Dive into the research topics of 'Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis'. Together they form a unique fingerprint.

Cite this