Quantifying Bounds in Strategy Logic

Authors: Nathanaƫl Fijalkow, Bastien Maubert, Aniello Murano and Sasha Rubin

Paper Information

Title:Quantifying Bounds in Strategy Logic
Authors:Nathanaƫl Fijalkow, Bastien Maubert, Aniello Murano and Sasha Rubin
Proceedings:SR SR18 papers
Editors: Nicolas Markey and Patricia Bouyer
Keywords:Prompt LTL, Strategy Logic, Model checking, Automata with counters, Verification

ABSTRACT. Program synthesis automatically constructs programs from specifications. Strategy Logic is a powerful 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.

Talk:Jul 08 16:00 (Session 42Q: Strategy Logic)