11 citations · 44 across the 24 of their papers we have counts for
32 papers
Multi-Valued Verification of Strategic Ability
Wojciech Jamroga, Beata Konikowska, Damian Kurpiewski +1
Some multi-agent scenarios call for the possibility of evaluating specifications in a richer domain of truth values. Examples include runtime monitoring of a temporal property over…
STV+Reductions: Towards Practical Verification of Strategic Ability Using Model Reductions
Damian Kurpiewski, Witold Pazderski, Wojciech Jamroga +1
We present a substantially expanded version of our tool STV for strategy synthesis and verification of strategic abilities. The new version adds user-definable models and support f…
A Declaration of Software Independence
Wojciech Jamroga, Peter Y. A. Ryan, Steve Schneider +2
A voting system should not merely report the outcome: it should also provide sufficient evidence to convince reasonable observers that the reported outcome is correct. Many deploye…
Strategic Abilities of Forgetful Agents in Stochastic Environments
Francesco Belardinelli, Wojciech Jamroga, Munyque Mittelmann +1
In this paper, we investigate the probabilistic variants of the strategy logics ATL and ATL* under imperfect information. Specifically, we present novel decidability and complexity…
Computationally Feasible Strategies
Catalin Dima, Wojciech Jamroga
Real-life agents seldom have unlimited reasoning power. In this paper, we propose and study a new formal notion of computationally bounded strategic ability in multi-agent systems.…
Scalable Verification of Strategy Logic through Three-valued Abstraction
Francesco Belardinelli, Angelo Ferrando, Wojciech Jamroga +2
The model checking problem for multi-agent systems against Strategy Logic specifications is known to be non-elementary. On this logic several fragments have been defined to tackle…
MsATL: a Tool for SAT-Based ATL Satisfiability Checking
Artur Niewiadomski, Magdalena Kacprzak, Damian Kurpiewski +3
We present MsATL: the first tool for deciding the satisfiability of Alternating-time Temporal Logic (ATL) with imperfect information. MsATL combines SAT Modulo Monotonic Theories s…
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-t…
Assume-Guarantee Verification of Strategic Ability
Łukasz Mikulski, Wojciech Jamroga, Damian Kurpiewski
Model checking of strategic abilities is a notoriously hard problem, even more so in the realistic case of agents with imperfect information. Assume-guarantee reasoning can be of g…
Verification of Multi-Agent Properties in Electronic Voting: A Case Study
Damian Kurpiewski, Wojciech Jamroga, Łukasz Maśko +4
Formal verification of multi-agent systems is hard, both theoretically and in practice. In particular, studies that use a single verification technique typically show limited effic…
Practical Model Reductions for Verification of Multi-Agent Systems
Wojciech Jamroga, Yan Kim
Formal verification of intelligent agents is often computationally infeasible due to state-space explosion. We present a tool for reducing the impact of the explosion by means of s…
Pretty Good Strategies for Benaloh Challenge
Wojciech Jamroga
Benaloh challenge allows the voter to audit the encryption of her vote, and in particular to check whether the vote has been represented correctly. An interesting analysis of the m…
Playing to Learn, or to Keep Secret: Alternating-Time Logic Meets Information Theory
Masoud Tabatabaei, Wojciech Jamroga
Many important properties of multi-agent systems refer to the participants' ability to achieve a given goal, or to prevent the system from an undesirable event. Among intelligent a…
Strategic (Timed) Computation Tree Logic
Jaime Arias, Wojciech Jamroga, Wojciech Penczek +2
We define extensions of CTL and TCTL with strategic operators, called Strategic CTL (SCTL) and Strategic TCTL (STCTL), respectively. For each of the above logics we give a synchron…
Towards Modelling and Verification of Social Explainable AI
Damian Kurpiewski, Wojciech Jamroga, Teofil Sidoruk
Social Explainable AI (SAI) is a new direction in artificial intelligence that emphasises decentralisation, transparency, social context, and focus on the human users. SAI research…
Verification of the Socio-Technical Aspects of Voting: The Case of the Polish Postal Vote 2020
Wojciech Jamroga, Peter Y. A. Ryan, Yan Kim
Voting procedures are designed and implemented by people, for people, and with significant human involvement. Thus, one should take into account the human factors in order to compr…
Bisimulations for Verifying Strategic Abilities with an Application to the ThreeBallot Voting Protocol
Francesco Belardinelli, Rodica Condurache, Catalin Dima +2
We propose a notion of alternating bisimulation for strategic abilities under imperfect information. The bisimulation preserves formulas of ATL for both the {\em objective} and…
STV+AGR: Towards Practical Verification of Strategic Ability Using Assume-Guarantee Reasoning
Damian Kurpiewski, Łukasz Mikulski, Wojciech Jamroga
We present a substantially expanded version of our tool STV for strategy synthesis and verification of strategic abilities. The new version provides a web interface and support for…
Practical Abstraction for Model Checking of Multi-Agent Systems
Wojciech Jamroga, Yan Kim
Model checking of multi-agent systems (MAS) is known to be hard, both theoretically and in practice. A smart abstraction of the state space may significantly reduce the model, and…
Reasoning about Human-Friendly Strategies in Repeated Keyword Auctions
Francesco Belardinelli, Wojtek Jamroga, Vadim Malvone +3
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 ex…
Convergence Voting: From Pairwise Comparisons to Consensus
Gergei Bana, Wojciech Jamroga, David Naccache +1
An important aspect of AI design and ethics is to create systems that reflect aggregate preferences of the society. To this end, the techniques of social choice theory are often ut…
A Survey of Requirements for COVID-19 Mitigation Strategies. Part I: Newspaper Clips
Wojciech Jamroga, David Mestel, Peter B. Roenne +2
The COVID-19 pandemic has influenced virtually all aspects of our lives. Across the world, countries have applied various mitigation strategies for the epidemic, based on social, p…
Natural Strategic Abilities in Voting Protocols
Wojciech Jamroga, Damian Kurpiewski, Vadim Malvone
Security properties are often focused on the technological side of the system. One implicitly assumes that the users will behave in the right way to preserve the property at hand.…
Model Checkers Are Cool: How to Model Check Voting Protocols in Uppaal
Wojciech Jamroga, Yan Kim, Damian Kurpiewski +1
The design and implementation of an e-voting system is a challenging task. Formal analysis can be of great help here. In particular, it can lead to a better understanding of how th…