SpaceVote

Probabilistic Verification of Complex Heterogeneous Systems: From Ballots to Ballistics

The SpaceVote project is a collaboration between researchers from Institute of Computer Science, Polish Academy of Sciences, The Luxembourg University and SpaceForest. The aim of the project is to use the latest achievements in probabilistic verification to analyze phenomena as diverse as influencing voters during voting and maneuvering a simple unmanned rocket.

In the last 30 years, the world has become densely connected. Most ICT systems address a complicated network of users, vastly distributed over geographical locations and cultural contexts. What is more, ICT services are usually done by people, with people, and for people. The intensive human involvement makes them hard to describe and analyse with the standard tools of formal verification.

Voting and elections are good examples of services that are difficult to specify, hard to verify, and extremely important to the society. The democratic societies are currently facing a number of serious threats. Electoral fraud, manipulation of voters, fake news and disinformation are used to swing the outcome of elections and severely undermine the voters' trust. If democracy is to be effective, it is essential to assess and mitigate those threats. In the course of our previous projects, we have used ideas from game theory, multi-agent systems, and theory of socio-technical systems towards the goal, with considerable success. It is now time to move on to richer formalizations that allow for reasoning about more realistic models of voters and attackers, and more mathematical analysis of their possible behaviour. To this end, we will extend our techniques to quantitative analysis of voting, and combine them with the recent advances in probabilistic verification. We will also show that the methodology can be applied well beyond voting procedures, for example to better synthesize strategies for small autonomous rockets navigating in an uncertain environment.

Funded by

Project Details

Outline

The Probabilistic Verification of Complex Heterogeneous Systems: From Ballots to Ballistics (SpaceVote) is funded by NCBiR (Narodowe Centrum Badań i Rozwoju, Poland) and FNR (Fonds National de la Recherche, Luxembourg) within POLLUX/CORE scheme. SpaceVote is co-lead by Prof. Peter Y. A. Ryan (Luxembourg) and Prof. Wojciech Jamroga (Poland). Please visit the team for the list of current and past- participating researchers. This website will provide the news about the project - the published papers, talks, software, organized workshops, etc.

Description

In the last 30 years, the world has become densely connected. Most ICT systems address a complicated network of users, functionalities, and infrastructure components, vastly distributed over geographical locations and cultural contexts. This results in a considerable space of potential threats that call for systematic (and preferably machine-assisted) analysis. What is more, ICT services are usually done by people, with people, and for people. The intensive human involvement makes them hard to analyse beyond the usual computational complexity obstacles.

