7 citations · 8 across the 9 of their papers we have counts for
15 papers
Formal Verification of Probabilistic Multi-Agent Systems for Ballistic Rocket Flight Using Probabilistic Alternating-Time Temporal Logic
Damian Kurpiewski, Jędrzej Michalczyk, Wojciech Jamroga +2
This technical report presents a comprehensive formal verification approach for probabilistic agent systems modeling ballistic rocket flight trajectories using Probabilistic Altern…
Towards Assume-Guarantee Verification of Abilities in Stochastic Multi-Agent Systems
Wojciech Jamroga, Damian Kurpiewski, Łukasz Mikulski
Model checking of strategic abilities is a notoriously hard problem, even more so in the realistic case of agents with imperfect information, acting in a stochastic environment. As…
Asynchronous Agents with Perfect Recall: Model Reductions, Knowledge-Based Construction, and Model Checking for Coalitional Strategies
Dilian Gurov, Filip Jamroga, Wojciech Jamroga +4
Model checking of strategic abilities for agents with memory is a notoriously hard problem, and very few attempts have been made to tackle it. In this paper, we present two importa…
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…
Pretty Good Strategies and Where to Find Them
Wojciech Jamroga, Damian Kurpiewski
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…
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…
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…
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…
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…
Fixpoint Approximation of Strategic Abilities under Imperfect Information
Wojciech Jamroga, Michał Knapik, Damian Kurpiewski
Model checking of strategic ability under imperfect information is known to be hard. The complexity results range from NP-completeness to undecidability, depending on the precise s…
Approximating Strategic Abilities under Imperfect Information: a Naive Approach
Wojciech Jamroga, Michał Knapik, Damian Kurpiewski
Alternating-time temporal logic (ATL) allows to specify requirements on abilities that different agents should (or should not) possess in a multi-agent system. However, model check…