scholarly journals Reasoning About Agents That May Know Other Agents’ Strategies

2021 ◽  
Author(s):  
Francesco Belardinelli ◽  
Sophia Knight ◽  
Alessio Lomuscio ◽  
Bastien Maubert ◽  
Aniello Murano ◽  
...  
Keyword(s):  
Model Checking ◽  
Strategic Reasoning ◽  
Strategy Logic ◽  
Strategic Ability

We study the semantics of knowledge in strategic reasoning. Most existing works either implicitly assume that agents do not know one another’s strategies, or that all strategies are known to all; and some works present inconsistent mixes of both features. We put forward a novel semantics for Strategy Logic with Knowledge that cleanly models whose strategies each agent knows. We study how adopting this semantics impacts agents’ knowledge and strategic ability, as well as the complexity of the model-checking problem.

scholarly journals Probabilistic Strategy Logic

2019 ◽  
Author(s):  
Benjamin Aminof ◽  
Marta Kwiatkowska ◽  
Bastien Maubert ◽  
Aniello Murano ◽  
Sasha Rubin
Keyword(s):  
Model Checking ◽  
Nash Equilibria ◽  
Stochastic Systems ◽  
Solution Concepts ◽  
Imperfect Recall ◽  
Double Exponential ◽  
Temporal Operator ◽  
Standard Solution ◽  
Strategy Logic ◽  
Exponential Space

We introduce Probabilistic Strategy Logic, an extension of Strategy Logic for stochastic systems. The logic has probabilistic terms that allow it to express many standard solution concepts, such as Nash equilibria in randomised strategies, as well as constraints on probabilities, such as independence. We study the model-checking problem for agents with perfect- and imperfect-recall. The former is undecidable, while the latter is decidable in space exponential in the system and triple-exponential in the formula. We identify a natural fragment of the logic, in which every temporal operator is immediately preceded by a probabilistic operator, and show that it is decidable in space exponential in the system and the formula, and double-exponential in the nesting depth of the probabilistic terms. Taking a fixed nesting depth, this gives a fragment that still captures many standard solution concepts, and is decidable in exponential space.

scholarly journals Verification of Broadcasting Multi-Agent Systems against an Epistemic Strategy Logic

2017 ◽  
Author(s):  
Francesco Belardinelli ◽  
Alessio Lomuscio ◽  
Aniello Murano ◽  
Sasha Rubin
Keyword(s):  
Model Checking ◽  
Secret Sharing ◽  
Imperfect Information ◽  
Multi Agent Systems ◽  
Perfect Recall ◽  
Agent Systems ◽  
Multi Agent ◽  
Strategy Logic

We study a class of synchronous, perfect-recall multi-agent systemswith imperfect information and broadcasting (i.e., fully observableactions). We define an epistemic extension of strategy logic withincomplete information and the assumption of uniform and coherentstrategies. In this setting, we prove that the model checking problem,and thus rational synthesis, is decidable with non-elementarycomplexity. We exemplify the applicability of the framework on arational secret-sharing scenario.

scholarly journals Parameterised Resource-Bounded ATL

2020 ◽  
Vol 34 (05) ◽  
pp. 7040-7046
Author(s):  
Natasha Alechina ◽  
Stéphane Demri ◽  
Brian Logan
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Parameter Extraction ◽  
Resource Requirement ◽  
Extraction Algorithm ◽  
Resource Requirements ◽  
Strategic Ability ◽  
Resource Logics

It is often advantageous to be able to extract resource requirements in resource logics of strategic ability, rather than to verify whether a fixed resource requirement is sufficient for achieving a goal. We study Parameterised Resource-Bounded Alternating Time Temporal Logic where parameter extraction is possible. We give a parameter extraction algorithm and prove that the model-checking problem is 2EXPTIME-complete.

Nondeterministic Strategies and their Refinement in Strategy Logic

2020 ◽  
Author(s):  
Giuseppe De Giacomo ◽  
Bastien Maubert ◽  
Aniello Murano
Keyword(s):  
Model Checking ◽  
Nash Equilibria ◽  
Computational Cost ◽  
Strategy Logic ◽  
State Of Affairs

Nondeterministic strategies are strategies (or protocols, or plans) that, given a history in a game, assign a set of possible actions, all of which are 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 refinement of Nash equilibria.

scholarly journals ATL Strategic Reasoning Meets Correlated Equilibrium

2017 ◽  
Author(s):  
Xiaowei Huang ◽  
Ji Ruan
Keyword(s):  
Model Checking ◽  
Correlated Equilibrium ◽  
Model Checker ◽  
Strategic Reasoning ◽  
Rational Agents ◽  
Software Model ◽  
Utilitarian Value ◽  
Total Rewards ◽  
Joint Strategy ◽  
Car Accident

This paper is motivated by analysing a Google self-driving car accident, i.e., the car hit a bus, with the framework and the tools of strategic reasoning by model checking. First of all, we find that existing ATL model checking may find a solution to the accident with {\it irrational} joint strategy of the bus and the car. This leads to a restriction of treating both the bus and the car as rational agents, by which their joint strategy is an equilibrium of certain solution concepts. Second, we find that a randomly-selected joint strategy from the set of equilibria may result in the collision of the two agents, i.e., the accident. Based on these, we suggest taking Correlated Equilibrium (CE) as agents' joint stratgey and optimising over the utilitarian value which is the expected sum of the agents' total rewards. The language ATL is extended with two new modalities to express the existence of an CE and a unique CE, respectively. We implement the extension into a software model checker and use the tool to analyse the examples in the paper. We also study the complexity of the model checking problems.

scholarly journals Satisfiability in Strategy Logic Can Be Easier than Model Checking

2019 ◽  
Vol 33 ◽  
pp. 2638-2645 ◽  
Author(s):  
Erman Acar ◽  
Massimo Benerecetti ◽  
Fabio Mogavero
Keyword(s):  
Model Checking ◽  
Order Logic ◽  
First Order Logic ◽  
Multi Agent Systems ◽  
First Order ◽  
Systems Model ◽  
Multi Agent ◽  
Decidable Fragment ◽  
Game Theoretic ◽  
Strategy Logic

In the design of complex systems, model-checking and satisfiability arise as two prominent decision problems. While model-checking requires the designed system to be provided in advance, satisfiability allows to check if such a system even exists. With very few exceptions, the second problem turns out to be harder than the first one from a complexity-theoretic standpoint. In this paper, we investigate the connection between the two problems for a non-trivial fragment of Strategy Logic (SL, for short). SL extends LTL with first-order quantifications over strategies, thus allowing to explicitly reason about the strategic abilities of agents in a multi-agent system. Satisfiability for the full logic is known to be highly undecidable, while model-checking is non-elementary.The SL fragment we consider is obtained by preventing strategic quantifications within the scope of temporal operators. The resulting logic is quite powerful, still allowing to express important game-theoretic properties of multi-agent systems, such as existence of Nash and immune equilibria, as well as to formalize the rational synthesis problem. We show that satisfiability for such a fragment is PSPACE-COMPLETE, while its model-checking complexity is 2EXPTIME-HARD. The result is obtained by means of an elegant encoding of the problem into the satisfiability of conjunctive-binding first-order logic, a recently discovered decidable fragment of first-order logic.

Sign in / Sign up

Export Citation Format

Share Document