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: | 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. |
Pages: | 15 |
Talk: | Jul 08 16:00 (Session 42Q: Strategy Logic) |
Paper: |