1,720,992 research outputs found
Decidability results for ATL∗ with imperfect information and perfect recall
No full textAlternating-Time Temporal Logic (ATL∗) is a central logic for multiagent systems. Its extension to the imperfect information setting (ATLJ) is well known to have an undecidable model-checking problem when agents have perfect recall. Studies have thus mostly focused either on agents without memory, or on alternative semantics to retrieve decidability. In this work we establish new decidability results for agents with perfect recall: We first prove a meta-Theorem that allows the transfer of decidability results for classes of multiplayer games with imperfect information, such as games with hierarchical observation, to the model-checking problem for ATL J. We then establish that model checking ATL∗ with strategy context and imperfect information is decidable when restricted to hierarchical instances
Towards a tool for LTL synthesis with bounded-energy constraints
No full textMCMAS is an open-source model checker specialised in logics for multi-agent systems (MAS), in particular logics for strategic reasoning, but which at the moment can only handle qualitative objectives. We propose a first step towards extending MCMAS to certain quantitative strategic logics where the quantitative aspects have the form of energy constraints. We show that the existence of strategies for a coalition of agents for objectives given as a combination of LTL formula and bounded energy constraint can be reduced to the same problem for pure LTL objectives. Using this reduction, we run some experiments with MCMAS to solve quantitative strategic problems. Copyright © 2019 for this paper by its authors
Formal Verification of Bayesian Mechanisms
No full textIn this paper, for the first time, we study the formal verification of Bayesian mechanisms through strategic reasoning. We rely on the framework of Probabilistic Strategy Logic (PSL), which is well-suited for representing and verifying multi-agent systems with incomplete information. We take advantage of the recent results on the decidability of PSL model checking under memoryless strategies, and reduce the problem of formally verifying Bayesian mechanisms to PSL model checking. We show how to encode Bayesian-Nash equilibrium and economical properties, and illustrate our approach with different kinds of mechanisms
Assume-guarantee synthesis for prompt linear temporal logic
No full textPrompt-LTL extends Linear Temporal Logic with a bounded version of the “eventually” operator to express temporal requirements such as bounding waiting times. We study assume-guarantee synthesis for prompt-LTL: the goal is to construct a system such that for all environments satisfying a first prompt-LTL formula (the assumption) the system composed with this environment satisfies a second prompt-LTL formula (the guarantee). This problem has been open for a decade. We construct an algorithm for solving it and show that, like classical LTL synthesis, it is 2-EXPTIME-complete
Public and Private Affairs in Strategic Reasoning
No full textDo agents know each others' strategies? In multi-process software construction, each process has access to the processes already constructed; but in typical human-robot interactions, a human may not announce their strategy to the robot (indeed, the human may not even know their own strategy). This question has often been overlooked when modeling and reasoning about multi-agent systems. In this work we study how it impacts strategic reasoning. To do so we consider Strategy Logic (SL), a well-established and highly expressive logic for strategic reasoning. Its usual semantics, which we call “white-box semantics”, models systems in which agents “broadcast” their strategies. By adding imperfect information to the evaluation games for the usual semantics, we obtain a new semantics called “black-box semantics”, in which agents keep their strategies private. We consider the model-checking problem and show that the black-box semantics has much lower complexity than white-box semantics for an important fragment of Strategy Logic
Reasoning about changes of observational power in logics of knowledge and time
No full textWe study dynamic changes of agents' observational power in logics of knowledge and time We consider CTL'K, the extension of CTLwith knowledge operators, and enrich it with a new operator that models a change in an agent's way of observing the system We extend the classic semantics of knowledge for agents with perfect recall to account for changes of observational power, and we show that this new operator increases the expressivity of CTL'K We reduce the model-checking problem for our logic to that for CTLK, which is known to be decidable This provides a solution to the model-checking problem for our logic, but it is not optimal, and we provide a direct model-chocking procedure with better complexity. © 2019 International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org) Ail rights reserved
Synthesis of Mechanisms with Strategy Logic (Short Paper)
No full textMechanism Design aims to design a game so that a desirable outcome is reached regardless of agents' self-interests. In this paper, we show how this problem can be rephrased as a synthesis problem, where mechanisms are automatically synthesized from a partial or complete specification in a high-level logical language. We show that Quantitative Strategy Logic is a perfect candidate for specifying mechanisms as it can express complex strategic and quantitative properties
Nondeterministic strategies and their refinement in strategy logic
No full textNondeterministic strategies are strategies (or protocols, or plans) that, given a history in a game, assign a set of possible actions, all of which should be winning. An important problem is that of refining such strategies. For instance, given a nondeterministic strategy that allows only safe executions, refine it to, additionally, eventually reach a desired state of affairs. We show that strategic problems involving strategy refinement can be solved elegantly in the framework of Strategy Logic (SL), a very expressive logic to reason about strategic abilities. Specifically, we introduce an extension of SL with nondeterministic strategies and an operator expressing strategy refinement. We show that model checking this logic can be done at no additional computational cost with respect to standard SL, and can be used to solve a variety of problems such as synthesis of maximally permissive strategies or maximally permissive Nash equilibria
Automated Synthesis of Mechanisms
No full textMechanism Design aims to design a game so that a desirable outcome is reached regardless of agents' self-interests. In this paper, we show how this problem can be rephrased as a synthesis problem, where mechanisms are automatically synthesized from a partial or complete specification in a high-level logical language. We show that Quantitative Strategy Logic is a perfect candidate for specifying mechanisms as it can express complex strategic and quantitative properties. We solve automated mechanism design in two cases: when the number of actions is bounded, and when agents play in turn
- …
