9 citations · 21 across the 5 of their papers we have counts for
6 papers
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…
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…
Modular Analysis of Tree-Topology Models
Laure Petrucci, Michał Knapik
We investigate networks of automata that synchronise over common action labels. A graph synchronisation topology between the automata is defined in such a way that two automata are…
Parametric Verification: An Introduction
Étienne André, Michał Knapik, Didier Lime +2
This paper constitutes a short introduction to parametric verification of concurrent systems. It originates from two 1-day tutorial sessions held at the Petri nets conferences in T…
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…