-
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.
-
Strategic (Timed) Computation Tree Logic
Authors:
Jaime Arias,
Wojciech Jamroga,
Wojciech Penczek,
Laure Petrucci,
Teofil Sidoruk
Abstract:
We define extensions of CTL and TCTL with strategic operators, called Strategic CTL (SCTL) and Strategic TCTL (STCTL), respectively. For each of the above logics we give a synchronous and asynchronous semantics, i.e., STCTL is interpreted over networks of extended Timed Automata (TA) that either make synchronous moves or synchronise via joint actions. We consider several semantics regarding inform…
▽ More
We define extensions of CTL and TCTL with strategic operators, called Strategic CTL (SCTL) and Strategic TCTL (STCTL), respectively. For each of the above logics we give a synchronous and asynchronous semantics, i.e., STCTL is interpreted over networks of extended Timed Automata (TA) that either make synchronous moves or synchronise via joint actions. We consider several semantics regarding information: imperfect (i) and perfect (I), and recall: imperfect (r) and perfect (R). We prove that SCTL is more expressive than ATL for all semantics, and this holds for the timed versions as well. Moreover, the model checking problem for SCTL[ir] is of the same complexity as for ATL[ir], the model checking problem for STCTL[ir] is of the same complexity as for TCTL, while for STCTL[iR] it is undecidable as for ATL[iR]. The above results suggest to use SCTL[ir] and STCTL[ir] in practical applications. Therefore, we use the tool IMITATOR to support model checking of STCTL[ir].
△ Less
Submitted 19 October, 2023; v1 submitted 26 February, 2023;
originally announced February 2023.
-
Towards Modelling and Verification of Social Explainable AI
Authors:
Damian Kurpiewski,
Wojciech Jamroga,
Teofil Sidoruk
Abstract:
Social Explainable AI (SAI) is a new direction in artificial intelligence that emphasises decentralisation, transparency, social context, and focus on the human users. SAI research is still at an early stage. Consequently, it concentrates on delivering the intended functionalities, but largely ignores the possibility of unwelcome behaviours due to malicious or erroneous activity. We propose that,…
▽ More
Social Explainable AI (SAI) is a new direction in artificial intelligence that emphasises decentralisation, transparency, social context, and focus on the human users. SAI research is still at an early stage. Consequently, it concentrates on delivering the intended functionalities, but largely ignores the possibility of unwelcome behaviours due to malicious or erroneous activity. We propose that, in order to capture the breadth of relevant aspects, one can use models and logics of strategic ability, that have been developed in multi-agent systems. Using the STV model checker, we take the first step towards the formal modelling and verification of SAI environments, in particular of their resistance to various types of attacks by compromised AI modules.
△ Less
Submitted 19 October, 2023; v1 submitted 2 February, 2023;
originally announced February 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.
-
Strategic Abilities of Asynchronous Agents: Semantic Side Effects and How to Tame Them
Authors:
Wojciech Jamroga,
Wojciech Penczek,
Teofil Sidoruk
Abstract:
Recently, we have proposed a framework for verification of agents' abilities in asynchronous multi-agent systems, together with an algorithm for automated reduction of models. The semantics was built on the modeling tradition of distributed systems. As we show here, this can sometimes lead to counterintuitive interpretation of formulas when reasoning about the outcome of strategies. First, the sem…
▽ More
Recently, we have proposed a framework for verification of agents' abilities in asynchronous multi-agent systems, together with an algorithm for automated reduction of models. The semantics was built on the modeling tradition of distributed systems. As we show here, this can sometimes lead to counterintuitive interpretation of formulas when reasoning about the outcome of strategies. First, the semantics disregards finite paths, and thus yields unnatural evaluation of strategies with deadlocks. Secondly, the semantic representations do not allow to capture the asymmetry between proactive agents and the recipients of their choices. We propose how to avoid the problems by a suitable extension of the representations and change of the execution semantics for asynchronous MAS. We also prove that the model reduction scheme still works in the modified framework.
△ Less
Submitted 18 October, 2023; v1 submitted 8 March, 2020;
originally announced March 2020.
