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 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 Strategy Logic with Simple Goals: Tractable Reasoning about Strategies

2019 ◽  
Author(s):  
Francesco Belardinelli ◽  
Wojciech Jamroga ◽  
Damian Kurpiewski ◽  
Vadim Malvone ◽  
Aniello Murano
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Computational Cost ◽  
Expressive Power ◽  
Game Theoretic ◽  
Strategy Logic ◽  
Tractable Reasoning

In this paper we introduce Strategy Logic with simple goals (SL[SG]), a fragment of Strategy Logic that strictly extends the well-known Alternating-time Temporal Logic ATL by introducing arbitrary quantification over the agents' strategies.  Our motivation comes from game-theoretic applications, such as expressing Stackelberg equilibria in games, coercion in voting protocols, as well as module checking for simple goals. Most importantly, we prove that the model checking problem for SL[SG] is PTIME-complete, the same as ATL. Thus, the extra expressive power comes at no computational cost as far as verification is concerned.

scholarly journals Learning Nash Equilibria in Zero-Sum Stochastic Games via Entropy-Regularized Policy Approximation

2021 ◽  
Author(s):  
Yue Guan ◽  
Qifan Zhang ◽  
Panagiotis Tsiotras
Keyword(s):  
Nash Equilibrium ◽  
Nash Equilibria ◽  
Stochastic Games ◽  
Computational Cost ◽  
Q Learning ◽  
Scheduling Scheme ◽  
Speed Up ◽  
Zero Sum ◽  
Q Function ◽  
Previous Training

We explore the use of policy approximations to reduce the computational cost of learning Nash equilibria in zero-sum stochastic games. We propose a new Q-learning type algorithm that uses a sequence of entropy-regularized soft policies to approximate the Nash policy during the Q-function updates. We prove that under certain conditions, by updating the entropy regularization, the algorithm converges to a Nash equilibrium. We also demonstrate the proposed algorithm's ability to transfer previous training experiences, enabling the agents to adapt quickly to new environments. We provide a dynamic hyper-parameter scheduling scheme to further expedite convergence. Empirical results applied to a number of stochastic games verify that the proposed algorithm converges to the Nash equilibrium, while exhibiting a major speed-up over existing algorithms.

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 Model Checking Coalition Nash Equilibria in MAD Distributed Systems

2009 ◽  
pp. 531-546 ◽  
Author(s):  
Federico Mari ◽  
Igor Melatti ◽  
Ivano Salvo ◽  
Enrico Tronci ◽  
Lorenzo Alvisi ◽  
...  
Keyword(s):  
Distributed Systems ◽  
Model Checking ◽  
Nash Equilibria

scholarly journals On Locally Strongest Assumption Generation Method for Component-Based Software Verification

2018 ◽  
Vol 34 (2) ◽  
Author(s):  
Hoang-Viet Tran ◽  
Pham Ngoc Hung
Keyword(s):  
Model Checking ◽  
Large Scale ◽  
Software Verification ◽  
Software Evolution ◽  
Computational Cost ◽  
Experimental Results ◽  
Correctness Proof ◽  
Containment Problem ◽  
Membership Queries ◽  
Language Containment

Assume-guarantee reasoning, a well-known approach in component-based software (CBS) verification, is infact a language containment problem whose computational cost depends on the sizes of languages of the softwarecomponents under checking and the assumption to be generated. Therefore, the smaller language assumptions,the more computational cost we can reduce in software verification. Moreover, strong assumptions are moreimportant in CBS verification in the context of software evolution because they can be reused many times in theverification process. For this reason, this paper presents a method for generating locally strongest assumptions withlocally smallest languages during CBS verification. The key idea of this method is to create a variant techniquefor answering membership queries of the Teacher when responding to the Learner in the L–based assumptionlearning process. This variant technique is then integrated into an algorithm in order to generate locally strongestassumptions. These assumptions will effectively reduce the computational cost when verifying CBS, especiallyfor large–scale and evolving ones. The correctness proof, experimental results, and some discussions about theproposed method are also presented.Keywords: Assume-guarantee reasoning, Model checking, Component-based software verification, Locallystrongest assumptions, Locally smallest language assumptions.

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 Model Checking Nash Equilibria in MAD Distributed Systems

2008 ◽  
Author(s):  
Federico Mari ◽  
Igor Melatti ◽  
Ivano Salvo ◽  
Enrico Tronci ◽  
Lorenzo Alvisi ◽  
...  
Keyword(s):  
Distributed Systems ◽  
Model Checking ◽  
Nash Equilibria

scholarly journals Synthesis of Controllable Nash Equilibria in Quantitative Objective Game

2018 ◽  
Author(s):  
Shaull Almagor ◽  
Orna Kupferman ◽  
Giuseppe Perelli
Keyword(s):  
Social Choice ◽  
Nash Equilibria ◽  
Price Of Anarchy ◽  
Decision Procedures ◽  
Price Of Stability ◽  
Multi Agent System ◽  
Agent System ◽  
Multi Agent ◽  
Real Value ◽  
Strategy Logic

In Rational Synthesis, we consider a multi-agent system in which some of the agents are controllable and some are not. All agents have objectives, and the goal is to synthesize strategies for the controllable agents so that their objectives are satisfied, assuming rationality of the uncontrollable agents. Previous work on rational synthesis considers objectives in LTL, namely ones that describe on-going behaviors, and in Objective-LTL, which allows ranking of LTL formulas. In this paper, we extend rational synthesis to LTL[F] -- an extension of LTL by quality operators. The satisfaction value of an LTL[F] formula is a real value in [0,1], where the higher the value is, the higher is the quality in which the computation satisfies the specification. The extension significantly strengthens the framework of rational synthesis and enables a study its game- and social-choice theoretic aspects. In particular, we study the price of stability and price of anarchy of the rational-synthesis game and use them to explain the cooperative and non-cooperative settings of rational synthesis. Our algorithms make use of strategy logic and decision procedures for it. Thus, we are able to handle the richer quantitative setting using existing tools. In particular, we show that the cooperative and non-cooperative versions of quantitative rational synthesis are 2EXPTIME-complete and in 3EXPTIME, respectively -- not harder than the complexity known for their Boolean analogues.

Sign in / Sign up

Export Citation Format

Share Document