Synthesis for Multi-weighted Games with Branching-Time Winning Conditions

Isabella Kaufmann, Kim Guldstrand Larsen, Jiří Srba*

*Kontaktforfatter

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

Abstrakt

We investigate the synthesis problem in a quantitative game-theoretic setting with branching-time objectives. The objectives are given in a recursive modal logic with semantics defined over a multi-weighted extension of a Kripke structure where each transition is annotated with multiple nonnegative weights representing quantitative resources such as discrete time, energy and cost. The objectives may express bounds on the accumulation of each resource both in a global scope and in a local scope (on subformulae) utilizing a reset operator. We show that both the model checking problem as well as the synthesis problem are decidable and that the model checking problem is EXPTIME-complete, while the synthesis problem is in 2-EXPTIME and is NEXPTIME-hard. Furthermore, we encode both problems to the calculation of maximal fixed points on dependency graphs, thus achieving on-the-fly algorithms with the possibility of early termination.

OriginalsprogEngelsk
TitelApplication and Theory of Petri Nets and Concurrency - 41st International Conference, PETRI NETS 2020, Proceedings
RedaktørerRyszard Janicki, Natalia Sidorova, Thomas Chatain
Antal sider21
ForlagSpringer VS
Publikationsdato2020
Sider46-66
ISBN (Trykt)9783030518301
ISBN (Elektronisk)978-3-030-51831-8
DOI
StatusUdgivet - 2020
Begivenhed41st International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2020 - Paris , Frankrig
Varighed: 24 jun. 202025 jun. 2020

Konference

Konference41st International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2020
LandFrankrig
ByParis
Periode24/06/202025/06/2020
NavnLecture Notes in Computer Science
Vol/bind12152
ISSN0302-9743

Fingeraftryk Dyk ned i forskningsemnerne om 'Synthesis for Multi-weighted Games with Branching-Time Winning Conditions'. Sammen danner de et unikt fingeraftryk.

Citationsformater