1. Introduction
Software systems cannot be trusted. Even though this sounds as a bold statement, it is most
of the time the case. A software system, to be considered trustworthy, has to ofer some
guarantees to the end user. Amongst these guarantees, correctness is by far one of the most
challenging to demonstrate. However, existent solutions to proof software correctness mainly
focus on monolithic systems. So, systems that do not usually present any kind of autonomy, nor
distribution, whatsoever. Unfortunately (in some sense), nowadays, artificial intelligent systems
can be found everywhere. Thus, techniques to tackle their verification in order to establish their
correctness also need to be revised (and adapted).
When we talk about software verification, we mainly refer to standard approaches such
as: testing, simulation, and formal verification. Testing and simulation have one main issue:
they can detect errors but can not determine their absence. To overcome this problem, formal
verification results to be very useful. This approach provides a formal-based methodology to
model systems, specify properties, and verify that a system satisfies a given specification.
In formal verification, the specification is usually based on temporal logics. The latter can
describe the order of events without introducing the time explicitly. In temporal logics, we
mainly distinguish between linear- and branching-time logics, which reflect the underlying
nature of the time we consider. The most popular temporal logics are (linear-time temporal
logic) [
34
], (computation tree logic) [
14
], and their extension * [
18
]. An outstanding
development in the area of temporal logics has been the discovery of algorithmic methods
to verify properties of finite-state systems represented by Kripke structures [
28
]. Hence, the
formal verification of a system modelled by a Kripke structure with respect to a temporal
logic specification can be rephrased as “Is a model of ?”, which explains the name model
checking (MC), as it was coined by Clarke and Emerson in [
14
].
Naturally, model checking is not the only existent formal verification technique. Specifically,
another verification approach focused on a more dynamic perspective (execution of the system
rather than verification of an abstraction of the latter) is called Runtime Verification [
32
].
Runtime verification (RV) is being pursued as a lightweight verification technique bridging
static verification techniques, such as MC, and testing. One of the main distinguishing features
of RV is due to its nature of being performed at runtime, which opens up the possibility to
act whenever incorrect behavior of a software system is detected. A fault is defined as the
deviation between the current behavior and the expected behavior of the system [
32, 16
]. A
fault might lead to a failure, but not necessarily. An error, on the other hand, is a mistake made
by a human that results in a fault and possibly in a failure. Runtime verification is the discipline
of computer science that deals with the study, development, and application of those verification
techniques that allow checking whether a run of a system under scrutiny satisfies or violates a
given correctness property.
In [
20
], we presented an initial vision on possible overlapping of RV and MC, especially in
the area of Multi-Agent Systems (MAS); which are distributed systems comprised of intelligent
components (called agents) that can be deployed to solve complex tasks in an autonomous
fashion (which may, or may not, involve cooperation and communication amongst the agents).
We focused on MAS for their implicit complexity, and consequently hard verification problem.
Nonetheless, in [
20
] we mainly focused on the verification aspects of combining RV and MC.
Instead, in here, we present some novel results in that direction, but we also focus on the synergy
between RV and MAS. Thus, not only focusing on how RV can be deployed to verify MAS, but
also on how the verification for MAS can be exploited to support RV.
In the rest of the paper we first discuss the state of the art of model checking and runtime
verification for MAS (Section 2). Then, in Section 3 we present our results to use runtime
verification to reduce the model checking complexity on MAS and conclude with future directions.
Finally, in Section 4 we present model checking techniques to help runtime verification and
conclude with some future works.
2. State of the art
Model Checking for MAS. One of the most important developments in this field is
Alternating-Time Temporal Logic (ATL), introduced by Alur, Henzinger, and Kupferman [
4
].
Such a logic allows to reason about strategies of agents having the satisfaction of temporal
goals as payof criterion. More formally, it is obtained as a generalization of CTL, in which
the existential E and the universal A path quantifiers are replaced with strategic modalities of
the form ⟨⟨Γ ⟩⟩ and [[Γ]] , where Γ is a set of agents. Despite its expressiveness, ATL sufers
from the strong limitation that strategies are treated only implicitly in the semantics of such
modalities. This restriction makes the logic less suited to formalize several important solution
concepts, such as the Nash Equilibrium. These considerations led to the introduction of Strategy
Logic (SL) [
33
], a more powerful formalism for strategic reasoning. As a key aspect, this logic
treats strategies as first-order objects that can be determined by means of the existential ∃ and
universal ∀ quantifiers, which can be respectively read as “there exists a strategy ” and “for
all strategies ”. Notably, a strategy is a generic conditional plan that at each step of the game
prescribes an action. With more detail, there are two main classes of strategies: memoryless
and memoryful. In the former case, agents choose an action by considering only the current
game state while, in the latter case, agents choose an action by considering the full history
of the game. Therefore, this plan is not intrinsically glued to a specific agent, but an explicit
binding operator (, ) allows to link an agent to the strategy associated with a variable .
Unfortunately, the high expressivity of SL comes at a price. Indeed, it has been proved that the
model-checking problem for SL becomes non-elementary complete and the satisfiability
undecidable. To gain back elementariness, several fragments of SL have been considered. Among
the others, Strategy Logic with Simple-Goals [
6
] considers SL formulas in which strategic
operators, bindings operators, and temporal operators are coupled. It has been shown that
Strategy Logic with Simple-Goals strictly subsume ATL and its MC problem is P-Complete, as
it is for ATL. To conclude this section, we want to focus on a key aspect in MAS: the agents’
visibility. Specifically, we distinguish between perfect and imperfect information games [
35
].
The former corresponds to a basic setting in which every agent has full knowledge about the
game. However, in real-life scenarios it is common to have situations in which agents have
to play without having all relevant information at hand. In computer science these situations
occur for example when some variables of a system are internal/private and not visible to an
external environment [
29, 13
]. In game models, the imperfect information is usually modelled
by setting an indistinguishability relation over the states of the game [
29, 35
]. This feature
deeply impacts on the MC complexity. For example, ATL becomes undecidable in the context
of imperfect information and memoryful strategies [
17
]. To overcome this problem, some
works have either focused on an approximation to perfect information [
8, 11
] or developed new
notions on strategies [
7, 26, 27, 10, 12, 9
].
Runtime Verification for MAS. In [
2
], the authors presented a framework to verify at
runtime agent interaction protocols (AIP). The formalism used in this work allows the introduction
of variables, that are then used to constrain the expected behavior in a more expressive way.
In [
19
], the same authors proposed an approach to verify at runtime AIP using multiple monitors.
This is obtained by decentralizing the global specification (specified as a Trace Expression [
1
]),
which is used to represent the global protocol, into partial specifications denoting the single
agents’ perspective. In [
5, 36
], other works on runtime verification of agent interactions are
proposed, and in [
30
] a framework for dynamic adaptive MAS (DAMS-RV) based on an adaptive
feedback loop is presented. Other approaches to MAS RV include the proposals spin-of from
the SOCS project where the SCIFF computational logic framework [
3
] is used to provide the
semantics of social integrity constraints. To model MAS interaction, expectation-based semantics
specifies the links between observed and expected events, providing a means to test runtime
conformance of an actual conversation with respect to a given interaction protocol [
38
]. Similar
work has been performed using commitments [
15
].
3. Runtime verification gives a hand to Model checking for
MAS
The model checking problem for giving a generic MAS is known to be undecidable.
Nonetheless, decidable fragments exist. Indeed, model checking under perfect information
is PTIME-complete [
4
], while under imperfect information and imperfect recall is PSPACE [
37
].
Unfortunately, MAS usually have imperfect information, and when memory is needed to achieve
the goals, the resulting model checking problem becomes undecidable. Given the relevance of
the imperfect information setting, even partial solutions to the problem are useful.
The only existent work on exploiting RV to formally verify the strategic behaviour in MAS
is [
24, 22
]. In such work, given an formula and a model of MAS , the procedure
extracts all the sub-models of with perfect information that satisfy a sub-formula of . Then,
runtime monitors are used to check if the remaining part of can be satisfied at execution time.
If this is the case, we conclude at runtime the satisfaction of for the corresponding system
execution. Note that, this does not imply that the system satisfies , indeed future executions
may violate . The formal result over only concerns the current execution, and how it has
behaved in it. However, the following preservation results holds.
Lemma 1. Given a model and an ATL formula , for any history ℎ of starting in , we
have that:
(ℎ) = ⊤ ⇒ , |=
(ℎ) = ⊥ ⇒ , ̸|= ∅
where is the variant of where all strategic operators are removed, is the variant of
where all strategic operators are converted into ⟨⟨⟩⟩, ∅ is the variant of where all strategic
operators are converted into ⟨⟨∅⟩⟩.
Lemma 1 shows a preservation result from RV to ATL model checking that needs to be
discussed. If our monitor returns true we have two possibilities:
1 The procedure found an under-approximation sub-model in which the original formula
is satisfied then it can conclude the verification procedure by using RV only by checking
that the atom representing holds in the initial state of the history ℎ given in input;
2 A sub-formula ′ is satisfied in an under-approximation sub-model and at runtime the
formula holds on the history ℎ given in input.
While case (1) gives a preservation result for the formula given in input, case (2) checks
formula instead of . That is, it substitutes as coalition for all the strategic operators
of but the ones in ′. So, our procedure approximates the truth value by considering the
case in which all the agents in the game collaborate to achieve the objectives not satisfied in
the model checking phase. That is, while in [
8, 11
] the approximation is given in terms of
information, in [
7
] is given in terms of memory of strategies, and in [
21
] the approximation
is given by generalizing the logic, here we give results by approximating the coalitions. So,
the main limitation of this approach concerns this aspect. Furthermore, we recall that the
procedure produces always results, even partial. This aspect is strongly relevant in concrete
scenario in which there is the necessity to have some sort of verification results. For example,
in the context of swarm robots, with this procedure we can verify macro properties such as
“the system works properly” since we are able to guarantee fully collaboration between agents
because this property is relevant and desirable for each agent in the game. The same reasoning
described above, can be applied in a complementary way for the case of over-approximation
sub-models and the falsity.
Note that this is the first attempt of using runtime verification to verify strategic properties on
MAS. Thus, even though the solution might not be optimal, it is a milestone for the corresponding
lines of research. Additional works will be done to improve the technique and, above all, its
implementation. For instance, we are planning to extend this work by considering a more
predictive flavour.
4. Model checking for MAS gives a hand to Runtime
verification
Runtime Verification is built on the assumption of perfect information over the system, that is,
the monitor checking the system can perceive everything. Unfortunately, this is not always the
case, especially when the system under analysis contains rational/autonomous components
and is deployed in real-world environments with possibly faulty sensors. In [
23
], an extension
of the standard Runtime Verification of Linear Temporal Logic properties to consider scenarios
with imperfect information is presented; along with all the engineering steps necessary to
update the verification pipeline. Moreover, a corresponding implementation is proposed and
applied to a case study involving robotic systems. In particular, [
23
] defines the notion of
imperfect information w.r.t. the monitor’s visibility over the system, and then re-engineers the
LTL monitor’s synthesis pipeline to recognise such visibility information.
In [
23
], imperfect information is specified by means of a indistinguishability relation ∼ over
the atomic propositions. Intuitively, given two atomic propositions and , it is said that they
are indistinguishable if and only if ∼ .
To handle the verification process in the imperfect information scenario, the standard RV
approach needs to be extended. This extension is based on the notion of duplication of the
atoms. The latter is used in order to make the truth value of each atomic proposition explicit.
The new monitor is defined as follows.
Definition 1 (Monitor with imperfect information).
Given an LTL formula and a visible
history ℎ, a monitor with imperfect information is so defined:
(ℎ) =
⎧
⎪⎪ ⊤
⎪
⎪⎪⎪⎪ ⊥
⎪
⎪⎨
⎪ ?̸⊥
⎪
⎪
⎪
⎪ ?
⎪ ̸⊤
⎪
⎪⎪⎩ ?
ℎ ∈ ℒ( ) ∧ ℎ ∈/ ℒ(¬ ) ∧ ℎ ∈/ ℒ(⊗ )
ℎ ∈/ ℒ( ) ∧ ℎ ∈ ℒ(¬ ) ∧ ℎ ∈/ ℒ(⊗ )
ℎ ∈/ ℒ( ) ∧ ℎ ∈/ ℒ(¬ ) ∧ ℎ ∈ ℒ(⊗ )
ℎ ∈ ℒ( ) ∧ ℎ ∈/ ℒ(¬ ) ∧ ℎ ∈ ℒ(⊗ )
ℎ ∈/ ℒ( ) ∧ ℎ ∈ ℒ(¬ ) ∧ ℎ ∈ ℒ(⊗ )
ℎ ∈ ℒ( ) ∧ ℎ ∈ ℒ(¬ ) ∧ ℎ ∈ ℒ(⊗ )
Where ℒ( ) is the language of histories satisfying , ℒ(¬ ) is the language of histories
violating , and finally, ℒ(⊗ ) is the language of histories making undefined (because of
lack of information).
In what follows, we provide two preservation results from the monitor with imperfect
information to the one with perfect information.
Lemma 2. Given a finite history , a monitor with its visibility (ℎ), and a general
monitor (ℎ), we have that:
if (ℎ) = ⊤ then (ℎ) = ⊤
if (ℎ) = ⊥ then (ℎ) = ⊥
The above results can be extended to consider multi-monitors and solved by using formal
verification for MAS. In fact, even though a single monitor does not have access to all the
information it needs, multiple monitors might. As in standard distributed RV [
25
], we are
planning to explore this idea as well, but focusing on the theoretical foundations of information
sharing amongst monitors. Specifically, we are going to show how this can be specified as a
multi-agent problem; where each monitor is denoted as an agent with the goal of gathering
all the information needed to carry out the verification of its formal property. By representing
the information sharing as a multi-agent problem, we could gain from diferent viewpoints. In
particular, we could exploit existing techniques, used for strategic reasoning [
31
], to guide the
information sharing amongst the monitors. Moreover, by denoting monitors as agents, we would
recognise their autonomy on what concern the sharing of private information. For instance, a
monitor could be the only one with the access to a certain resource, and it is not realistic to
assume it will freely share such information. This because the act of sharing information is not
free of charge, since it requires to both consume computation time and bandwidth. For this,
and other reasons, it is of paramount importance to take into consideration the cost of sharing.
We are going to show how such cost can be ported into the multi-agent problem, and how it
can guide the selection of the information sharing strategy of the agents (i.e., the monitors).
In particular, we are going to study the theoretical foundation of information sharing amongst
runtime monitors. We will tackle this by porting the problem into a multi-agent setting. By
dosing so, we apply existing formal verification techniques, such as model checking [
31
], to
exploit the strategic reasoning of the agents to overcome the information sharing problem. We
will not only present theoretical results, but we will also propose an implementation prototype,
as a proof of concept.