4 papers · 1 filter
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…
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…
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…