Arrow Research search

Author name cluster

Wojtek Jamroga

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.

10 papers
1 author row

Possible papers

10

AAMAS Conference 2024 Conference Paper

Verification of Stochastic Multi-Agent Systems with Forgetful Strategies

  • Francesco Belardinelli
  • Wojtek Jamroga
  • Munyque Mittelmann
  • Aniello Murano

Intelligent autonomous agents need to reason about different kinds of uncertainty in a Multi-Agent System (MAS): first, due to the occurrence of randomization and, second, their inability to completely observe the state of the system. In this paper, we investigate the verification of system specifications in probabilistic variants of the logics ATL and ATL∗ under imperfect information (II). The resulting setting combines these two sources of uncertainty and captures the situation in which agents have qualitative uncertainty about the local state as well as quantitative uncertainty about the occurrence of future events. Since the model-checking problem is undecidable when considered in the context of strategies with perfect recall, we focus on memoryless (positional) strategies. As the main result, we show that, in stochastic MAS under II, model-checking Probabilistic ATL is in EXPTIME when agents play probabilistic strategies. Filling the gap in recent work, we also show that model-checking Probabilistic ATL∗ is PSPACE-complete when the proponent coalition is restricted to deterministic strategies.

PDF

Highlights Conference 2022 Conference Abstract

A Survey of Requirements for COVID-19 Mitigation Strategies

  • Wojtek Jamroga

The COVID-19 pandemic has influenced virtually all aspects of our lives. Across the world, countries have applied various mitigation strategies, based on social, political, and technological instruments. It seemed clear at the first glance what all those measures have been trying to achieve, and what the criteria of success are. But is it really that clear? Quoting various media sources, with COVID we had to fight an unprecedented threat to *health* and *economic stability*. While fighting it, we should protect *privacy*, *equality* and *fairness*, as well as do a coordinated assessment of *usefulness*, *effectiveness*, *technological readiness*, *cyber-security risks*, and threats to *fundamental freedoms* and *human rights*. Taken together, this is hardly a straightforward set of goals and requirements. We postulate that modal logics for multi-agent systems provide a common platform to study (and balance) essential properties of pandemic mitigation strategies. We also show how one can obtain a list of such properties by ``distilling'' them from media snippets. Finally, we present a preliminary take on their formal specification. (Joint work with David Mestel, Peter B. Roenne, Peter Y. A. Ryan, and Marjan Skrobot)

Details

AAMAS Conference 2022 Conference Paper

Reasoning about Human-Friendly Strategies in Repeated Keyword Auctions

  • Francesco Belardinelli
  • Wojtek Jamroga
  • Vadim Malvone
  • Munyque Mittelmann
  • Aniello Murano
  • Laurent Perrussel

In online advertising, search engines sell ad placements for keywords continuously through auctions. This problem can be seen as an infinitely repeated game since the auction is executed whenever a user performs a query with the keyword. As advertisers may frequently change their bids, the game will have a large set of equilibria with potentially complex strategies. In this paper, we propose the use of natural strategies for reasoning in such setting as they are processable by artificial agents with limited memory and/or computational power as well as understandable by human users. To reach this goal, we introduce a quantitative version of Strategy Logic with natural strategies in the setting of imperfect information. In a first step, we show how to model strategies for repeated keyword auctions and take advantage of the model for proving properties evaluating this game. In a second step, we study the logic in relation to the distinguishing power, expressivity, and model-checking complexity for strategies with and without recall.

PDF

Highlights Conference 2018 Conference Abstract

Towards Partial Order Reductions for Strategic Ability

  • Wojtek Jamroga

ABSTRACT. Alternating-time temporal logic ATL* and its fragment ATL extend temporal logic with the notion of strategic ability. However, there are two caveats. First, many tools and algorithmic solutions focus on agents with perfect information. This is clearly unrealistic in all but the simplest multi-agent scenarios (though somewhat easy to understand, since model checking of ATL variants with imperfect information is both theoretically and practically hard). Secondly, the semantics of strategic logics are almost exclusively based on synchronous concurrent game models. Still, many real-life systems are inherently asynchronous. No less importantly, many systems that are synchronous at the implementation level can be more conveniently modeled as asynchronous on a more abstract level. In this paper, we make the first step towards strategic analysis of asynchronous systems with imperfect information. Our contribution is threefold. First, we define a semantics of strategic abilities for agents in asynchronous systems, with and without perfect information. Secondly, we present some general complexity results for verification of strategic abilities in such systems. Thirdly, and most importantly, we adapt *partial order reduction (POR)* to model checking of strategic abilities for agents with imperfect information. We also demonstrate that POR allows to significantly reduce the size of the model, and thus to make the verification more feasible. In fact, we show that the most efficient known variant of POR, defined for linear time logic LTL, can be applied almost directly. The (nontrivial) proof that the LTL reductions work also for the more expressive strategic operators is the main contribution of this paper. Interestingly, it turns out that the scheme does *not* work for ATL with perfect information strategies. Until now, virtually all the results have suggested that verification of strategic abilities is significantly easier for agents with perfect information. Thus, we identify an aspect of verification that might be in favor of imperfect information strategies in some contexts. (This is joint work with Wojciech Penczek, Piotr Dembiński, and Antoni Mazurkiewicz, to appear soon at AAMAS 2018)

Details

Highlights Conference 2015 Conference Abstract

State and Path Coalition Effectivity Models of Concurrent Multi-Player Games

  • Wojtek Jamroga

We consider models of multi-player games where abilities of players and coalitions are defined in terms of sets of outcomes which they can effectively enforce. We extend the well studied state effectivity models of one-step games in two different ways. On the one hand, we develop multiple state effectivity functions associated with different long-term temporal operators. On the other hand, we define and study coalitional path effectivity models where the outcomes of strategic plays are infinite paths. For both extensions we obtain representation results with respect to concrete models arising from concurrent game structures. We also apply state and path coalitional effectivity models to provide alternative, arguably more natural and elegant semantics to the alternating-time temporal logic ATL*, and discuss their technical and conceptual advantages.

Details

Highlights Conference 2013 Conference Abstract

Strategic games and truly playable effectivity functions

  • Valentin Goranko
  • Wojtek Jamroga
  • Paolo Turrini

A well-known result states that every strategic game generates a playable effectivity function, and every playable effectivity function can be implemented with a strategic game. We show that the latter does not hold for infinite games. We identify the error in the proof, and present examples of playable effectivity functions for which no equivalent strategic game exists. Then, we characterize the class of *truly playable* functions that do correspond to strategic games. We also show that Coalition Logic cannot distinguish between the two classes, and we extend it to a logic that is expressive enough.

PDF Details

AAMAS Conference 2008 Conference Paper

A Temporal Logic for Markov Chains

  • Wojtek Jamroga

Most models of agents and multi-agent systems include information about possible states of the system (that defines relations between states and their external characteristics), and information about relationships between states. Qualitative models of this kind assign no numerical measures to these relationships. At the same time, quantitative models assume that the relationships are measurable, and provide numerical information about the degrees of relations. In this paper, we explore the analogies between some qualitative and quantitative models of agents/processes, especially those between transition systems and Markovian models. Typical analysis of Markovian models of processes refers only to the expected utility that can be obtained by the process. On the other hand, modal logic offers a systematic method of describing phenomena by combining various modal operators. Here, we try to exploit linguistic features, offered by propositional modal logic, for analysis of Markov chains and Markov decision processes. To this end, we propose Markov temporal logic – a multi-valued logic that extends the branching time logic ctl*.

PDF