Voting and elections are good examples of services that are difficult to specify, hard to verify, and extremely important to the society. If democracy is to be effective, it is essential to assess and mitigate the threats of fraud, manipulation, and coercion. In the course of our previous projects VoteVerif and STV, we have used ideas from game theory, multi-agent systems, and theory of socio-technical systems to redefine and analyse requirements for voting procedures. We made significant progress towards better understanding of the interplay between technological and social components, and developed novel approaches to modelling and verification. However, our approach has been so far qualitative, in the sense that we focused on agents with binary preferences (likes/doesn't like), binary system objectives (win or lose), and nonprobabilistic behaviours. It is now time to move on to richer formalizations that address quantitative information about how much the users or attackers like a given outcome, the degree of system correctness and how to balance conflicting correctness requirements, and last but not least probabilistic strategies of participants and response of the system. This poses a significant challenge, but also brings the formal specifications closer to reality, and results in more valuable outcomes of formal analysis.

To achieve the goal, we will extend the techniques that we developed for qualitative analysis of voting, and combine them with the recent advances in probabilistic model checking. We will also show that the methodology can be applied well beyond voting procedures, for example to better synthesize strategies for small autonomous rockets navigating in an uncertain environment.

Keywords

information security, socio-technical systems, e-democracy, secure voting protocols, coercion-resistance and confidentiality, model checking and rational verification, strategy synthesis, autonomous moving objects, algorithms and tools, reliability and dynamics of trust

The team

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.

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.

Prof. Marta Kwiatkowska

Key areas: modelling and automated verification, probabilistic and quantitative verification, synthesis from quantitative specifications.

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.

Prof. Dr. Marcus VÖLP

Key areas: security, dependability, resilience, fault and intrusion tolerance, microkernel-based systems, teal-time and embedded systems, cyber-physical systems.

Özgür CEYHAN, PhD

Key areas: resilience, fault and intrusion tolerance, artificial neural networks.

Rafał Graczyk, PhD

Key areas: resilience, fault and intrusion tolerance, cyber-physical systems, automotive and aerospace vehicles and infrastructures.

Jerzy Julian Michalski, PhD

Key areas: space R&D, microwave technology, Inertial Measurement Units.

Łukasz Mikulski, PhD

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

Mateusz Kamiński, MSc, PhD student

Key areas: tool development.

Yan Kim, MSc, PhD student

Key areas: modelling and analysis of voting protocols.

Damian Kurpiewski, MSc, PhD student

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

Teofil Sidoruk, MSc, PhD student

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

Publications

2024

  • Artur Niewiadomski, Maciej Nazarczuk, Mateusz Przychodzki, Magdalena Kacprzak, Wojciech Penczek, Andrzej Zbrzezny
    SMT4SMTL: a Tool for SMT-Based Satisfiability Checking of SMTL.
    AAMAS 2024: Proceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems, 2024, To appear.
  • Wojciech Jamroga, Munyque Mittelmann, Aniello Murano, and Giuseppe Perelli
    Playing Quantitative Games Against an Authority: On the Module Checking Problem.
    Proceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems AAMAS 2024. To appear.
  • Francesco Belardinelli, Wojciech Jamroga, Munyque Mittelmann, and Aniello Murano
    Verification of Stochastic Multi-Agent Systems with Forgetful Strategies.
    Proceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems AAMAS 2024. To appear.
  • Mateusz Kaminski, Damian Kurpiewski and Wojciech Jamroga
    STV+KH: Towards Practical Verification of Strategic Ability for Knowledge and Information Flow.
    Proceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems AAMAS 2024. To appear.
  • Wojciech Jamroga, Yan Kim, Peter Y.A. Ryan, and Peter Roenne
    "You Shall not Abstain!" A Formal Study of Forced Participation.
    Proceedings of the 9th Workshop on Advances in Secure Electronic Voting Voting '24. To appear.
  • Wojciech Jamroga, Yan Kim, and Damian Kurpiewski
    Scalable Verification of Social Explainable AI by Variable Abstraction.
    Proceedings of the 16th International Conference on Agents and Artificial Intelligence ICAART 2024, vol.1, pp. 149-158. DOI: 10.5220/0000183700003636. PDF
  • Jaime Arias, Carlos Olarte, Laure Petrucci, Łukasz Maśko, Wojciech Penczek, Teofil Sidoruk
    Optimal Scheduling of Agents in ADTrees: Specialised Algorithm and Declarative Models.
    "IEEE Transactions on Reliability", 2024

2023

  • Damian Kurpiewski, Wojciech Jamroga, Teofil Sidoruk
    Towards Modelling and Verification of Social Explainable AI.
    ICAART 2023: Proceedings of the 15th International Conference on Agents and Artificial Intelligence, 2023. PDF
  • Jaime Arias, Wojciech Jamroga, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk
    Strategic (Timed) Computation Tree Logic.
    AAMAS 2023: Proceedings of the 22nd International Conference on Autonomous Agents and Multiagent Systems, 2023. PDF (extended version)
  • Wojciech Jamroga, Damian Kurpiewski
    Pretty Good Strategies and Where to Find Them.
    EUMAS 2023: Proceedings of the 20th European Conference on Multi-Agent Systems, 2023. PDF
  • Francesco Belardinelli, Wojciech Jamroga, Munyque Mittelmann, Aniello Murano
    Strategic Abilities of Forgetful Agents in Stochastic Environments.
    KR 2023: Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning, 2023. PDF
  • Masoud Tabatabaei, Wojciech Jamroga.
    Playing to Learn, or to Keep Secret: Alternating-Time Logic Meets Information Theory.
    AAMAS 2023: Proceedings of the 22nd International Conference on Autonomous Agents and Multiagent Systems, 2023. PDF
  • Francesco Belardinelli, Angelo Ferrando, Wojciech Jamroga, Vadim Malvone, Aniello Murano
    Scalable Verification of Strategy Logic through Three-Valued Abstraction.
    IJCAI 2023: Proceedings of the 32nd International Joint Conference on Artificial Intelligence, 2023. PDF
  • Ryszard Janicki, Maciej Koutny, Łukasz Mikulski
    Interval Traces with Mutex Relation.
    PETRI NETS 2023: Proceedings of the 44th International Conference on Application and Theory of Petri Nets and Concurrency, 2023
  • Wojciech Jamroga, Yan Kim
    Practical Model Reductions for Verification of Multi-Agent Systems.
    IJCAI 2023: Proceedings of the 32nd International Joint Conference on Artificial Intelligence, 2023. PDF
  • Wojciech Jamroga, Yan Kim
    Practical Abstraction for Model Checking of Multi-Agent Systems.
    KR 2023: Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning, 2023. PDF
  • Catalin Dima, Wojciech Jamroga
    Computationally Feasible Strategies.
    AAMAS 2023: Proceedings of the 22nd International Conference on Autonomous Agents and Multiagent Systems, 2023. PDF
  • Magdalena Kacprzak, Artur Niewiadomski, Wojciech Penczek, Andrzej Zbrzezny
    SMT-Based Satisfiability Checking of Strategic Metric Temporal Logic.
    ECAI 2023: Proceedings of the 26th European Conference on Artificial Intelligence, 2023
  • Wojciech Jamroga
    Pretty Good Strategies for Benaloh Challenge.
    E-Vote-ID 2023: Proceedings of the 8th International Joint Conference on Electronic Voting, 2023. PDF (extended version)
  • Daqian Shao, Marta Kwiatkowska
    Sample Efficient Model-free Reinforcement Learning from LTL Specifications with Optimality Guarantees.
    IJCAI 2023: Proceedings of the 32nd International Joint Conference on Artificial Intelligence, 2023
  • Benjie Wang, Marta Kwiatkowska
    Compositional Probabilistic and Causal Inference using Tractable Circuit Models.
    AISTATS 2023: Proceedings of The 26th International Conference on Artificial Intelligence and Statistics, 2023

Our Software

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.
The source code of the tool can be found at https://github.com/blackbat13/stv
The tool has a web version available at http://stv.cs-htiew.com/

MsATL

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.