-
Verification of Multi-Agent Properties in Electronic Voting: A Case Study
Authors:
Damian Kurpiewski,
Wojciech Jamroga,
Łukasz Maśko,
Łukasz Mikulski,
Witold Pazderski,
Wojciech Penczek,
Teofil Sidoruk
Abstract:
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 efficiency, and allow to verify only toy examples. Here, we propose some new techniques and combine them with several recently developed ones to see what progress can be achieved for a real-life scenario. Namely, we use fixpo…
▽ More
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 efficiency, and allow to verify only toy examples. Here, we propose some new techniques and combine them with several recently developed ones to see what progress can be achieved for a real-life scenario. Namely, we use fixpoint approximation, domination-based strategy search, partial order reduction, and parallelization to verify heterogeneous scalable models of the Selene e-voting protocol. The experimental results show that the combination allows to verify requirements for much more sophisticated models than previously.
△ Less
Submitted 24 October, 2023;
originally announced October 2023.
-
Optimal Scheduling of Agents in ADTrees: Specialised Algorithm and Declarative Models
Authors:
Jaime Arias,
Carlos Olarte,
Laure Petrucci,
Łukasz Maśko,
Wojciech Penczek,
Teofil Sidoruk
Abstract:
Expressing attack-defence trees in a multi-agent setting allows for studying a new aspect of security scenarios, namely how the number of agents and their task assignment impact the performance, e.g. attack time, of strategies executed by opposing coalitions. Optimal scheduling of agents' actions, a non-trivial problem, is thus vital. We discuss associated caveats and propose an algorithm that syn…
▽ More
Expressing attack-defence trees in a multi-agent setting allows for studying a new aspect of security scenarios, namely how the number of agents and their task assignment impact the performance, e.g. attack time, of strategies executed by opposing coalitions. Optimal scheduling of agents' actions, a non-trivial problem, is thus vital. We discuss associated caveats and propose an algorithm that synthesises such an assignment, targeting minimal attack time and using the minimal number of agents for a given attack-defence tree. We also investigate an alternative approach for the same problem using Rewriting Logic, starting with a simple and elegant declarative model, whose correctness (in terms of schedule's optimality) is self-evident. We then refine this specification, inspired by the design of our specialised algorithm, to obtain an efficient system that can be used as a playground to explore various aspects of attack-defence trees. We compare the two approaches on different benchmarks.
△ Less
Submitted 19 October, 2023; v1 submitted 8 May, 2023;
originally announced May 2023.
-
Minimal Schedule with Minimal Number of Agents in Attack-Defence Trees
Authors:
Jaime Arias,
Łukasz Maśko,
Wojciech Penczek,
Laure Petrucci,
Teofil Sidoruk
Abstract:
Expressing attack-defence trees in a multi-agent setting allows for studying a new aspect of security scenarios, namely how the number of agents and their task assignment impact the performance, e.g. attack time, of strategies executed by opposing coalitions. Optimal scheduling of agents' actions, a non-trivial problem, is thus vital. We discuss associated caveats and propose an algorithm that syn…
▽ More
Expressing attack-defence trees in a multi-agent setting allows for studying a new aspect of security scenarios, namely how the number of agents and their task assignment impact the performance, e.g. attack time, of strategies executed by opposing coalitions. Optimal scheduling of agents' actions, a non-trivial problem, is thus vital. We discuss associated caveats and propose an algorithm that synthesises such an assignment, targeting minimal attack time and using minimal number of agents for a given attack-defence tree.
△ Less
Submitted 29 April, 2022; v1 submitted 17 January, 2021;
originally announced January 2021.
