Arrow Research search

Author name cluster

Damian Kurpiewski

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

13 papers
2 author rows

Possible papers

13

IJCAI Conference 2025 Conference Paper

Approximate Verification of Strategic Abilities under Imperfect Information Using Local Models

  • Damian Kurpiewski
  • Wojciech Jamroga
  • Yan Kim

Verification of strategic ability under imperfect information is challenging, with complexity ranging from NP-complete to undecidable. This is partly because traditional fixpoint equivalences fail in this setting. Some years ago, an interesting idea of fixpoint approximation was proposed for model checking of ATL_ir, i. e. , the logic of strategic ability for agents with imperfect information and imperfect recall. In this paper, we propose a new variant of the approximation, that uses the agent's local model rather than the global model of the system. We prove correctness of the construction, and demonstrate its effectiveness through experimental results on scalable models of voting.

PDF Details DOI

IJCAI Conference 2025 Conference Paper

NatSTV: Towards Verification of Natural Strategic Ability

  • Mateusz Kamiński
  • Damian Kurpiewski
  • Wojciech Jamroga

We present NatSTV, a tool for approximate verification of natural strategic ability in multi-agent systems. The tool builds on our model checker STV (STrategic Verifier), and implements heuristic synthesis of natural strategies for asynchronous agents with imperfect information and recall. All of that is available through a web interface, with no need to install or configure the software by the user.

PDF Details DOI

ECAI Conference 2024 Conference Paper

STV+FLY: On-the-Fly Model Checking of Strategic Ability in Multi-Agent Systems

  • Damian Kurpiewski
  • Mateusz Kaminski
  • Wojciech Jamroga

In this paper, we present a substantially enhanced version of our software tool STV (STrategic Verifier), dedicated to strategy synthesis and model checking of strategic abilities in multi-agent systems. The new extension, called STV+FLY, incorporates an advanced strategy synthesis algorithm that enables model checking with on-the-fly generation of the global model. This innovative approach allows for the verification of some strategic properties without generating the entire global state space, thus avoiding an important bottleneck and significantly improving the efficiency.

Details

AAMAS Conference 2024 Conference Paper

STV+KH: Towards Practical Verification of Strategic Ability for Knowledge and Information Flow

  • Mateusz Kamiński
  • Damian Kurpiewski
  • Wojciech Jamroga

We present an expanded version of our tool STV for model checking of strategic abilities. The new version adds support for knowledge and uncertainty operators, thus enabling the verification of properties such as privacy, anonymity, and strategic information flow. All of that is available through a web interface, with no need to install or configure the software by the user.

PDF

EUMAS Conference 2023 Conference Paper

Pretty Good Strategies and Where to Find Them

  • Wojciech Jamroga
  • Damian Kurpiewski

Abstract Synthesis of bulletproof strategies in imperfect information scenarios is a notoriously hard problem. In this paper, we suggest that it is sometimes a viable alternative to aim at “reasonably good” strategies instead. This makes sense not only when an ideal strategy cannot be found due to the complexity of the problem, but also when no winning strategy exists at all. We propose an algorithm for synthesis of such “pretty good” strategies. The idea is to first generate a surely winning strategy with perfect information, and then iteratively improve it with respect to two criteria of dominance: one based on the amount of conflicting decisions in the strategy, and the other related to the tightness of its outcome set. We focus on reachability goals and evaluate the algorithm experimentally with very promising results.

Details

AAMAS Conference 2022 Conference Paper

Towards Assume-Guarantee Verification of Strategic Ability

  • Łukasz Mikulski
  • Wojciech Jamroga
  • Damian Kurpiewski

Formal verification of strategic abilities is a hard problem. We propose to use the methodology of assume-guarantee reasoning in order to facilitate model checking of alternating-time temporal logic with imperfect information and imperfect recall.

PDF

AAMAS Conference 2019 Conference Paper

On Domination and Control in Strategic Ability

  • Damian Kurpiewski
  • Michał Knapik
  • Wojciech Jamroga

We propose a technique to compare partial strategies for agents and coalitions in multi-agent environments with imperfect information. The proposed relation mimics the game-theoretic notion of strategic dominance: a stronger partial strategy can replace a weaker one in a full strategy, while preserving the enforceability of a given goal. Our version of dominance is based on a new notion of input/output characteristics for partial strategies. Intuitively, the inputs are the states where the strategy gains control over execution, and the outputs are the states where it returns the control to the environment. Moreover, we identify the sources of dependence between partial strategies, and show conditions under which they can be analysed in a fully independent way. We evaluate our approach on two scalable benchmarks from the literature. The experiments are carried out for the tasks of incremental synthesis of uniform strategies and optimization of a winning strategy, with very promising results.

PDF

IJCAI Conference 2019 Conference Paper

Strategy Logic with Simple Goals: Tractable Reasoning about Strategies

  • Francesco Belardinelli
  • Wojciech Jamroga
  • Damian Kurpiewski
  • Vadim Malvone
  • Aniello Murano

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.

PDF Details

AAMAS Conference 2019 Conference Paper

STV: Model Checking for Strategies under Imperfect Information

  • Damian Kurpiewski
  • Wojciech Jamroga
  • Michał Knapik

We present an experimental tool for verification of strategic abilities under imperfect information, as well as strategy synthesis. The problem is well known to be hard, both theoretically and in practice. The tool, called StraTegic Verifier (STV), implements several recently developed algorithms to overcome the complexity.

PDF

AAMAS Conference 2017 Conference Paper

Fixpoint Approximation of Strategic Abilities under Imperfect Information

  • Wojciech Jamroga
  • Michal Knapik
  • Damian Kurpiewski

Model checking of strategic ability under imperfect information is known to be hard. In this paper, we propose translations of ATLir formulae that provide lower and upper bounds for their truth values, and are cheaper to verify than the original specifications. Most interestingly, the lower approximation is provided by a fixpoint expression that uses a nonstandard variant of the next-step ability operator. We show the correctness of the translations, establish their computational complexity, and validate the approach by experiments with a scalable scenario of Bridge play.

PDF