The Team

Prof. Peter Y. A. Ryan, co-PI

  • The leader of the Luxembourgish part of the project. Key areas: information security, in particular coercion-resistant and voter-verifiable voting protocols.
  • Personal website

Prof. Wojciech Jamroga, co-PI

  • The leader of the Polish part of the project. Key areas: logical methods for specification and verification of multi-agent systems, as well as game-theoretic models of MAS.
  • Personal website

Prof. Wojciech Penczek

  • Key areas: models of distributed systems, multi-agent systems, modelling of knowledge and belief, temporal logics, automated verification, planning, and model checking of concurrent systems.
  • Personal website

Michał Knapik, PhD, research associate (postdoc)

  • Key areas: model checking for temporal and strategic logics; formal methods for multi-agent systems.
  • Personal website

Gabriele Lenzini, PhD

  • Key areas: modelling, analysis and design of secure and trustworthy systems, analysis of security in socio-technical systems.
  • Personal website

Damian Kurpiewski, MSc, PhD student

  • Key areas: modelling and analysis of complex systems, algorithms for model-checking, tool development.
  • Personal website

Teofil Sidoruk, MSc, PhD student

  • Key areas: state space reduction methods, model checking of multi-agent systems.

Yan Kim, MSc, PhD student

  • Key areas: modelling and analysis of voting protocols.

Prof. Marek Bednarczyk

  • Key areas: algorithms for parallel computation and automated search.

Tadeusz Puźniakowski, PhD

  • Key areas: algorithms for parallel computation and automated search.
  • Personal website

Łukasz Mikulski, PhD

  • Key areas: reduction methods, model-checking algorithms, optimization methods.

Witold Pazderski, MSc, PhD student

  • Key areas: tool development.

Peter Roenne, PhD

  • Key areas: cryptography and design of e-voting protocols.

David Mestel, PhD

  • Key areas: information security, quantified information flow.

Associated Researchers

Łukasz Maśko, PhD

Masoud Tabatabaei, PhD

Publications and Software


MsATL: A Tool for SAT-Based ATL Satisfiability Checking
Artur Niewiadomski, Magdalena Kacprzak, Damian Kurpiewski, Michał Knapik, Wojciech Penczek, Wojciech Jamroga; AAMAS 2020: 2111-2113
Towards Model Checking of Voting Protocols in Uppaal
Wojciech Jamroga, Yan Kim, Damian Kurpiewski, Peter Y. A. Ryan; E-Vote-ID 2020: 129-146
Natural Strategic Abilities in Voting Protocols
Wojciech Jamroga, Damian Kurpiewski, Vadim Malvone; STAST 2020
Multi-valued Verification of Strategic Ability
Wojciech Jamroga, Beata Konikowska, Damian Kurpiewski, Wojciech Penczek; Fundam. Informaticae 175(1-4): 207-251
Towards Partial Order Reductions for Strategic Ability
Wojciech Jamroga, Wojciech Penczek, Teofil Sidoruk, Piotr Dembinski, Antoni W. Mazurkiewicz; J. Artif. Intell. Res. 68: 817-850
SAT-Based ATL Satisfiability Checking
Magdalena Kacprzak, Artur Niewiadomski, Wojciech Penczek; KR 2020


StraTegic Verifier (STV)
STV is a prototype tool aimed at verification of strategic abilities in multi-agent systems, and synthesis of strategies that guarantee a given temporal goal.
MsATL is a prototype tool for deciding the satisfiability of Alternating-time Temporal Logic (ATL) with imperfect information. MsATL combines SAT Modulo Monotonic Theories solvers with existing ATL model checkers: MCMAS and STV. The tool can deal with various semantics of ATL, including perfect and imperfect information, and can handle additional practical requirements. MsATL can be applied for synthesis of games that conform to a given specification, with the synthesised game often being minimal.