arXiv subjects

Fabio Mogavero

Publications and source records attributed to Fabio Mogavero.

25 records · Page 2Linked to original sources

arXiv2014

MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications

We introduce MCMAS-SLK, a BDD-based model checker for the verification of systems against specifications expressed in a novel, epistemic variant of strategy logic. We give syntax and semantics of the specification language and introduce a labelling algorithm for epistemic and strategy logic modalities. We provide details of the checker which can also be used for synthesising agents' strategies so that a specification is satisfied by the system. We evaluate the efficiency of the implementation by discussing the results obtained for the dining cryptographers protocol and a variant of the cake-cutting problem.

cs.LO↗

arXiv2014

On the Remarkable Features of Binding Forms

Hilbert's Entscheidungsproblem has given rise to a broad and productive line of research in mathematical logic, where the classification process of decidable classes of first-order sentences represent only one of the remarkable results. According to the criteria used to identify the particular classes of interest, this process was declined into several research programs, of which some of the most deeply investigated are the ones classifying sentences in prenex normal form in base of their prefix vocabulary. Unfortunately, almost all of these approaches did not shed any light on the reasons why modal logic is so robustly decidable. Trying to answer to this question, Andreka, van Benthem, and Nemeti introduced the guarded fragment of first-order logic, which generalizes the modal framework by essentially retaining all its fundamental properties. They started, so, a completely new research program based on the way quantifications can be relativized. Although this approach succeeded in its original task, we cannot consider it satisfactory in spotting the reasons why some complex extensions of modal logic are well-behaved. In particular, by just using the related results, we are not able to derive the decidability of multi-agent logics for strategic abilities. In this paper, aiming to lay the foundation for a more thorough understanding of some of these decidability questions, we introduce a new kind of classification based on the binding forms that are admitted in a sentence, i.e., on the way the arguments of a relation can be bound to a variable. We describe a hierarchy of first-order fragments based on the Boolean combinations of these forms, showing that the less expressive one is already incomparable with the guarded logic and related extensions. We also prove, via a new model-theoretic technique, that it enjoys the finite-model property and a PSpace satisfiability problem.

cs.LO↗

arXiv2014

Proceedings 2nd International Workshop on Strategic Reasoning

This volume contains the proceedings of the 2nd International Workshop on Strategic Reasoning 2014 (SR 2014), held in Grenoble (France), April 5-6, 2014. The SR workshop aims to bring together researchers, possibly with different backgrounds, working on various aspects of strategic reasoning in computer science, both from a theoretical and a practical point of view. This year SR has hosted four invited talks by Thomas A. Henzinger, Wiebe van der Hoek, Alessio R. Lomuscio, and Wolfgang Thomas. Moreover, the workshop has hosted 14 contributed talks, all selected among the full contributions submitted, which have been deeply evaluated, by four reviewers, according to their quality and relevance.

cs.GT↗

arXiv2013

Proceedings 1st International Workshop on Strategic Reasoning

This volume contains the proceedings of the 1st International Workshop on Strategic Reasoning 2013 (SR 2013), held in Rome (Italy), March 1617, 2013. The SR workshop aims to bring together researchers, possibly with different backgrounds, working on various aspects of strategic reasoning in computer science, both from a theoretical and a practical point of view. This year SR has hosted four outstanding invited talks by Krishnendu Chatterjee, Alessio R. Lomuscio, Jean-Francois Raskin, and Michael Wooldridge. Moreover, the program committee selected 13 papers among the 23 contributions submitted. Almost all of them have been revised by three reviews and the contributions have been selected according to quality and relevance to the topics of the workshop.

cs.GT↗

arXiv2012

A Decidable Fragment of Strategy Logic

Strategy Logic (SL, for short) has been recently introduced by Mogavero, Murano, and Vardi as a useful formalism for reasoning explicitly about strategies, as first-order objects, in multi-agent concurrent games. This logic turns to be very powerful, subsuming all major previously studied modal logics for strategic reasoning, including ATL, ATL*, and the like. Unfortunately, due to its expressiveness, SL has a non-elementarily decidable model-checking problem and a highly undecidable satisfiability problem, specifically, $Σ_{1}^{1}$-Hard. In order to obtain a decidable sublogic, we introduce and study here One-Goal Strategy Logic (SL[1G], for short). This logic is a syntactic fragment of SL, strictly subsuming ATL*, which encompasses formulas in prenex normal form having a single temporal goal at a time, for every strategy quantification of agents. SL[1G] is known to have an elementarily decidable model-checking problem. Here we prove that, unlike SL, it has the bounded tree-model property and its satisfiability problem is decidable in 2ExpTime, thus not harder than the one for ATL*.

cs.LO↗

arXiv2012

Reasoning About Strategies: On the Model-Checking Problem

In open systems verification, to formally check for reliability, one needs an appropriate formalism to model the interaction between agents and express the correctness of the system no matter how the environment behaves. An important contribution in this context is given by modal logics for strategic ability, in the setting of multi-agent games, such as ATL, ATL\star, and the like. Recently, Chatterjee, Henzinger, and Piterman introduced Strategy Logic, which we denote here by CHP-SL, with the aim of getting a powerful framework for reasoning explicitly about strategies. CHP-SL is obtained by using first-order quantifications over strategies and has been investigated in the very specific setting of two-agents turned-based games, where a non-elementary model-checking algorithm has been provided. While CHP-SL is a very expressive logic, we claim that it does not fully capture the strategic aspects of multi-agent systems. In this paper, we introduce and study a more general strategy logic, denoted SL, for reasoning about strategies in multi-agent concurrent games. We prove that SL includes CHP-SL, while maintaining a decidable model-checking problem. In particular, the algorithm we propose is computationally not harder than the best one known for CHP-SL. Moreover, we prove that such a problem for SL is NonElementarySpace-hard. This negative result has spurred us to investigate here syntactic fragments of SL, strictly subsuming ATL\star, with the hope of obtaining an elementary model-checking problem. Among the others, we study the sublogics SL[NG], SL[BG], and SL[1G]. They encompass formulas in a special prenex normal form having, respectively, nested temporal goals, Boolean combinations of goals and, a single goal at a time. About these logics, we prove that the model-checking problem for SL[1G] is 2ExpTime-complete, thus not harder than the one for ATL\star.

cs.LO↗

arXiv2010

Quantitative Fairness Games

We consider two-player games played on finite colored graphs where the goal is the construction of an infinite path with one of the following frequency-related properties: (i) all colors occur with the same asymptotic frequency, (ii) there is a constant that bounds the difference between the occurrences of any two colors for all prefixes of the path, or (iii) all colors occur with a fixed asymptotic frequency. These properties can be viewed as quantitative refinements of the classical notion of fair path in a concurrent system, whose simplest form checks whether all colors occur infinitely often. In particular, the first two properties enforce equal treatment of all the jobs involved in the system, while the third one represents a way to assign a given priority to each job. For all the above goals, we show that the problem of checking whether there exists a winning strategy is CoNP-complete.

cs.GT↗