2026-07-20T17:24:44Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9690 2024-03-06T10:44:50Z ddc:004 open_access

Quantifying Bounds in Strategy Logic Fijalkow, Nathanaël Maubert, Bastien Murano, Aniello Rubin, Sasha Prompt LTL Strategy Logic Model checking Automata with counters Program synthesis constructs programs from specifications in an automated way. Strategy Logic (SL) is a powerful and versatile specification language whose goal is to give theoretical foundations for program synthesis in a multi-agent setting. One limitation of Strategy Logic is that it is purely qualitative. For instance it cannot specify quantitative properties of executions such as "every request is quickly granted", or quantitative properties of trees such as "most executions of the system terminate". In this work, we extend Strategy Logic to include quantitative aspects in a way that can express bounds on "how quickly" and "how many". We define Prompt Strategy Logic, which encompasses Prompt LTL (itself an extension of LTL with a prompt eventuality temporal operator), and we define Bounded-Outcome Strategy Logic which has a bounded quantifier on paths. We supply a general technique, based on the study of automata with counters, that solves the model-checking problems for both these logics. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Nathanaël Fijalkow and Bastien Maubert and Aniello Murano and Sasha Rubin 2018 Is Part Of LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2018.23 urn:nbn:de:0030-drops-96901 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.23 eng https://creativecommons.org/licenses/by/3.0/legalcode