License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2018.23
URN: urn:nbn:de:0030-drops-96901
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9690/
Go to the corresponding LIPIcs Volume Portal

Fijalkow, Nathanaël ; Maubert, Bastien ; Murano, Aniello ; Rubin, Sasha

Quantifying Bounds in Strategy Logic

pdf-format:
LIPIcs-CSL-2018-23.pdf (0.6 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{fijalkow_et_al:LIPIcs:2018:9690,
  author =	{Nathana{\"e}l Fijalkow and Bastien Maubert and Aniello Murano and Sasha Rubin},
  title =	{{Quantifying Bounds in Strategy Logic}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic  (CSL 2018)},
  pages =	{23:1--23:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Dan Ghica and Achim Jung},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9690},
  URN =		{urn:nbn:de:0030-drops-96901},
  doi =		{10.4230/LIPIcs.CSL.2018.23},
  annote =	{Keywords: Prompt LTL, Strategy Logic, Model checking, Automata with counters}
}

Keywords: Prompt LTL, Strategy Logic, Model checking, Automata with counters
Collection: 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)
Issue Date: 2018
Date of publication: 29.08.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI