1940

# Multi-Valued Verification of Strategic Ability

Wojciech Jamroga  Beata Konikowska  Damian Kurpiewski  Wojciech Penczek
Institute of Computer Science
Polish Academy of Sciences
Jana Kazimierza 5 Address for correcpondence: Institute of Computer Science,
Polish Academy of Sciences, Jana Kazimierza 5, 01-248 Warsaw, Poland 01-248
Warsaw  Poland
{jamroga  konikowska  kurpiewski<EMAIL_ADDRESS>
###### Abstract

Some multi-agent scenarios call for the possibility of evaluating
specifications in a richer domain of truth values. Examples include runtime
monitoring of a temporal property over a growing prefix of an infinite path,
inconsistency analysis in distributed databases, and verification methods that
use incomplete anytime algorithms, such as bounded model checking. In this
paper, we present _multi-valued alternating-time temporal logic_ (mv-
ATL${}^{*}_{\rightarrow}$), an expressive logic to specify strategic abilities
in multi-agent systems. It is well known that, for branching-time logics, a
general method for model-independent translation from multi-valued to two-
valued model checking exists. We show that the method cannot be directly
extended to mv-ATL${}^{*}_{\rightarrow}$. We also propose two ways of
overcoming the problem. Firstly, we identify constraints on formulas for which
the model-independent translation can be suitably adapted. Secondly, we
present a model-dependent reduction that can be applied to all formulas of mv-
ATL${}^{*}_{\rightarrow}$. We show that, in all cases, the complexity of
verification increases only linearly when new truth values are added to the
evaluation domain. We also consider several examples that show possible
applications of mv-ATL${}^{*}_{\rightarrow}$ and motivate its use for model
checking multi-agent systems.

††issue: 175 (2020)

Multi-Valued Verification of Strategic Ability

##  1 Introduction

Alternating-time temporal logic ATL${}_{\textup{{}}}^{\ast}$ and its less
expressive variant ATL${}_{\textup{{}}}$ [1, 2] are probably the most popular
logics that allow for reasoning about agents’ abilities in strategic
encounters. ATL${}_{\textup{{}}}^{\ast}$ combines features of temporal logic
and basic game theory, encapsulated in the main language construct of the
logic, $\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\gamma$,
which can be read as “the group of agents $A$ has a strategy to enforce
$\gamma$”. Property $\gamma$ can include operators $\mathsf{X}\,$ (“next”),
$\mathsf{G}\,$ (“always”), $\mathsf{F}\,$ (“eventually”) and/or
$\,\mathsf{U}\,$ (“until”). Much research on ATL${}_{\textup{{}}}^{\ast}$ has
focused on the way it can be used for verification of multi-agent systems,
including theoretical studies on the complexity of model checking, as well as
practical verification algorithms.

Multi-valued semantics have been already proposed for various temporal and
temporal-epistemic logics, and applied in verification of distributed and
multi-agent systems. In this paper, we extend the general approach of [3, 4]
to verification of strategic abilities for agents and their coalitions. Many
relevant properties of multi-agent systems are intuitively underpinned by the
ability (or inability) of particular agents to obtain particular outcomes. For
example, most functionality requirements can be specified as the ability of
the authorized users to achieve their legitimate goals. At the same time, many
security properties can be phrased in terms of the inability of unauthorized
users to compromise the system. We show that reasoning about, and verification
of such statements can be naturally conducted in richer domains of truth
values, regardless of the actual notion of strategic play and constraints on
the agents’ epistemic capabilities. Moreover, multiple truth values incur no
significant increase of either the theoretical or the practical complexity of
the model checking problem. In fact, we show that multi-valued verification of
strategic abilities can be usually done by means of an efficient translation
to classical verification. We also present a case study that demonstrates the
modeling value of the approach and its efficiency.

###  1.1 Multi-valued model checking: Why bother?

Typically, model checking is a yes/no problem. That is, the output is a
classical truth value: $\top$ for “yes”, $\bot$ for “no.” However, it is
sometimes convenient to consider the output of verification in a richer domain
of values. This can be due to at least three reasons. First, our reasoning
about the world can be based on a non-classical notion of truth (e.g., graded,
fuzzy, constructive, defeasible etc.). For example, if an atomic statement
$\mathsf{{pol}}$ (“the area is polluted”) is evaluated according to
measurements conducted in the environment, the possible outputs can include
“highly,” “much,” “little,” and “not at all,” instead of simply “yes” and
“no.” Multi-valued semantics take those outputs directly as the possible truth
values of $\mathsf{{pol}}$, and hence also of more complex formulas involving
$\mathsf{{pol}}$. This is particularly useful in case of model checking
realistic systems, as it allows to lift logical reasoning to a richer domain
of answers in a compact way.

Secondly, we can understand the properties of the world in a classical way
(being always completely true or fully false), but our model of the system can
be only partially conclusive. A good example is runtime monitoring of temporal
properties, where a temporal formula (interpreted with an infinite time
horizon in mind) is checked on a finite but constantly growing sequence of
events, observed so far. Consider for instance specification
$\mathsf{F}\,\mathsf{{cool}}$ (“the reactor will be cooled down sometime in
the future”). If $\mathsf{{cool}}$ has already occurred then the formula is
clearly true whatever happens next. What if it has not occurred? Then, the
formula may still turn out true (because $\mathsf{{cool}}$ may occur in
subsequent steps), but it can also turn out false; effectively, the truth
value is unknown in our current model. Likewise, formula
$\mathsf{G}\,\mathsf{{cool}}$ (“$\mathsf{{cool}}$ will always hold”) can be
only proved false in the course of monitoring, or the model is inconclusive
regarding its value. Indeed, well known approaches to runtime monitoring use
multi-valued interpretation of temporal formulas in finite runs [5, 6].

Conflicting evidence coming from different sources is another reason why one
may need to deal with an imperfect model of the system. This can happen, e.g.,
in case of a distributed knowledge base, where some components may be outdated
and/or contain unreliable information. In classical logic, the deductive
explosion would make any attempt at reasoning useless. In multi-valued logics,
one can assign a special truth value (“inconsistent”) to situations when
conflicting evidence about the value of $\mathsf{{p}}$ exists, and conduct the
verification in the usual way.

Thirdly, even if the model is complete and faithful, the verification
procedure can be only partially conclusive. For instance, in bounded model
checking [7, 8], a full transition system is given but the formula is checked
on runs of length at most $n$. Now, again, $\mathsf{F}\,\mathsf{{p}}$ is
clearly true if we find $\mathsf{{p}}$ to occur on every path in up to $n$
steps. Otherwise, the output is inconclusive (because $\mathsf{{p}}$ might or
might not occur in subsequent steps). The case of $\mathsf{G}\,\mathsf{{p}}$
is analogous.

Note that different sources of multiple truth values can easily combine. For
example, runtime monitoring of a distributed knowledge base may require
handling both the possible inconsistency of data across different locations
and the uncertainty about how the system state will evolve. This kind of
scenarios are most conveniently modeled by partially, rather than linearly
ordered sets of answers. Overall, it should be up to the designer to decide
which domain of truth values will be used for verification. In this paper, we
provide a general methodology, together with flexible algorithms, that can be
used for any distributive lattice of interpretation.

###  1.2 Technical contribution and outline of the paper

The focus of the article is on general multi-valued verification of strategic
abilities in multi-agent systems. The main contributions are:

  1. 1.

We propose a multi-valued variant of alternating-time temporal logic
ATL${}_{\textup{{}}}^{\ast}$, called mv-ATL${}^{*}_{\rightarrow}$, over
arbitrary lattices of logical values. We also show that the new logic is a
conservative extension of the standard, 2-valued ATL${}_{\textup{{}}}^{\ast}$.

  2. 2.

We study the multi-valued model checking problem for mv-
ATL${}^{*}_{\rightarrow}$. Similarly to the previous work on temporal model
checking [3, 4], we do not propose dedicated algorithms for mv-
ATL${}^{*}_{\rightarrow}$. Instead, we look for general efficient translations
from the multi-valued case to the 2-valued case. In this respect, we:

    1. (a)

prove that no model-independent translation exists for the whole language of
mv-ATL${}^{*}_{\rightarrow}$,

    2. (b)

identify a broad subclass of formulas for which such a translation can be
obtained,

    3. (c)

propose a recursive model-dependent translation that works for all instances
of the problem.

  3. 3.

We show that all results are insensitive to the actual notion of strategy and
strategic play. In particular, they easily extend to verification of
strategies under imperfect information.

  4. 4.

Finally, we report an implementation of the verification algorithm based on
the translation to 2-valued model checking, and evaluate its performance
experimentally.

Point 2 might require further explanation. Multi-valued model checking often
provides a _conceptual_ approximation of the classical (two-valued)
verification problem, especially in case the precise model is difficult to
obtain. On the other hand, we show a _technical_ reduction of multi-valued
model checking to the two-valued variant. Thus, typically, a designer who
wants to verify properties of a complex system, expressed in (classical)
ATL${}_{\textup{{}}}^{\ast}$, would first come up with a conceptual
approximation of the problem in mv-ATL${}^{*}_{\rightarrow}$, then use the
technical translation of the specification back to model checking of
ATL${}_{\textup{{}}}^{\ast}$, and finally run the latter by means of an
existing tool (such as MCMAS [9]).

The structure of the paper is as follows. We begin by presenting the context
of our work: the alternating time logic ATL${}_{\textup{{}}}^{\ast}$ in
Section 2, and distributive lattices in Section 3. We also introduce our
working example of drones monitoring the pollution in a city. In Section 4, we
define the syntax and semantics of our multi-valued variant of
ATL${}_{\textup{{}}}^{\ast}$, the logic mv-ATL${}^{*}_{\rightarrow}$. Section
5 discusses the model checking problem for mv-ATL${}^{*}_{\rightarrow}$ (in
general and under certain restrictions). Until that point, we assume the
classical interpretation of transitions in models, i.e., the multi-valued
approach is applied only to the labeling of _states_. Section 6 extends our
definitions and results to models with many-valued transitions. We also show
that the idea of _may/must abstraction_ can be seen as a special case of model
checking mv-ATL${}^{*}_{\rightarrow}$. Section 7 adapts our results to
verification of strategies for agents with imperfect information. In Section
8, we present an experimental evaluation of our algorithms, based on the
drones scenario. Finally, we conclude in Section 9.

Previous version of the article. The main concepts and some of the results
have appeared in a preliminary form in the conference paper [10]. The present
version extends it with proper proofs, a comprehensive discussion on
motivation and applicability, and a generalization of the framework to models
with multi-valued transitions. We also add a case study (complete with a
detailed experimental evaluation) based on a newly proposed benchmark model.

###  1.3 Related work

Multi-valued interpretation of modal formulas has been used in multiple
approaches to verification. The main idea was proposed by Fitting [11, 12]
already more than 25 years ago. Further fundamental work on multi-valued modal
logic includes, e.g., [13] where general properties of multi-valued
abstractions were studied, and demonstrated on an example 9-valued bilattice.

In the 2000s, a number of works adapted the idea to verification of
distributed and multi-agent systems. A variant of CTL${}_{\textup{{}}}^{\ast}$
for models over finite quasi-boolean lattices was proposed in [3], together
with a general translation scheme that reduced multi-valued model checking of
CTL${}_{\textup{{}}}^{\ast}$ specifications to the standard 2-valued case.
This was later extended to multi-valued modal $\mu$-calculus [14, 15, 16, 17],
and to multi-valued modal $\mu$-calculus with knowledge [4].111 Note that,
despite having “games” in the title, [16] was not concerned with strategic
specifications. “Games” were used there only in the technical sense, to define
the semantics of $\mu$-calculus. However, [18] deals with game applications of
[16].  Our paper follows this line of work, and extends the techniques to
strategic operators of ATL${}_{\textup{{}}}^{\ast}$. We also enrich the
language with the two-valued “implication” (or comparison) and ”equivalence”
operators $\rightarrow$ and $\cong$, which provide: (i) the notions of
material implication and biconditional, useful in specifying general
properties of multi-valued models; (ii) a way of model checking “threshold
properties” analogous to probabilistic temporal logics behind PRISM [19]. As
it turns out, the new operators require non-trivial treatment, significantly
different from the previous works [3, 14, 15, 4, 16, 17].

All the above papers consider _general_ multi-valued verification, i.e., the
interpretation can be based on an arbitrary finite lattice. Another line of
work considers model checking over specific domains of truth values, tailored
to a particular class of scenarios. Model checking methods for the special
case of 3-valued temporal logics were discussed in [20, 21, 22] and, recently,
in [23]. Two different methods for approximating the standard two-valued
semantics of ATL${}_{\textup{{}}}^{\ast}$ under imperfect information by using
three-valued ATL${}_{\textup{{}}}^{\ast}$ are presented and analysed in [24,
25]. However, these approaches use only Kleene’s three valued logic rather
than general distributive lattices. Moreover, a partial algorithm for model
checking two-valued perfect recall via its approximation as three-valued
bounded recall is constructed in [24].

Related approaches include runtime verification, which often uses 3-valued [5]
or 4-valued interpretation [6, 14] of temporal formulas. Moreover, a 4-valued
semantics has been used to evaluate database queries [26, 27]. A 3-valued
semantics of strategic abilities in models of perfect information was
considered in [28] for verification of alternating $\mu$-calculus, and in [29]
for abilities expressed in ATL${}_{\textup{{}}}$.222 More precisely, the
semantics in [29] includes agents’ indistinguishability relations in the
model, but it allows for non-uniform play, thus effectively assuming that the
agents have perfect information about the current state of the system while
playing.  In [30], another 3-valued semantics of ATL${}_{\textup{{}}}$ was
studied, for both perfect and imperfect information. In all those papers
(i.e., [28, 29, 30]), the main aim was to verify may/must abstractions of
multi-agent systems. Note that, while the agenda of our paper comes close to
that of [29, 30], our semantics differs from [29] even in the 3-valued case.
Moreover, our multi-valued semantics of ATL${}_{\textup{{}}}$ is a
conservative extension of standard ATL${}_{\textup{{}}}$, whereas the one in
[29] is not. In contrast, the ATL${}_{\textup{{}}}$ variant in [30] _is_ a
conservative extension of the 2-valued semantics, and can be in fact
considered as a very special case of our general semantics.

A quite different but related strand of research concerns real-valued logics
over probabilistic models for temporal [31, 32, 33] and strategic
specifications [34]. We also mention the research on probabilistic model
checking of temporal and strategic logics [35, 36, 19, 37, 38, 39] that
evaluates specifications in the 2-valued domain but recognizes different
degrees of success and the need to aggregate them over available strategies
and possible paths.

In sum, there have been approaches to general multi-valued model checking of
temporal and epistemic properties, but no analogous proposals for strategic
properties. Furthermore, there were proposals for multi-valued verification of
strategic properties over specific (and usually very simple) sets of truth
vales, but no framework that studies the same problem for arbitrary lattices.
This paper fills the gap, and combines elements of both strands to obtain a
general framework for multi-valued verification of ability in systems of
interacting agents.

##  2 How to specify strategic abilities

We begin by recalling the basics of two-valued alternating-time temporal
logic. We also introduce our working example that will be used throughout the
paper.

###  2.1 Syntax

_Alternating-time temporal logic_ [1, 2] generalizes the branching-time
temporal logic CTL${}_{\textup{{}}}^{\ast}$ by replacing path quantifiers
$\mathsf{E},\mathsf{A}$ with _strategic modalities_
$\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}$. Informally,
$\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\gamma$ says that a
group of agents $A$ has a collective strategy to enforce temporal property
$\gamma$. ATL${}_{\textup{{}}}^{\ast}$ formulas can include temporal
operators: $\mathsf{X}\,$ (“in the next state”), $\mathsf{G}\,$ (“always from
now on”), $\mathsf{F}\,$ (“now or sometime in the future”), and
$\,\mathsf{U}\,$ (strong “until”). Similarly to CTL${}_{\textup{{}}}^{\ast}$
and CTL, we consider two syntactic variants of the alternating-time logic,
namely ATL${}_{\textup{{}}}^{\ast}$ and ATL${}_{\textup{{}}}$. Formally, let
${\mathbb{A}\mathrm{gt}}$ be a finite set of agents, and $Prop$ a countable
set of atomic propositions. The language of ATL${}_{\textup{{}}}^{\ast}$ is
defined as follows:

$\varphi::=\mathsf{{p}}\mid\neg\varphi\mid\varphi\wedge\varphi\mid\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\gamma$,
$\gamma::=\varphi\mid\neg\gamma\mid\gamma\land\gamma\mid\mathsf{X}\,\gamma\mid\gamma\,\mathsf{U}\,\gamma$.

where $A\subseteq{\mathbb{A}\mathrm{gt}}$ and $\mathsf{{p}}\in Prop$.
Traditionally, only the state formulas $\varphi$ are called formulas of
ATL${}_{\textup{{}}}^{\ast}$. Derived boolean connectives and constants
($\lor,\top,\bot$) are defined as usual. “Sometime”, “weak until”, and “always
from now on” are defined as
$\mathsf{F}\,\gamma\equiv\top\,\mathsf{U}\,\gamma$,
$\gamma_{1}\,\mathsf{W}\,\gamma_{2}\equiv\neg((\neg\gamma_{2})\,\mathsf{U}\,(\neg\gamma_{1}\land\neg\gamma_{2}))$,
and $\mathsf{G}\,\gamma\equiv\gamma\,\mathsf{W}\,\bot$. Also, we can use
$[\\![{A}]\\!]\gamma\equiv\neg\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\neg\gamma$
to express that, for each strategy of $A$, property $\gamma$ holds on some
paths.

ATL${}_{\textup{{}}}$ (without “star”) is the syntactic variant in which
strategic and temporal operators are combined into compound modalities:
$\varphi::=\mathsf{{p}}\mid\lnot\varphi\mid\varphi\land\varphi\mid\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{X}\,\varphi\mid\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\varphi\,\mathsf{U}\,\varphi\mid\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\varphi\,\mathsf{W}\,\varphi$.

###  2.2 Models

The semantics of ATL${}_{\textup{{}}}^{\ast}$ is typically defined over
synchronous multi-agent transition systems, i.e., models where all the agents
simultaneously decide on their next actions, and the combination of their
choices determines the next state, see the following definition.

######  Definition 2.1 (CGS)

A _concurrent game structure (CGS)_ is a tuple
$M=\langle{{\mathbb{A}\mathrm{gt}},St,Act,d,t,Prop,V}\rangle$, which includes
nonempty finite sets of: agents ${\mathbb{A}\mathrm{gt}}$, states $St$,
actions $Act$, atomic propositions $Prop$, and a propositional valuation
$V:St\rightarrow 2^{Prop}$. The function $d:{\mathbb{A}\mathrm{gt}}\times
St\rightarrow 2^{Act}\setminus\\{{\emptyset}\\}$ defines the availability of
actions. The (deterministic) transition function $t$ assigns a successor state
$q^{\prime}=t(q,\alpha_{1},\dots,\alpha_{|{\mathbb{A}\mathrm{gt}}|})$ to each
state $q\in St$ and any tuple of actions $\alpha_{i}\in d(i,q)$, one per agent
$i\in{\mathbb{A}\mathrm{gt}}$, that can be executed in $q$. A _pointed CGS_ is
a pair $(M,q_{0})$, where $M$ is a CGS and $q_{0}\in St$ is the initial state
of $M$.

A _path_ $\lambda=q_{0}q_{1}q_{2}\dots$ in a CGS is an infinite sequence of
states such that there is a transition between each $q_{i},q_{i+1}$ for each
$i\geq 0$.

$\lambda[i]$ denotes the $i$th position on $\lambda$ (starting from $i=0$) and
$\lambda[i,\infty]$ the suffix of $\lambda$ starting with $i$.

###  2.3 Semantics

Given a CGS, we define the strategies and their outcomes as follows. A
_perfect recall strategy_ (or _IR-strategy_) for agent $a$ is a function
$s_{a}:St^{+}\rightarrow Act$ such that $s_{a}(q_{0}q_{1}\dots q_{n})\in
d(a,q_{n})$. A _memoryless strategy_ (or _Ir-strategy_) for $a$ is a function
$s_{a}:St\rightarrow Act$ such that $s_{a}(q)\in d(a,q)$. A _collective
strategy_ for a group of agents $A=\\{{a_{1},\ldots,a_{r}}\\}$ is a tuple of
individual strategies $s_{A}=\langle{s_{a_{1}},\ldots,s_{a_{r}}}\rangle$. Note
that $s_{A}$ only binds the agents in $A$, while agents outside $A$ can act as
they wish. The set of such strategies is denoted by $\Sigma_{A}^{\textit{IR}}$
(resp. $\Sigma_{A}^{\textit{Ir}}$). The “outcome” function $out(q,s_{A})$
returns the set of all paths that can occur when agents $A$ execute strategy
$s_{A}$ from state $q$ onward. The semantics of perfect recall
ATL${}_{\textup{{}}}^{\ast}$ is defined as follows:

$M,q\models$ iff , for ;

$M,q\models\neg\neg\varphi$ iff $M,q\models\varphi$, and
$M,q\models\neg\varphi$ iff $M,q\not\models\varphi$ for $\varphi\neq\neg\psi$
for any $\psi$;

$M,q\models\varphi_{1}\wedge\varphi_{2}$ iff $M,q\models\varphi_{1}$ and
$M,q\models\varphi_{2}$;

$M,q\models\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\gamma$
iff there is a strategy $s_{A}\in\Sigma_{A}^{\textit{IR}}$ such that, for each
path $\lambda\in out(q,s_{A})$, we have $M,\lambda\models\gamma$.

$M,\lambda\models\varphi$ iff $M,\lambda[0]\models\varphi$;

$M,\lambda\models\neg\neg\gamma$ iff $M,\lambda\models\gamma$, and
$M,\lambda\models\neg\gamma$ iff $M,\lambda\not\models\gamma$ for
$\lambda\neq\neg\gamma$ for any $\gamma$;

$M,\lambda\models\gamma_{1}\wedge\gamma_{2}$ iff $M,\lambda\models\gamma_{1}$
and $M,\lambda\models\gamma_{2}$;

$M,\lambda\models\mathsf{X}\,\gamma$ iff $M,\lambda[1,\infty]\models\gamma$;
and

$M,\lambda\models\gamma_{1}\,\mathsf{U}\,\gamma_{2}$ iff there is an
$i\in\mathbb{N}_{0}$ such that $M,\lambda[i,\infty]\models\gamma_{2}$ and
$M,\lambda[j,\infty]\models\gamma_{1}$ for all $0\leq j<i$,

where $\mathbb{N}_{0}$ is the set of non-negative integers. The memoryless
semantics of ATL* uses strategies of $\Sigma_{A}^{\textit{Ir}}$ rather than
$\Sigma_{A}^{\textit{IR}}$.

Figure 1: Map: drone navigation and measurements in an area of Cracow.
Location colors indicate whether the PM2.5 readings are within or beyond the
norm

######  Example 2.2 (Drones patrolling for pollution)

Consider a team of $k$ drones monitoring air pollution in the city of Cracow,
Poland. For this scenario, we use the map shown in Figure 1. To keep the
resulting CGS small, the map is a grid that only includes four locations, and
the drones can move between the locations in one direction only (either North
or East).333A more complex map will be used for the experiments in Section 8.
The initial location is $0$, and the drones are supposed to reach location $3$
(called their “target” location). Each drone has a sensor to measure the level
of PM2.5 in the air, that is the rate of particles with a diameter less than
2.5 microns. The drone can also communicate with the nearest sensor on the
ground that reports the PM2.5 rate on the ground level, as well as the current
measurements of temperature, air pressure, and humidity. Note that some
measurements may be unobtainable at some locations. In particular, no
measurements are available at the start location. We also assume, for the sake
of simplicity, that the environment can be viewed as stationary with respect
to the movement of drones, i.e., the measurements at a location do not change
throughout the patrolling mission.

Figure 2 presents a pointed concurrent game structure $M_{1}$ that models the
above scenario for $k=2$ drones. Every drone is a separate agent, with two
actions available: $N$ (fly North) and $E$ (fly East). Due to a limited
battery capacity, a drone can only visit $l=2$ locations before the battery
dies. Each state of the model includes information about the current locations
of the drones, possibly distinguishing the locations that have been already
visited by the team. Note that in our simple scenario the only pair of
locations that can be reached by the drones via two different routes is
$(3,3)$. The corresponding two states are labeled accordingly $(3,3)_{1}$ and
$(3,3)_{2}$.

$(0,0)$$(1,1)$$(2,2)$$(3,3)_{1}$$(3,3)_{2}$$(1,2)$$(2,1)$(N,N)(E,E)(N,E)(E,N)(E,E)(N,N)(E,N)(N,E)
Figure 2: Model $M_{1}$: autonomous drones monitoring pollution

Most of the atomic propositions refer to the pollution measurements available
to a drone at its current location. That is, indicates that the $i$th drone
registers pollution; more precisely: the sensor of drone $i$ reports that the
level of PM2.5 exceeds the norm. Similarly, indicates that the sensor of drone
$i$ reports a level of PM2.5 within the norm. Moreover, (resp. ) says that the
ground sensor nearest to drone $i$ reports a level of PM2.5 exceeding the norm
(resp. within the norm). Proposition

######  Example 2.3 (Drones, ctd.)

For the model in Example 2.2, we have, for instance,
$M_{1},(0,0)\models\langle\\!\langle{1}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{F}\,$:
drone $1$ has a strategy ensuring that its sensor will eventually register
pollution. The stratety itself is simple: when in the state $(0,0)$ fly North.
Moreover,
$M_{1},(0,0)\models\langle\\!\langle{1}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{F}\,$:
it also has a strategy for reaching a location where it registers no
pollution. This time the simplest strategy is to fly East. In fact,
$M_{1},(0,0)\models\langle\\!\langle{1}\rangle\\!\rangle_{{}_{\\!\mathit{}}}(\mathsf{F}\,$:
there is a single strategy for achieving both goals. The drone needs to fly
East first, and then fly North.

Furthermore, no drone can assure on its own that all of the locations will
eventually be visited:
$M_{1},(0,0)\models\neg\langle\\!\langle{1}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{F}\,$.
This can only be ensured if both drones cooperate:
$M_{1},(0,0)\models\langle\\!\langle{1,2}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{F}\,$.
On the other hand, the drones are bound to end up at the target location, no
matter what they decide to do:
$M_{1},(0,0)\models\langle\\!\langle{\emptyset}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{F}\,$.
$\square$

##  3 Multi-valued domains of interpretation

As the formulas of our multi-valued version of ATL${}_{\textup{{}}}^{\ast}$
will be interpreted in distributive lattices of truth values [40], we recall
the relevant notions and results in this section.

###  3.1 Lattices of truth values

###### Definition 3.1

A lattice is a partially ordered set ${\cal L}=(\mbox{L},\leq)$, where every
pair of elements $x,y\in\mbox{L}$ has the greatest lower bound (called meet
and denoted by $x\sqcap y$) and the least upper bound (called join and denoted
by $x\sqcup y$).

Note that the meet and join of any $x,y\in\mbox{L}$ are uniquely determined
due to the antisymmetry of $\leq$.

In what follows, we only consider finite lattices. We denote the least and the
greatest elements of ${\cal L}$ by $\bot,\top$, respectively. Also, we write
(i) $x_{1}<x_{2}\mbox{ iff }x_{1}\leq x_{2}\mbox{ and }x_{1}\neq x_{2}$, and
(ii) $x_{1}\bowtie~x_{2}\mbox{ iff neither }\\\ x_{1}\leq~x_{2}\mbox{ nor
}x_{2}\leq~x_{1}$. Moreover, let:

  * •

$\uparrow x=\\{y\in L\mid x\leq y\\}$ denote the upward closure of $x$, and

  * •

$\downarrow x\>=\\{y\in L\mid y\leq x\\}$ denote the downward closure of $x$.

A lattice ${\cal L}^{\prime}=(\mbox{L}^{\prime},\leq^{\prime})$ is a
sublattice of a lattice ${\cal L}=(\mbox{L},\leq)$ if
$\mbox{L}^{\prime}\subseteq\mbox{L}$ and
$\leq^{\prime}=\leq\cap(\mbox{L}^{\prime}\times\mbox{L}^{\prime})$.

###### Definition 3.2

A lattice ${\cal L}=(\mbox{L},\leq)$ is _distributive_ if, for any
$x,y,z\in\mbox{L}$, the following two conditions hold: (i) $z\sqcup(x\sqcap
y)=(z\sqcup x)\sqcap(z\sqcup y)$, (ii) $z\sqcap(x\sqcup y)=(z\sqcap
x)\sqcup(z\sqcap y)$.

Note that, for any lattice ${\cal L}$, the operations $\sqcup$ and $\sqcap$
are associative.

$\top$$u$$\bot$ | $\top$$s$$n$$\bot$ | $\top$$a$$b$$\bot$
---|---|---
${\bf 3}$ |  ${\bf 4}$ | ${\bf 2\times 2}$

$\top$$u\sqcup i$$u$$i$$u\sqcap i$$\bot$ | $\top$$\top_{d}\sqcup\top_{g}$$\top_{d}$$\top_{g}$$u$$\bot_{d}$$\bot_{g}$$\bot_{d}\sqcap\bot_{g}$$\bot$
---|---
${\bf 2+2\times 2}$ | ${\bf 2+2\times 2+2\times 2}$

Figure 3: Distributive lattices and their join-irreducible elements

######  Example 3.3 (Some useful lattices)

Figure 3 presents five distributive lattices with applicability motivated by
clear practical intuitions. The total order ${\bf 3}$ is the most popular
lattice in multi-valued verification. The intuition is simple: $\top$ stands
for absolute truth, $\bot$ for absolute falsity, and $u$ can be read as
“unknown” or “undefined.” That is, when a formula $\varphi$ is assigned the
value $u$, this indicates that the statement represented by $\varphi$ cannot
be conclusively evaluated (its truth value – in the classical sense – cannot
be determined, or even does not exist at the moment). The lattice is very
often used in model checking approaches based on abstraction, with $u$
assigned to formulas for which the verification has proved inconclusive.

The total order ${\bf 4}$ allows for representing graded uncertainty. For
instance, in 4-valued approaches to runtime monitoring, $s$ is interpreted as
“still possibly true,” and $n$ stands for “not proved false yet.” In evidence-
based reasoning, the values can correspond to situations when there is much
(respectively, little) evidence supporting $\varphi$. The lattice can be
generalized to the $k$-valued linear order ${\bf k}$, useful in scenarios
where the amount of positive/negative evidence is weakly indicative for the
truth of a statement. Consider a corpus of data coming from event logs that
support or reject proposition

$l_{1}$$l_{2}$$l_{3}$ Figure 4: Non-distributive lattices M5 and N5

Not every lattice is distributive, as shown in Figure 4. However, distributive
lattices have a very simple characterization: a lattice is distributive iff it
contains neither M5 nor N5 as a sublattice [40].

######  Remark 3.4 (Quasi-boolean lattices and De Morgan algebras)

The operations of join and meet are natural semantic counterparts of
disjunction and conjunction. Some multi-valued approaches also add the
_complement_ operation $\sim{}\\!$ to the lattice, as the semantic counterpart
of multi-valued negation. A lattice with complement is usually called _quasi-
Boolean_ , and when distributive it is referred to as a _De Morgan algebra_.
The most popular case is the lattice underlying 3-valued Kleene logic, used
e.g. in [30, 25]. However, the choice of a generic complement to suit any
lattice is problematic from the conceptual point of view. For instance, what
should be the “opposite” value to $i$ in the lattice ${\bf 2+2\times 2}$? In
other words, if statement $\varphi$ is assessed as “inconsistent”, what should
be the evaluation of “not $\varphi$?”. There is no uniform answer to that
question, so in a general approach paper, like ours, a good strategy is to
avoid the negation as much as possible. This is why instead of negation we
have chosen to use here another non-monotonic connective: two-valued
implication representing the lattice order, which is useful in all practical
cases when we want to compare the truth values of two formulas.

###  3.2 Join-irreducible elements

###### Definition 3.5

Let ${\cal L}=(\mbox{L},\leq)$ be a lattice. An element $\ell\in\mbox{L}$ is
called join-irreducible iff $\ell\neq\bot$ and, for any $x,y\in\mbox{L}$, if
$\ell=x\sqcup y$, then either $\ell=x$ or $\ell=y$. The set of all join-
irreducible elements of ${\cal L}$ is denoted by ${\cal JI}({\cal L})$.

It is well known [41] that every element $x\neq\bot$ of a finite distributive
lattice can be uniquely decomposed into the join of all join-irreducible
elements in its downward closure, i.e.

$x=\bigsqcup({\cal JI}({\cal L})\;\cap\downarrow x)$ (1)

###### Example 3.6

The join-irreducible elements of the distributive lattices in Figure 3 are
marked with black dots. All other ones can be decomposed into the join of some
join-irreducible elements. $\square$

We will use the characterization (1) to define translations from multi-valued
to standard model checking through the following theorem.

######  Theorem 3.7 ([4])

Let ${\cal L}$ be a finite distributive lattice, and let $\ell\in{\cal
JI}({\cal L})$. Then the _threshold function_
$f_{\ell}:\mbox{L}\longrightarrow\\{\bot,\top\\}$, defined by

$f_{\ell}(x)=\left\\{\begin{array}[]{cl}\top&\text{if }x\geq\ell\\\
\bot&\text{otherwise}\end{array}\right.$

preserves arbitrary bounds, i.e., for an arbitrary set of indices $I$, we
have:

$f_{\ell}(\bigsqcap_{i\in I}x_{i})=\bigsqcap_{i\in I}f_{\ell}(x_{i})\hskip
30.00005ptand\hskip 30.00005ptf_{\ell}(\bigsqcup_{i\in
I}x_{i})=\bigsqcup_{i\in I}f_{\ell}(x_{i}).$ (2)

###### Remark 3.8

The above does not hold for lattices which are not distributive. To see this,
consider the element $\ell_{1}$ of lattice M5, which is join-irreducible.
However, $f_{\ell_{1}}$ does not preserve the upper bounds, as
$f_{\ell_{1}}(\ell_{2}\sqcup\ell_{3})=f_{\ell_{1}}(\top)=\top$ whereas
$f_{\ell_{1}}(\ell_{2})\sqcup f_{\ell_{1}}(\ell_{3})=\bot\sqcup\bot=\bot$.

##  4 Multi-valued strategic logic mv-ATL${}^{*}_{\rightarrow}$

In this section we extend the syntax and semantics of
ATL${}_{\textup{{}}}^{\ast}$ to allow for multi-valued reasoning. That is, we
propose a variant of ATL${}_{\textup{{}}}^{\ast}$ where formulas are
interpreted in an arbitrary lattice ${\cal L}=(\mbox{L},\leq)$.

It is sometimes useful to refer to logical values in the object language. To
enable this, we assume that a natural interpretation of suitable constants is
given, in the following way.

######  Definition 4.1 (Interpreted lattice)

Let $\mathcal{C}$ be a countable set of symbols. An interpreted lattice over
$\mathcal{C}$ is a triple ${\cal L}^{+}=(\mbox{L},\leq,\sigma)$, where
$(\mbox{L},\leq)$ is a lattice, and $\sigma:\mathcal{C}\rightarrow\mbox{L}$ is
an interpretation of the symbols in $\mathcal{C}$ as truth values in L.

To explicitly show the connection between the named truth values and their
names in $\mathcal{C}$, for any interpreted lattice ${\cal
L}^{+}=(\mbox{L},\leq,\sigma)$ and any truth value $x\in\sigma(\mathcal{C})$,
we will use the notation $\,\framebox{$x$}\,$ to denote an arbitrarily
selected symbol $c\in\mathcal{C}$ such that $\sigma(c)=x$. We do not make any
specific assumptions about $\sigma$. In particular, we do not assume that
$\sigma$ must be surjective, as in many situations only some truth values in L
need to be referred to in formulas. However, in all the examples that follow
in this paper, $\sigma$ actually _is_ a bijection, since every truth value
used there has a specific purpose. Thus, for all our examples, it holds that
$\mathcal{C}=\\{\,\framebox{$l$}\,\>|\>l\in\mbox{L}\\}$, and
$\sigma(\,\framebox{$x$}\,)=x$ for all $x\in\sigma(\mathcal{C})$.

###  4.1 Syntax

Since, as explained in Remark 3.4, multi-valued negation can be problematic
from the conceptual viewpoint, we will use instead the binary implication
operator $\rightarrow$ corresponding to the lattice order. Our implication
operator is similar to the well-known implication of many-valued Goedel-Dummet
logic, and in general to relevant implication or residuum of lattice meet, of
which the former is just a special case. However, our implication is a two-
valued operator, which makes it better suited for proof system purposes. As it
can be used for comparing truth values of formulas, it is of obvious practical
importance in many applications, where we are mainly interested in
ascertaining whether the truth value of a given formula $\varphi$ is greater
than the logical value of some other formula $\psi$ (see Example 4.3 below for
more explanations and illustration). Moreover, in case of two-valued logic,
classical negation can be expressed using $\rightarrow$ and the constant
representing $\bot.$

To increase the expressive power of the language, we also allow for the use of
symbols in $\mathcal{C}$.

The resulting logic is called mv-ATL${}^{*}_{\rightarrow}$ and has the
following syntax:

$\varphi::=c\mid$,

$\gamma::=\varphi\mid\gamma\land\gamma\mid\gamma\vee\gamma\mid\mathsf{X}\,\gamma\mid\gamma\,\mathsf{U}\,\gamma\mid\gamma\,\mathsf{W}\,\gamma$.

where , $A\subseteq{\mathbb{A}\mathrm{gt}}$, and $c\in\mathcal{C}$, with
$Prop$ being a countable set of atomic propositions, and $\mathcal{C}$ a
countable set of constants.

In what follows, by an implication formula we mean any formula of the form
$\varphi_{1}\rightarrow\varphi_{2}$. Additionally, we define an equivalence
formula as
$\varphi_{1}\cong\varphi_{2}=(\varphi_{1}\rightarrow\varphi_{2})\land(\varphi_{2}\rightarrow\varphi_{1})$.

The sublogic of mv-ATL${}^{*}_{\rightarrow}$ without the implication operator
will be denoted by mv-ATL${}_{\textup{{}}}^{\ast}$.

###  4.2 Semantics

The semantics of mv-ATL${}^{*}_{\rightarrow}$ is defined over concurrent game
structures with multi-valued interpretation of atomic propositions.

######  Definition 4.2 (Multi-valued CGS)

Let ${\cal L}^{+}=(\mbox{L},\leq,\sigma)$ be an interpreted lattice. A _multi-
valued concurrent game structure (mv-CGS)_ over ${\cal L}^{+}$ is a tuple
$M=\langle{{\mathbb{A}\mathrm{gt}},St,Act,d,t,Prop,\mathit{V},{\cal
L}^{+}}\rangle$, where ${\mathbb{A}\mathrm{gt}}$, $St$, $Act$, $d$, $t$,
$Prop$ are as before, and $\mathit{V}:Prop\times St\rightarrow\mbox{L}$
assigns at any state all atomic propositions with truth values from the
logical domain L.

######  Example 4.3 (Drones ctd.)

A multi-valued model of the drone scenario is presented in Figure 5. To
evaluate atomic propositions and their negations, we use the lattice ${\bf
2+2\times 2+2\times 2}$ introduced in Section 3.1. Each proposition , refers
to the level of pollution from the viewpoint of drone $i$, that is, given by
the available measurements at the current location of the drone. Whenever a
proposition evaluates to $\bot$, we omit that valuation from the picture.
$\square$

$(0,0)$$[$$[$$(1,1)$$[$$[$$(2,2)$$(3,3)_{1}$$[$$[$$[$$(3,3)_{2}$$[$$[$$[$$[$$(1,2)$$[$$(2,1)$$[$(N,N)(E,E)(N,E)(E,N)(E,E)(N,N)(E,N)(N,E)
Figure 5: Multi-valued model $M_{2}$ for the drone scenario.

Logical operators can often be naturally interpreted as either maximizers or
minimizers of the truth values. For example, disjunction ($\varphi\lor\psi$)
can be understood as a maximizer (“the most that we can hope to make of either
$\varphi$ or $\psi$”), and conjunction as a minimizer (“the least that we can
guarantee for both $\varphi$ and $\psi$”). This extends to existential
quantification (maximizing) and universal quantification (minimizing) over
paths, strategies, moments in time, etc. Formally, let
$M=\langle{{\mathbb{A}\mathrm{gt}},St,Act,d,t,Prop,\mathit{V},{\cal
L}^{+}}\rangle$ be an mv-CGS over ${\cal L}^{+}=(\mbox{L},\leq,\sigma)$. The
valuation function $[{\cdot}]$ is given as below. We sometimes use
$\bigsqcap_{X}\\{{Y}\\}$ as a shorthand for $\bigsqcap\\{{Y\mid X}\\}$, and
similarly for the supremum. For any $q\in St$ and any path $\lambda$ in $M$,
we define:

$[{c}]_{{M,q}}=\sigma(c)$ for $c\in\mathcal{C}$;

$[{\prop{p}}]_{{M,q}}=\mathit{V}($ for ;

$[{\varphi_{1}\land\varphi_{2}}]_{{M,q}}=[{\varphi_{1}}]_{{M,q}}\sqcap[{\varphi_{2}}]_{{M,q}}$;

$[{\varphi_{1}\lor\varphi_{2}}]_{{M,q}}=[{\varphi_{1}}]_{{M,q}}\sqcup[{\varphi_{2}}]_{{M,q}}$;

$[{\gamma_{1}\land\gamma_{2}}]_{{M,\lambda}}=[{\gamma_{1}}]_{{M,\lambda}}\sqcap[{\gamma_{2}}]_{{M,\lambda}}$
and
$[{\gamma_{1}\lor\gamma_{2}}]_{{M,\lambda}}=[{\gamma_{1}}]_{{M,\lambda}}\sqcup[{\gamma_{2}}]_{{M,\lambda}}$;

$[{\varphi}]_{{M,\lambda}}=[{\varphi}]_{{M,\lambda[0]}}$;

$[{\mathsf{X}\,\gamma}]_{{M,\lambda}}=[{\gamma}]_{{M,\lambda[1..\infty]}}$;

$[{\gamma_{1}\,\mathsf{U}\,\gamma_{2}}]_{{M,\lambda}}=\bigsqcup_{i\in\mathbb{N}_{0}}\bigsqcap_{0\leq
j<i}\\{{[{\gamma_{2}}]_{{M,\lambda[i..\infty]}}\sqcap[{\gamma_{1}}]_{{M,\lambda[j..\infty]}}}\\}$;

$[{\gamma_{1}\,\mathsf{W}\,\gamma_{2}}]_{{M,\lambda}}=\bigsqcap_{i\in\mathbb{N}_{0}}\\{{[{\gamma_{1}}]_{{M,\lambda[i..\infty]}}}\\}\sqcup\
\bigsqcup_{i\in\mathbb{N}_{0}}\bigsqcap_{0\leq
j<i}\\{{[{\gamma_{2}}]_{{M,\lambda[i..\infty]}}\sqcap[{\gamma_{1}}]_{{M,\lambda[j..\infty]}}}\\}$;

$[{\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\gamma}]_{{M,q}}=\bigsqcup_{s_{A}\in\Sigma_{A}}\bigsqcap_{\lambda\in
out(q,s_{A})}\\{{[{\gamma}]_{{M,\lambda}}}\\}$;

$[{[\\![{A}]\\!]\gamma}]_{{M,q}}=\bigsqcap_{s_{A}\in\Sigma_{A}}\bigsqcup_{\lambda\in
out(q,s_{A})}\\{{[{\gamma}]_{{M,\lambda}}}\\}$;

$[{\varphi_{1}\rightarrow\varphi_{2}}]_{{M,q}}=\top$ if
$[{\varphi_{1}}]_{{M,q}}\leq[{\varphi_{2}}]_{{M,q}}$ and $\bot$ otherwise.

It is worth noting that our implication operator differs from the well-known
residue of lattice meet in being two-valued — which makes it better suited for
use in any proof system, and more intuitive in specification of many
requirements.

The semantics of the two “until” operators demands a more detailed
explanation. The computation of
$[{\gamma_{1}\,\mathsf{U}\,\gamma_{2}}]_{{M,\lambda}}$ seeks to achieve a
position $i$ on path $\lambda$, for which the value of $\gamma_{2}$ at
$\lambda[i]$, and the values of $\gamma_{1}$ at all the points preceding
$\lambda[i]$, are guaranteed maximal. The semantics of
$\gamma_{1}\,\mathsf{W}\,\gamma_{2}$ is based on the well-known unfolding
$\gamma_{1}\,\mathsf{W}\,\gamma_{2}\equiv(\mathsf{G}\,\gamma_{1})\lor(\gamma_{1}\,\mathsf{U}\,\gamma_{2})$,
transformed here to a multi-valued interpretation. Note also that in case of
the derived temporal operators “sometime” and “always” the semantic rules
reduce to:

$[{\mathsf{F}\,\gamma}]_{{M,\lambda}}=\bigsqcup_{i\in\mathbb{N}}[{\gamma}]_{{M,\lambda[i..\infty]}}$;

$[{\mathsf{G}\,\gamma}]_{{M,\lambda}}=\bigsqcap_{i\in\mathbb{N}}[{\gamma}]_{{M,\lambda[i..\infty]}}$.

Thus, for instance, the formula
$\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{F}\,$ can be
read as: “the maximal level of pollution readings that $A$ can guarantee to
reach.” Clearly, such statements do not always submit to intuitive
understanding, in particular when nested strategic operators are used. Because
of that, we will stick to simple formulas in our working examples, that is,
ones that are relatively easy to read.

######  Example 4.4 (Drones ctd.)

For the model in Figure 5, we have
$[{\langle\\!\langle{1}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{F}\,\prop{pol_{1}}}]_{{M_{2},(0,0)}}=\top$:
there is a strategy for drone 1 to surely detect pollution (the strategy being
to fly North in state $(0,0)$, and then East in $(1,1)$ or $(1,2)$). Similarly
for the other drone we have
$[{\langle\\!\langle{2}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{F}\,\prop{pol_{2}}}]_{{M_{2},(0,0)}}=\top$
(the same strategy, but now executed by drone 2). On the other hand,
$[{\langle\\!\langle{1}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{G}\,\prop{pol_{1}}}]_{{M_{2},(0,0)}}=u$:
the maximal _guaranteed_ level of detection throughout the mission is $u$
(obtained by the same strategy again). This means that if drone 1 wants to
maximize its detection level, the best it can achieve is to keep it
consistently at the level of “uncertain” or higher. Finally,

$[{\langle\\!\langle{1,2}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{F}\,(\prop{target}\land\prop{allvisited}\land(\prop{pol_{1}}\lor\prop{pol_{2}}))}]_{{M_{2},(0,0)}}=\top_{d}$.

That is, if the drones cooperate, and their goal is to reach the target, visit
all the locations on the way, and at the end get the pollution detected by at
least one of them, then their degree of success is $\top_{d}$ (pollution
indicated by the drone sensor but not by the ground sensor). $\square$

The logical constants we have introduced are especially useful in implication
formulas, as the subsequent example demonstrates.

######  Example 4.5 (Implication formulas)

The “implication” operator provides several interesting specification
patterns. For instance, it allows for specifications that are accepted when
the “strength” of a property reaches a given threshold, similarly to the
probabilistic approaches of [19, 39]. As an example, the formula
$\,\framebox{$u$}\,\rightarrow\langle\\!\langle{1}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{G}\,$
can be used to specify that the truth value of
$\langle\\!\langle{1}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{G}\,$ is at
least $u$ (intuitively: there is no evidence that the formula is false). It is
easy to see that the formula is true in the model of Figure 5; formally:
$[{\,\framebox{$u$}\,\rightarrow\langle\\!\langle{1}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{G}\,\prop{pol_{1}}}]_{{M_{2},(0,0)}}=\top$.
Naturally, any stronger requirement on the value of
$\langle\\!\langle{1}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{G}\,$
evaluates to “false,” e.g.,
$[{\,\framebox{$\top$}\,\rightarrow\langle\\!\langle{1}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{G}\,\prop{pol_{1}}}]_{{M_{2},(0,0)}}=\bot$.

Moreover, the formula
$\langle\\!\langle{1}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{F}\,$ says
that the ability of drone 2 to spot pollution is at least as good as that of
drone 2 (the formula evaluates to $\top$ in $M_{2},(0,0)$). Finally,
$\langle\\!\langle{1}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{F}\,($ says
that the first drone has a strategy to ensure that it will reach a location
where only the ground sensor indicates pollution. Clearly, the last formula
evaluates to $\bot$ in $M_{2},(0,0)$. $\square$

We note that most approaches to general multi-valued model checking of
temporal specifications [3, 14, 4, 16] allow also for _multi-valued
transitions_ in the models, analogous to probabilistic transitions in Markov
chains and Markov Decision Processes. That is, transitions can be assigned
“weights” drawn from the same algebra ${\cal L}$. Similarly, most 3-valued
approaches to temporal abstraction and model checking implicitly assume
3-valued transitions by distinguishing between _may_ and _must_ transitions
[46, 20, 21, 22]. However, the two approaches differ in how such transitions
affect the semantics of formulas with universal quantification (such as “for
all paths $\gamma$”). In the general multi-valued approach, the “weaker” the
path is, the more it decreases the value of the formula. In the 3-valued
approach, “weaker” paths have less influence on the overall value. We do not
engage in this discussion here, and leave a proper treatment of multi-valued
transitions until Section 6.

###  4.3 Truth Levels

We assume that $\top$ is a single designated value, standing for full logical
truth. In consequence, the truth and validity of formulas can be defined in a
straightforward way as follows:

######  Definition 4.6 (Validity levels)

Let $M$ be mv-CGS, $q$ a state in $M$, and $\varphi$ a state formula of mv-
ATL${}^{*}_{\rightarrow}$. Then:

  * •

$\varphi$ is _true in $M,q$_ (written $M,q\models\varphi$) iff
$[{\varphi}]_{{M,q}}=\top$.

  * •

$\varphi$ is _valid in $M$_ (written $M\models\varphi$) iff $\varphi$ is true
in every state of $M$.

  * •

$\varphi$ is _valid_ (written $\models\varphi$) iff $\varphi$ is valid in
every mv-CGS $M$.

  * •

Additionally, for a path formula $\gamma$, we can say that $\gamma$ holds on
run $\lambda$ in a mv-CGS $M$ (written $M,\lambda\models\gamma$) iff
$[{\gamma}]_{{M,\lambda}}=\top$.

We now show that mv-ATL${}^{*}_{\rightarrow}$ agrees with standard
ATL${}_{\textup{{}}}^{\ast}$ on 2-valued models, unlike the 3-valued version
of ATL${}_{\textup{{}}}^{\ast}$ from [29].

###### Theorem 4.7

The logic mv-ATL${}^{*}_{\rightarrow}$ is a conservative extension of
ATL${}_{\textup{{}}}^{\ast}$, i.e., every CGS $M$ for
ATL${}_{\textup{{}}}^{\ast}$ can be identified with an mv-CGS $M^{\prime}$ for
mv-ATL${}^{*}_{\rightarrow}$ over the lattice 2 such that, for any
ATL${}_{\textup{{}}}^{\ast}$ formula $\varphi$ and any state (path) $\xi$, we
have $M^{\prime},\xi\models\varphi\mbox{ iff }M,\xi\models\varphi$.

###### Proof 4.8

For any CGS
$M=\langle{{\mathbb{A}\mathrm{gt}},St,Act,d,t,Prop,\mathit{V}}\rangle$ for
ATL${}_{\textup{{}}}^{\ast}$, let
$M^{\prime}=\langle{{\mathbb{A}\mathrm{gt}},St,Act,d,t,Prop,\mathit{V}^{\prime},{\bf
2}}\rangle$, where: (i) ${\bf 2}=(\\{\bot,\top\\},\leq,\sigma)$ is an
interpreted classical lattice of two truth values over ${\cal
C}=\\{\,\framebox{$\bot$}\,,\,\framebox{$\top$}\,\\}$ and
$\sigma(\,\framebox{$l$}\,)=l$ for any $l\in\\{\bot,\top\\}$; (ii)
$\mathit{V}^{\prime}(p,q)=\top$ if $q\in\mathit{V}(p)$ and $\bot$ otherwise.
Then $M^{\prime}$ is an mv-CGS for mv-ATL${}^{*}_{\rightarrow}$, and an easy
check shows that, for any ATL${}_{\textup{{}}}^{\ast}$ formula $\varphi$ and
any state (path) $\xi$, it indeed obtains $M^{\prime},\xi\models\varphi$ iff
$M,\xi\models\varphi$.

##  5 Model checking mv-ATL${}^{*}_{\rightarrow}$

Given an mv-CGS $M$, a state $q$ in $M$, and an mv-ATL${}^{*}_{\rightarrow}$
formula $\varphi$, the model checking problem consists in computing the value
of $[{\varphi}]_{{M,q}}$. This can be done in two ways: either by using a
dedicated algorithm, or through an efficient reduction to the ”classical”,
2-valued version of model checking. The latter option has many advantages.
First and foremost, it allows us to benefit from the ongoing developments in
2-valued model checking, including symbolic model checking techniques,
heuristics, model reduction techniques, etc. In this section, we show how
model checking of mv-ATL${}^{*}_{\rightarrow}$ can be reduced to the 2-valued
variant of this problem. Since a basic result underlying such reduction holds
for distributive lattices only, throughout the section we assume that all
lattices under consideration are distributive, unless stated to the contrary.

We emphasize again that, while multi-valued model checking typically provides
a _conceptual_ approximation of classical verification, the results in this
section are about something else. Here, we look for a _technical_ reduction
from multi-valued to two-valued model checking, with the sole purpose of
facilitating the verification process.

###  5.1 From multi-valued model checking to classical model checking

It is well known that model checking multi-valued temporal logics can be
reduced to classical, 2-valued model checking [3, 14, 15, 4]. The reduction is
of one-to-many type, i.e., a single instance of multi-valued model checking
translates to linearly many instances of classical model checking. The key
result in this respect is [3, Theorem 1]. It proposes a method for
“clustering” the truth values from lattice ${\cal L}$ into a smaller lattice
${\cal L}^{\prime}$ in such a way that the outcome of model checking is
preserved. We will now show that the analogue of that theorem holds for mv-
ATL∗, i.e., the sublanguage of mv-ATL${}^{*}_{\rightarrow}$ without the
$\rightarrow$ operator.

###### Definition 5.1

  1. 1.

By a lattice reduction triple (LRT) we mean a triple $({\cal L},{\cal
L}_{f},f)$, where ${\cal L}=(\mbox{L},\leq)$ is an arbitrary finite lattice,
${\cal L}_{f}=(\mbox{L}_{f},\leq_{f})$ its sublattice, and
$f:\mbox{L}\rightarrow\mbox{L}_{f}$ a homomorphism — a mapping which preserves
arbitrary bounds in ${\cal L}$, i.e. such that

$f(\bigsqcap_{i\in I}x_{i})=\bigsqcap_{i\in I}f(x_{i})\hskip
30.00005ptand\hskip 30.00005ptf(\bigsqcup_{i\in I}x_{i})=\bigsqcup_{i\in
I}f(x_{i})$ (3)

for an arbitrary set of indices $I$.

  2. 2.

Given an LRT $({\cal L},{\cal L}_{f},f)$ and an mv-CGS $M=$
$\langle{{\mathbb{A}\mathrm{gt}},St,Act,d,t,Prop,{\mathcal{V}},{\cal
L}^{+}}\rangle$ over an interpreted lattice ${\cal
L}^{+}=(\mbox{L},\leq,\sigma)$, by the reduction of $M$ to ${\cal L}_{f}$ via
$f$ we mean the mv-CGS
$f(M)=\langle{{\mathbb{A}\mathrm{gt}},St,Act,d,t,Prop,{\mathcal{V}}_{f},(\mbox{L}_{f},\leq_{f},\sigma_{f})}\rangle$,
where

    1. (a)

$\sigma_{f}(c)=f(\sigma(c))$ for any $c\in\mathcal{C}$, and

    2. (b)

${\mathcal{V}}_{f}(p,q)=f({\mathcal{V}}(p,q))$ for any $q\in St$ and $p\in
Prop$.

###### Definition 5.2

For any LRT $({\cal L},{\cal L}_{f},f)$ and any model $M$ over L, by the
translation condition for LRT and formula $\varphi$ we mean the relationship

$[{\varphi}]_{{M,\xi}}\in
f^{-1}(x)\qquad\mbox{iff}\qquad[{\varphi}]_{{f(M),\xi}}=x$ (4)

holding for any state (respectively, path) $\xi$.

The proof of the theorem follows easily from the key result given below:

###### Lemma 5.3

Let a state or path formula $\varphi$ be such that

$[{\varphi}]_{{M,\xi}}=\bigsqcup_{i\in I}\bigsqcap_{j_{i}\in
J_{i}}[{\varphi_{j_{i}}}]_{{M,\xi_{j_{i}}}}\;\;\;\mbox{or}\;\;\;\;[{\varphi}]_{{M,\xi}}=\bigsqcap_{i\in
I}\bigsqcup_{j_{i}\in J_{i}}[{\varphi_{j_{i}}}]_{{M,\xi_{j_{i}}}}$

for any mv-CGS $M$, any states and/or paths $\xi,\xi_{j_{i}}$ of $M$, any
countable sets $I,J_{i}$, and state (resp. path) formulas of mv-ATL∗
$\varphi_{j_{i}}$ for $j_{i}\in J_{i},i\in I$, such that all
$\varphi_{j_{i}}$’s satisfy translation condition (4). Then $\varphi$
satisfies the translation condition too.

###### Proof 5.4

We consider the case $[{\varphi}]_{{M,\iota}}=\bigsqcup_{i\in
I}\bigsqcap_{j_{i}\in J_{i}}[{\varphi_{j_{i}}}]_{{M,\iota_{j_{i}}}}$; the
other case follows by symmetry. As $f$ preserves the bounds, by the assumption
on $\varphi$ we have $f([{\varphi}]_{{M,\iota}})=\bigsqcup_{i\in
I}\bigsqcap_{j_{i}\in J_{i}}f([{\varphi_{j_{i}}}]_{{M,\iota_{j_{i}}}}\\!)$.
Each $\varphi_{j_{i}}$ satisfies (4), so
$f([{\varphi}]_{{M,\iota}})=\bigsqcup_{i\in I}\bigsqcap_{j_{i}\in
J_{i}}[{\varphi_{j_{i}}}]_{{M_{f},\iota_{j_{i}}}}=[{\varphi}]_{{M_{f},\iota}}$,
whence $[{\varphi}]_{{M_{f},\iota}}=x$ iff $[{\varphi}]_{{M,\iota}}\in
f^{-1}(x)$, and (4) holds for $\varphi$.

Now, we can formulate the reduction theorem.

######  Theorem 5.5 (Reduction theorem)

Let ${\cal L}=(\mbox{L},\leq)$ be an arbitrary finite lattice, and $({\cal
L},{\cal L}_{f},f)$ an LRT. Further, let $M$ be an mv-CGS over an interpreted
lattice ${\cal L}^{+}=(\mbox{L},\leq,\sigma)$ with
$M=\langle{{\mathbb{A}\mathrm{gt}},St,Act,d,t,Prop,{\mathcal{V}},{\cal
L}^{+}}\rangle$ , and let
$f(M)=\langle{{\mathbb{A}\mathrm{gt}},St,Act,d,t,Prop,{\mathcal{V}}_{f},(\mbox{L}_{f},\leq_{f},\sigma_{f})}\rangle$
be the image of $M$ under $f$. Then, for any state (respectively, path)
formula $\varphi$ of mv-ATL∗ over ${\cal L}$ and any state (respectively,
path) $\xi$, the following condition is satisfied:

$[{\varphi}]_{{M,\xi}}\in
f^{-1}(x)\qquad\mbox{iff}\qquad[{\varphi}]_{{f(M),\xi}}=x$ (5)

###### Proof 5.6

We use induction on the length of a formula. Equation (5) clearly holds for
propositional variables and their negations. Assume it holds for formulas of
length at most $k$, and consider formula $\varphi$ of length $k+1$. Then we
have the following cases:

  1. (a)

$\varphi=\varphi_{1}\wedge\varphi_{2}$ or
$\varphi=\varphi_{1}\vee\varphi_{2}$, where each $\varphi_{i}$ is a formula of
length at most $k$. Then
$[{\varphi_{1}}]_{{M,q}}=[{\varphi_{1}}]_{{M,q}}\sqcap[{\varphi_{2}}]_{{M,q}}$
or
$[{\varphi_{1}}]_{{M,q}}=[{\varphi_{1}}]_{{M,q}}\sqcup[{\varphi_{2}}]_{{M,q}}$,
respectively, where $\varphi_{1},\varphi_{2}$ satisfy (5). As
$[{\varphi_{1}}]_{{M,q}}$ is in one of the two dual forms prescribed by Lemma
5.3 for $I=\\{1\\}$ and $J_{1}=\\{1,2\\}$, by that lemma, $\varphi$ must
satisfy (5), too.

  2. (b)

$\gamma=\gamma_{1}\wedge\gamma_{2}$ or $\gamma=\gamma_{1}\vee\gamma_{2}$ —
analogously to (a).

  3. (c)

$\varphi={\rm X}\psi$, where $\psi$ is of length at most $k$. Then
$[{\mathsf{X}\,\gamma}]_{{M,\lambda}}=[{\gamma}]_{{M,\lambda[1..\infty]}}$,
and as $\psi$ satisfies (5) by inductive hypothesis, so obviously does
$\varphi$. The reasoning is similar to (a).

  4. (d)

$\varphi={\rm U}\psi$, where
$[{\gamma_{1}\,\mathsf{U}\,\gamma_{2}}]_{{M,\lambda}}=\bigsqcup_{i\in\mathbb{N}_{0}}\bigsqcap_{0\leq
j<i}\\{{[{\gamma_{2}}]_{{M,\lambda[i..\infty]}}\sqcap[{\gamma_{1}}]_{{M,\lambda[j..\infty]}}}\\}$;

Since the operator ${\rm U}$ corresponds to a combination of finite and
infinite lower and upper bounds applied to values of formulas of length at
most $k$ for which (5) holds, then by Lemma 5.3 Equation (5) must hold for
$\varphi$ too.

  5. (e)

$\varphi={\rm W}\psi$, where

$[{\gamma_{1}\,\mathsf{W}\,\gamma_{2}}]_{{M,\lambda}}=\bigsqcap_{i\in\mathbb{N}_{0}}\\{{[{\gamma_{1}}]_{{M,\lambda[i..\infty]}}}\\}\sqcup\bigsqcup_{i\in\mathbb{N}_{0}}\bigsqcap_{0\leq
j<i}\\{{[{\gamma_{2}}]_{{M,\lambda[i..\infty]}}\sqcap[{\gamma_{1}}]_{{M,\lambda[j..\infty]}}}\\}$;

Since the operator ${\rm W}$ corresponds to a combination of finite and
infinite lower and upper bounds applied to values of formulas of length at
most $k$ for which (5) holds, then by Lemma 5.3 Equation (5) must hold for
$\varphi$ too.

  6. (f)

$\varphi=\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\gamma$,
where $\gamma$ is of length at most $k$. Then $\gamma$ satisfies (5) by
inductive hypothesis, and as
$[{\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\gamma}]_{{M,q}}=\bigsqcup_{s_{A}\in\Sigma_{A}}\bigsqcap_{\lambda\in
out(q,s_{A})}[{\gamma}]_{{M,\lambda}}$, then $\varphi$ satisfies (5) by Lemma
5.3.

  7. (g)

$\varphi=[\\![{A}]\\!]\gamma$ — analogously to (e).

Note that the mapping $f$ can be seen as an abstraction of truth values
similar to the well-known technique of _state abstraction_ [42, 43]. That is,
we can view each value $x\in\mbox{L}_{f}$ as an _abstract truth value_
corresponding to the subset $f^{-1}(x)$ of the original truth values in L.
Clearly, those subsets partition L into equivalence classes. Theorem 5.5 says
that if $f$ satisfies conditions (3), then model checking in the abstract
model $M_{f}$ yields the equivalence class corresponding to the output of the
original model checking problem in the concrete model $M$.

How can we use Theorem 5.5 to reduce multi-valued model checking to the
2-valued case? Recall the threshold functions
$f_{\ell}:\mbox{L}\longrightarrow\\{\bot,\top\\}$, defined by

$f_{\ell}(x)=\left\\{\begin{array}[]{cl}\top&\text{if }x\geq\ell\\\
\bot&\text{otherwise}\end{array}\right.$

We already stated in Theorem 3.7 that those functions preserve bounds. The
following is an immediate corollary of the above:

###### Corollary 5.7

For any state (respectively, path) formula $\varphi$ of mv-ATL∗ and any state
(respectively, path) $\xi$, we have

$[{\varphi}]_{{M,\xi}}\geq\ell\qquad\mbox{iff}\qquad
M_{f_{\ell}},\xi\models\varphi.$ (6)

Note that each $M_{f_{\ell}}$ is a classical, 2-valued model. Together with
Equation (1), we have $[{\varphi}]_{{M,\xi}}=\bigsqcup\\{\ell\in{\cal
JI}({\cal L})\;\mid\;[{\varphi}]_{{M^{\ell},\xi}}=\top\\}$. This gives us a
simple algorithm for computing $[{\varphi}]_{{M,\xi}}$, presented in Figure 6.
The following is straightforward.

Algorithm $mcheck_{tr}(M,\xi,\varphi)$;
---
1. For every join-irreducible logical value $\ell\in{\cal JI}({\cal L})$, model-check (classically) $\varphi$ in ${M_{f_{\ell}},\xi}$; 2. Collect the values of $\ell$ for which the answer was “yes” in a set $\mathcal{X}$; 3. Return the join of the values in $\mathcal{X}$, i.e., $\bigsqcup\mathcal{X}$.
Figure 6: Translation-based model checking for mv-ATL∗

###### Theorem 5.8

The one-to-many reduction from multi-valued model checking of mv-ATL∗ to
2-valued model checking of ATL${}_{\textup{{}}}^{\ast}$ runs in linear time
with respect to the size of the model and the number of truth values.

######  Example 5.9 (Testing of the drones)

Consider the pollution monitoring scenario from the previous examples. Suppose
that we want to test the design of a drone patrol before its deployment in the
physical environment. One way to carry out offline testing is to model-check
the relevant properties of the design against a randomly generated sample of
area maps. For the clarity of the examples we have used a crafted by hand map.
For the map in Figure 1 and the mv-CGS $M_{2}$ in Figure 5, we obtain the
collection of classical models presented in Figure 8. Note that projections
$(M_{2})_{f_{\top}}$ and $(M_{2})_{f_{\top\\!_{g}}}$ are in fact identical,
and similarly for $(M_{2})_{f_{\bot_{d}}}$, $(M_{2})_{f_{\bot_{g}}}$, and
$(M_{2})_{f_{\bot_{d}\sqcap\bot_{g}}}$.

Suppose now that we want to compute the value of
$\langle\\!\langle{1,2}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{F}\,($ in
$M_{2},(0,0)$. The formula holds in state $(0,0)$ of models
$(M_{2})_{f_{\top\\!_{d}}}$, $(M_{2})_{f_{\bot_{d}}}$,
$(M_{2})_{f_{\bot_{g}}}$, and $(M_{2})_{f_{\bot_{d}\sqcap\bot_{g}}}$, but not
in $(M_{2})_{f_{\top}}$ and $(M_{2})_{f_{\top\\!_{g}}}$. Thus, the output of
model checking is
$\top_{d}\,\sqcup\,\bot_{d}\,\sqcup\,\bot_{g}\,\sqcup\,(\bot_{d}\sqcap\bot_{g})=\top_{d}$.
Moreover, to model-check
$\langle\\!\langle{1}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{F}\,$, we
observe that the formula holds in all the projection models in Figure 8. Thus,
its value in $M_{2},(0,0)$ is
$\top\,\sqcup\,\top_{d}\,\sqcup\,\top_{g}\,\sqcup\,\bot_{d}\,\sqcup\,\bot_{g}\,\sqcup\,(\bot_{d}\sqcap\bot_{g})=\top$.
$\square$

|
$(0,0)$$(1,1)$$(2,2)$$(3,3)_{1}$$(3,3)_{2}$$(1,2)$$(2,1)$(N,N)(E,E)(N,E)(E,N)(E,E)(N,N)(E,N)(N,E)
---
|
$(0,0)$$(1,1)$$(2,2)$$(3,3)_{1}$$(3,3)_{2}$$(1,2)$$(2,1)$(N,N)(E,E)(N,E)(E,N)(E,E)(N,N)(E,N)(N,E)
---
$(M_{2})_{f_{\top}}$ and $(M_{2})_{f_{\top\\!_{g}}}$ | $(M_{2})_{f_{\top\\!_{d}}}$

|
$(0,0)$$(1,1)$$(2,2)$$(3,3)_{1}$$(3,3)_{2}$$(1,2)$$(2,1)$(N,N)(E,E)(N,E)(E,N)(E,E)(N,N)(E,N)(N,E)
---
$(M_{2})_{f_{\bot_{d}}}$, $(M_{2})_{f_{\bot_{g}}}$, and
$(M_{2})_{f_{\bot_{d}\sqcap\bot_{g}}}$

Figure 7: Model translations for the drone scenario

Algorithm $gmcheck_{tr}(M,\varphi)$;
---
1. Set the initial valuation of $\varphi$ to ${\mathcal{V}}_{\varphi}$ such that ${\mathcal{V}}_{\varphi}(q)=\bot$ for every $q\in St$; 2. For every join-irreducible logical value $\ell\in{\cal JI}({\cal L})$: $\bullet$ Compute the set of states $Q_{\ell}$ that (classically) satisfy $\varphi$ in $M_{f_{\ell}}$; $\bullet$ For each $q\in Q_{\ell}$, do ${\mathcal{V}}_{\varphi}(q):={\mathcal{V}}_{\varphi}(q)\sqcup\ell$; 3. Return ${\mathcal{V}}_{\varphi}$.

Figure 8: Translation-based global model checking for mv-ATL∗

The algorithm in Figure 6 is an example of _local_ model checking. That is,
given a state (respectively, path) and a formula, it returns the truth value
of the formula in that state (respectively, on that path). In two-valued modal
logics, verification of state formulas is often done by means of _global model
checking_ that returns the exact set of states where the input formula holds.
For many logics – including ATL${}_{\textup{{}}}$ and
ATL${}_{\textup{{}}}^{\ast}$– this provides strictly more information with no
extra computational cost. The analogous problem for multi-valued modal logics
would ask for a _valuation_ of the input formula, i.e., a mapping from the
states of the model to the truth values of $\varphi$. A global model checking
algorithm for mv-ATL∗, based on the translation to two-valued model checking,
is presented in the next section, in Figure 8.

###  5.2 Translating implication formulas: Impossibility result

Unfortunately, Theorem 5.5 cannot be extended to mv-ATL${}^{*}_{\rightarrow}$,
i.e., to the full language containing implication formulas of the form
$\varphi_{1}\rightarrow\varphi_{2}$, where $\rightarrow$ represents the
lattice order.

###### Proposition 5.10

There are lattice reduction triples and formulas of mv-
ATL${}^{*}_{\rightarrow}$ that do not satisfy translation condition (5).

###### Proof 5.11

Consider the lattice ${\cal L}_{o}=(\mbox{L}_{o},\leq)$, where
$\mbox{L}_{o}=\\{0,...,k-1,k,...,2k-1\\}$, and $\leq$ is the usual total order
on $\mbox{L}_{o}$. Clearly, in ${\cal L}_{o}$ we have $0=\bot$ and $2k-1=\top$
according to our lattice notation. Then $(\\{0,2k-1\\},\leq)$ is a sublattice
of ${\cal L}_{o}$ and the reduction $f:\mbox{L}_{o}\rightarrow\\{0,2k-1\\}$
given by $f(x)=2k-1$ if $x\geq k$, and $f(x)=0$ if $x<k$ preserves the bounds
in ${\cal L}_{o}$. Thus $({\cal L}_{o},\\{0,2k-1\\},f)$ is a lattice reduction
triple.

Now take arbitrary $k_{1},k_{2}$ such that $0<k_{1}<k_{2}<k$, and an mv-CGS
$M$ over ${\cal L}_{o}^{+}=({\cal L}_{o},\sigma)$ for an arbitrary
$\sigma:\mathcal{C}\rightarrow\mbox{L}_{o}$ such that, for some state $q\in
St$ of $M$ and atomic propositions $p_{1},p_{2}\in Prop$, we have
$V(p_{i},q)=k_{i}$ for $i=1,2$.

Next, let $\varphi=p_{2}\rightarrow p_{1}$. Since $[{p_{i}}]_{{M,q}}=k_{i}$
for $i=1,2$ and $k_{2}>k_{1}$, we have
$\neg([{p_{2}}]_{{M,q}}\leq[{p_{1}}]_{{M,q}})$, whence
$[{\varphi}]_{{M,q}}=0$.

However, for the model $M_{1}$ obtained from $M$ with the reduction $f$ we get
$[{p_{i}}]_{{M_{1},q}}=0$ for $i=1,2$ (as $k_{i}<k$, $f(k_{i})=0$ for
$i=1,2$), where $[{p_{2}}]_{{M_{1},q}}\leq[{p_{1}}]_{{M_{1},q}}$, which
implies $[{\varphi}]_{{M_{1},q}}=2k-1$. Yet, as
$f^{-1}(2k-1)=\\{k,k+1,...,2k-1\\}$ we have $[{\varphi}]_{{M,q}}=0\not\in
f^{-1}(2k-1)$, which contradicts Equation (5).

The above result can be generalized as follows:

###### Theorem 5.12

If ${\cal L}=(\mbox{L},\leq)$ of Theorem 5.5 contains a chain or anti-chain of
cardinality $n$, and ${\cal L}^{\prime}=(\mbox{L}^{\prime},\leq^{\prime})$ is
a sublattice of ${\cal L}$ of cardinality $n^{\prime}<n$, then there is no
function $f:\mbox{L}\rightarrow\mbox{L}^{\prime}$ satisfying translation
condition (5) if the language under consideration contains implication
formulas.

###### Proof 5.13

Assume $X=\\{x_{1},x_{2},\ldots,x_{n}\\}$ is a chain or anti-chain in $L$. Let
$M$ be a model such that, for some state $s\in Q$ of $M$ and propositional
variables $p_{1},p_{2},\ldots,p_{n}\in Prop$, we have $V(s,p_{i})=k_{i}$ for
$i=1,2,\ldots,n$. Consider any $f:L\rightarrow L^{\prime}$. As
$card(L^{\prime})=n^{\prime}<n$, than there must be $k,l\in\\{1,\ldots,n\\}$
such that $k\neq l$ and $f(x_{k})=f(x_{l})$. Let

$\varphi=\left\\{\begin{array}[]{ll}p_{l}\rightarrow p_{k}&\mbox{if $X$ is a
chain and $x_{k}<x_{l}$}\\\ p_{k}\rightarrow
p_{l}&\mbox{otherwise}\end{array}\right.$

Then, clearly, $x_{l}\not\leq x_{k}$ (note that if $X$ is an anti-chain, then
$x_{r}\not\leq x_{q}$ for any $1\leq r,s\leq n$). Hence
$[{p_{l}}]_{{M,q}}\not\leq[{p_{k}}]_{{M,q}}$, and $[{\varphi}]_{{M,q}}=\bot$.
However, as $f(x_{k})=f(x_{l})$, we have
$[{p_{l}}]_{{M_{1},q}}\leq[{p_{k}}]_{{M_{1},q}}$, whence
$[{\varphi}]_{{M_{1},q}}=\top$. Thus $f$ does not satisfy Equation (5).

In other words, if the size of the target lattice ${\cal L}^{\prime}$ is
strictly smaller than the “diameter” of the source lattice ${\cal L}$ (that
is, the cardinality of the longest chain or antichain in ${\cal L}$), then a
“clustering” of truth values from ${\cal L}$ into ${\cal L}^{\prime}$ that
preserves Equation (5) is impossible. Note that the diameter of _any_ lattice
with more than 2 values must be at least 3, and hence it exceeds the size of
the classical 2-valued lattice 2. The following is an immediate consequence of
the above:

###### Corollary 5.14

For any multi-valued lattice ${\cal L}$ there is no reduction of ${\cal L}$ to
the 2-valued lattice of classical truth values that satisfies the translation
condition (5) for the whole language of mv-ATL${}^{*}_{\rightarrow}$.

###  5.3 Translating implication formulas even more impossible

We already know that there is no general translation from multi-valued to two-
valued model checking for implication formulas. Now we will show that the
impossibility result can be extended to any “clustering” of truth values from
the original lattice ${\cal L}$. To this end, we give a necessary and
sufficient condition for the existence of a function $f:L\rightarrow L_{f}$
that preserves bounds in ${\cal L}$ and satisfies the translation condition
(5) also for implication formulas.

The following lemma states that, in order to obtain the analogue of Theorem
5.5 for implication formulas, the mapping $f$ would have to preserve both the
ordering and incomparability of the elements in ${\cal L}$.

###### Lemma 5.15

Let $({\cal L},{\cal L}_{f},f)$ be a lattice reduction triple, let $M$ be an
mv-CGSs over L, and $f(M)$ its reduction to ${\cal L}_{f}$. Then translation
condition (5) of that theorem is satisfied for all implication formulas iff
the following conditions hold:

  1. C1:

$(\forall x_{1},x_{2}\in\mbox{L})\ [x_{1}<x_{2}\ \Rightarrow\
f(x_{1})<f(x_{2})]$

  2. C2:

$(\forall x_{1},x_{2}\in\mbox{L})\ [x_{1}\bowtie x_{2}\ \Rightarrow\
f(x_{1})\bowtie f(x_{2})]$

###### Proof 5.16

Note that an implication formula is a state formula, and that for any such
formula $\psi$ we have $[{\psi}]_{{M,q}}\in\\{\bot,\top\\}$ for any mv-CGS $M$
and any $q\in St$. Thus in order to prove (5) for such formulas, it suffices
to show that, for any implication formula $\varphi$ and any state $q$:

$[{\varphi}]_{{M_{f},q}}=\top\mbox{ iff }[{\varphi}]_{{M,q}}\in f^{-1}(\top)$
(7)

“(7) $\boldsymbol{\Rightarrow}$ (C1 $\land$ C2)”: We start by proving the
necessity of conditions C1 and C2. Assume first that $f$ satisfies (7) for
implication formulas. We should prove that $f$ satisfies Conditions C1, C2 for
all such formulas. For what follows, denote $\xi=p_{1}\rightarrow
p_{2},\psi=p_{2}\rightarrow p_{1}$, where $p_{1},p_{2}\in Prop$, $p_{1}\neq
p_{2}$ where $Prop$ is the set of atomic propositions of our logic).

C1:

We argue by contradiction. Suppose $x_{1},x_{2}\in\mbox{L},x_{1}<x_{2}$ and
$f(x_{1})\geq f(x_{2})$. Then, as $x_{1}<x_{2}$ implies $x_{1}\leq x_{2}$ and
$f$ preserves bounds, we also have $f(x_{1})\leq f(x_{2})$, whence
$f(x_{1})=f(x_{2})$.

Now let $M$ be an mv-CGS over ${\cal L}$ such that, for some state $q\in St$,
we have $V(p_{i},q)=x_{i}$ for $i=1,2$, and let $M_{f}$ be the image of $M$
under $f$. Since $\psi=p_{2}\rightarrow p_{1}$ and
$[{p_{2}}]_{{M,q}}=x_{2}>x_{1}=[{p_{1}}]_{{M,q}}$, we have
$[{\psi}]_{{M,q}}=\bot$. However, $[{\psi}]_{{M_{f},q}}=\top$, because
$[{p_{2}}]_{{M_{f},q}}=f(x_{2})=f(x_{1})=[{p_{1}}]_{{M_{f},q}}$. As
$\bot\not\in f^{-1}(\top)$, this contradicts (7).

C2:

We again argue by contradiction. Suppose $x_{1},x_{2}\in L,x_{1}\bowtie x_{2}$
and $\neg(f(x_{1})\bowtie f(x_{2}))$. Without any loss of generality, we can
assume that $f(x_{1})\leq f(x_{2})$. Let mv-CGSs $M,M_{f}$ and state $q$ of
$M$ be like in the preceding item. Then, as $[{p_{1}}]_{{M,q}}=x_{1}\bowtie
x_{2}=[{p_{2}}]_{{M,q}}$, we have in particular
$[{p_{1}}]_{{M,q}}\not\leq[{p_{2}}]_{{M,q}}$. Since $\xi=p_{1}\rightarrow
p_{2}$, this implies $[{\xi}]_{{M,q}}=\bot$. In turn,
$[{\xi}]_{{M_{f},q}}=\top$, because $[{p_{1}}]_{{M_{f},q}}=f(x_{1})\leq
f(x_{2})=[{p_{2}}]_{{M_{f},q}}$, which again contradicts (7).

“(C1 $\land$ C2) $\boldsymbol{\Rightarrow}$ (7)”: It remains to prove the
sufficiency of conditions C1 and C2. We assume that C1, C2 hold, and prove
that (7) holds for formulas of the form
$\varphi=\varphi_{1}\rightarrow\varphi_{2}$. We start by proving this result
for non-nested implication formulas, i.e., we assume that
$\varphi_{1},\varphi_{2}$ do not contain $\rightarrow$. Then, by Theorem 5.5,
(7) holds for $\varphi_{1},\varphi_{2}$, which implies that

$[{\varphi_{i}}]_{{M_{f},q}}=f([{\varphi_{i}}]_{{M,q}}),\ \ i=1,2.\ \ \ \ $
(8)

“(7L) $\Rightarrow$ (7R)”: We begin with the forward implication in (7).
Assume that $[{\varphi}]_{{M_{f},q}}=\top$. Then
$[{\varphi_{1}}]_{{M_{f},q}}\leq[{\varphi_{2}}]_{{M_{f},q}}$. By (8), this
implies $f([{\varphi_{1}}]_{{M,q}})\leq f([{\varphi_{2}}]_{{M,q}}$. We show by
contradiction that

$[{\varphi_{1}}]_{{M,q}}\leq[{\varphi_{2}}]_{{M,q}}.$ (9)

Suppose that (9) does not hold, then we have two possible cases:

Case 1:

$[{\varphi_{1}}]_{{M,q}}>[{\varphi_{2}}]_{{M,q}}$. Then by C1 we have
$f([{\varphi_{1}}]_{{M,q}})>f([{\varphi_{2}}]_{{M,q}})$, whence from (8) we
get $[{\varphi_{1}}]_{{M_{f},q}}>[{\varphi_{2}}]_{{M_{1},q}}$ and
$[{\varphi}]_{{M_{f},q}}=\bot$ — which is a contradiction.

Case 2:

$[{\varphi_{1}}]_{{M,q}}\bowtie[{\varphi_{2}}]_{{M,q}}$. Then
$f([{\varphi_{1}}]_{{M,q}})\bowtie f([{\varphi_{2}}]_{{M,q}})$ by C2, whence
from (8) we get
$\neg([{\varphi_{1}}]_{{M_{f},q}}\leq[{\varphi_{2}}]_{{M_{f},q}})$.
Consequently, $[{\varphi}]_{{M_{f},q}}=\bot$ — which is again a contradiction.

Thus (9) above holds, whence $[{\varphi}]_{{M,q}}=\top\in f_{1}(\top)$, and
the forward implication in (7) holds.

“(7R) $\Rightarrow$ (7L)”: The final step is proving the backward implication
in (7). Assume that $[{\varphi}]_{{M,q}}=f^{-1}(\top)$. As
$[{\varphi}]_{{M,q}}\in\\{\bot,\top\\}$ and $f(\bot)\neq\top$ by the
preservation of bounds by $f$ and the non-triviality of $L,L_{f}$, we obtain
$[{\varphi}]_{{M,q}}=\top$, whence
$[{\varphi_{1}}]_{{M,q}}\leq[{\varphi_{2}}]_{{M,q}}$. Since $f$ preserves
bounds, this implies $f([{\varphi_{1}}]_{{M,q}})\geq
f([{\varphi_{2}}]_{{M,q}})$, whence from (8) we obtain
$[{\varphi_{1}}]_{{M_{1},q}}\leq[{\varphi_{2}}]_{{M_{f},q}}$. This yields
$[{\varphi}]_{{M_{f},q}}=\top$, whence the backward implication in (7) holds,
too.

Nested formulas: The proof for nested formulas proceeds by induction. Assume
that (7) holds for implication formulas with $\rightarrow$ nested at most $k$
times, and assume $\varphi$ is an implication formula with $\rightarrow$
nested $k+1$ times. Then $\varphi=\varphi_{1}\rightarrow\varphi_{2}$, where
$\rightarrow$ is nested at most $k$ times in $\varphi_{1},\varphi_{2}$.
Consequently, by the inductive assumption (9) holds for
$\varphi_{1},\varphi_{2}$, and repeating the proof given above for implication
formulas without nesting of $\rightarrow$ we can show that (7) holds for
$\varphi$ too.

This completes the proof of the sufficiency of C1, C2 for all implication
formulas, and the proof of Lemma 5.15.

From Lemma 5.15 we can easily derive by induction the following general
result:

###### Theorem 5.17

Let the $({\cal L},{\cal L}_{f},f)$ be an LRT. Then, the translation condition
is satisfied for all formulas of mv-ATL${}^{*}_{\rightarrow}$ over ${\cal L}$
iff conditions C1, C2 of Lemma 5.15 hold.

It can be seen that conditions C1, C2 imply that any translation $f$ meeting
them must preserve the exact structure of the lattice ${\cal L}$. An important
consequence of that fact is:

###### Corollary 5.18

Given a lattice ${\cal L}=(\mbox{L},\leq)$ and its sublattice ${\cal
L}_{f}=(\mbox{L}_{f},\leq_{f})$, any function
$f:\mbox{L}\rightarrow\mbox{L}_{f}$ preserving the algebra bounds and
satisfying translation condition (5) for all implication formulas must be one-
to-one.

###### Proof 5.19

Suppose that $f$ satisfies the above assumption, $x_{1},x_{2}\in L$ and
$x_{1}\neq x_{2}$. Then we have one of the following cases:

  1. 1.

$x_{1}<x_{2}$ or $x_{2}<x_{1}$. Then $f(x_{1})\neq f(x_{2})$ by C1 of Theorem
5.17.

  2. 2.

$x_{1}\bowtie x_{2}$. Then $f(x_{1})\bowtie f(x_{2})$ by C2 of Theorem 5.17,
which again implies $f(x_{1})\neq f(x_{2})$.

The meaning of Corollary 5.18 is that there is no way of reducing $n$-valued
model checking to $k$-valued model checking for $k<n$, if we want to handle
all implication formulas. Clearly, Corollary 5.14 in Section 5.2 is a special
case of the above result.

###  5.4 Translation of model checking for _some_ implication formulas

By Corollary 5.7, there is a simple translation from multi-valued to classical
model checking for strategic and temporal operators. By Corollary 5.18, we
know that it cannot be generally extended to implication formulas. The next
question is: can we construct such a translation for _some_ implication
formulas? If so, for which ones? The impossibility result in Corollary 5.18 is
due to the fact that implication formulas can be used to encode the semantics
in the language — including in particular its $n$-valued character. However,
one usually wants to model-check one formula at a time. Then, Theorem 5.17 can
be in some cases modified to provide the desired reduction:

###### Theorem 5.20

Let $({\cal L},\mbox{L}_{f},f)$ be a lattice reduction triple (LRT), let $M$
be a CGS over ${\cal L}$ and $f(M)$ its reduction to ${\cal L}_{f}$. Further,
let $\varphi$ be a formula of mv-ATL${}^{*}_{\rightarrow}$ and $Sub(\varphi)$
the set of all its subformulas. Then $\varphi$ satisfies translation condition
(5) whenever, for any implication formula $\phi\in Sub(\varphi)$ such that
$\phi=\varphi_{1}\rightarrow\varphi_{2}$, any state (resp. path) $\xi$, and
$x_{i}=[{\varphi_{i}}]_{{M,\xi}},i=1,2,$ the following conditions hold:

C1’: $x_{1}<x_{2}\ \Rightarrow\ f(x_{1})<f(x_{2})$ |  |  |  C2’: $x_{1}\bowtie x_{2}\ \Rightarrow\ f(x_{1})>f(x_{2})$
---|---|---|---

###### Proof 5.21

To prove the thesis, we assume that C1’, C2’ are satisfied, and show by
structural induction that translation condition (5)

$[{\psi}]_{{M_{f},\xi}}=x\ \ \ \ {\rm iff}\ \ \ \ \ [{\psi}]_{{M,\xi}}\in
f^{-1}(x)$

holds for any $\psi\in Sub(\varphi)$.

For atomic or constant $\psi$, the thesis follows from Theorem 5.5. Suppose
now that Equation (5) holds for all subformulas of $\varphi$ having rank $k$,
and assume $\psi$ is of rank $k+1$. If $\psi$ is obtained from subformulas of
rank at most $k$ using any operator $Op$ other than $\rightarrow$, then
Equation (5) follows from the fundamental Lemma 5.3.

Thus, it remains to consider the case of $\rightarrow$. Assume
$\psi=\psi_{1}\rightarrow\psi_{2}$, with Equation (5) being satisfied for both
$\psi_{1},\psi_{2}$. Since $\psi$ is an implication formula, according to what
we have already noted in the proof of Lemma 5.15, proving (5) for $\psi$
reduces to showing condition (7), i.e.,

$[{\psi}]_{{M_{f},q}}=\top\ \ \ \ {\rm iff}\ \ \ \ \ [{\psi}]_{{M,q}}\in
f^{-1}(\top).$

Note that since $\psi_{1},\psi_{2}$ are in $Sub(\varphi)$, then C1’, C2’ hold
for $x_{i}=[{\varphi_{i}}]_{{M,q}},i=1,2$. By the inductive assumption, we
also have

$[{\psi_{i}}]_{{M_{f},q}}=f([{\psi_{i}}]_{{M,q}}),\ \ i=1,2\ \vspace*{1mm}$
(10)

“$\boldsymbol{\Rightarrow}$”: We begin with the forward implication in (7).
Assume that $[{\psi}]_{{M_{f},q}}=\top$. Then
$[{\psi_{1}}]_{{M_{f},q}}\leq[{\psi_{2}}]_{{M_{f},q}}$. By (10), this implies
$f([{\psi_{1}}]_{{M,q}})\leq f([{\psi_{2}}]_{{M,q}}$. We show by contradiction
that it implies

$[{\psi_{1}}]_{{M,q}}\leq[{\psi_{2}}]_{{M,q}}$ (11)

Suppose that (11) does not hold, then we have two possible cases:

Case 1: $[{\psi_{1}}]_{{M,q}}>[{\psi_{2}}]_{{M,q}}$. Then by condition C1’ we
have $f([{\psi_{1}}]_{{M,q}})>f([{\psi_{2}}]_{{M,q}})$, whence from (10) we
get $[{\psi_{1}}]_{{M_{f},q}}>[{\psi_{2}}]_{{M_{f},q}}$ and
$[{\psi}]_{{M_{f},q}}=\bot$, which is a contradiction.

Case 2: $[{\psi_{1}}]_{{M,q}}\bowtie[{\psi_{2}}]_{{M,q}}$. Then
$f([{\psi_{1}}]_{{M,q}})>f([{\psi_{2}}]_{{M,q}})$ by condition C2’, which
again leads to a contradiction by what we have already proved for Case 1.

Thus (11) above holds, whence $[{\psi}]_{{M,q}}=\top\in f^{-1}(\top)$, and the
forward implication in (7) holds.

“$\boldsymbol{\Leftarrow}$”: The final step consists in proving the backward
implication in (7). Assume that $[{\psi}]_{{M,q}}=f^{-1}(\top)$. As
$[{\psi}]_{{M,q}}\in\\{\bot,\top\\}$ and $f(\bot)\neq\top$ by the preservation
of bounds by $f$ and the non-triviality of ${\cal L},{\cal L}_{f}$, we get
$[{\psi}]_{{M,q}}\\!=\\!\top$, and consequently
$[{\psi_{1}}]_{{M,q}}\leq[{\psi_{2}}]_{{M,q}}$. Since $f$ preserves bounds,
this implies $f([{\psi_{1}}]_{{M,q}})\leq f([{\psi_{2}}]_{{M,q}})$, whence
from (10) we obtain $[{\psi_{1}}]_{{M_{f},q}}\leq[{\psi_{2}}]_{{M_{f},q}}$.
This yields $[{\psi}]_{{M_{f},q}}=\top$, whence the backward implication in
(7) holds, too.

Assume that our mv-CGSs are defined over distributive lattices. We now show
that the translation method of Section 5.1, based on join irreducible elements
${\cal JI}({\cal L})$, can be applied to a formula $\varphi$ of
ATL${}_{\textup{{}}}^{\ast}$ and an mv-CGS $M$, provided that the assumptions
of Theorem 5.20 are satisfied. By (1), for each $x\in\mbox{L}$ we have
$x=\bigsqcup({\cal JI}({\cal L})\;\cap\downarrow x)$. Let $M^{\ell}$ be the
model obtained using the translation $f_{\ell}$. Therefore, according to
Theorem 5.20: $[{\varphi}]_{{M^{\ell},\xi}}=x\mbox{ iff
}[{\varphi}]_{{M,\xi}}\in f_{\ell}^{-1}(x)$ whence
$[{\varphi}]_{{M^{\ell},\xi}}=\top\mbox{ iff
}[{\varphi}]_{{M,\xi}}\in\;\uparrow\\!\ell$. Thus,

$[{\varphi}]_{{M,\xi}}=\bigsqcup\\{\ell\in{\cal JI}({\cal
L})\;\mid\;[{\varphi}]_{{M^{\ell},\xi}}=\top\\}.$ (12)

###### Example 5.22

Consider model $M_{2}$ in Figure 5 and formula
$\phi=\langle\\!\langle{1}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{G}\,($.
Subformula can take the following truth values throughout the model:
$\bot,u,\top\\!_{d},\top$. Similarly, can evaluate to $\bot,\top\\!_{d}$. Thus
by Theorem 5.20 mapping $f_{\top\\!_{d}}$ meets translation condition (5), and
we can use the translation method of Section 5.1 to check if the value of
$\phi$ is at least $\top\\!_{d}$.

On the other hand, all the other “cutoff” mappings (i.e.,
$f_{\bot_{d}\sqcap\bot_{g}},f_{\bot_{d}},f_{\bot_{g}},f_{\top\\!_{g}}$, and
$f_{\top}$) do not satisfy condition C1’, and hence the correctness of the
translation is not guaranteed for those truth values.

The following is an immediate consequence of Theorem 5.20.

###### Corollary 5.23

Let ${\cal L}$, its sublattice ${\cal L}_{f}$,
$f:\mbox{L}\rightarrow\mbox{L}_{f}$, and $M,M_{f}$ be as in Theorem 5.5.
Further, let $\varphi$ be a formula of mv-ATL${}^{*}_{\rightarrow}$ such that
every implication subformula of $\varphi$ is of the form
$\psi_{1}\rightarrow\psi_{2}$, where
$\psi_{i}\in\\{\,\framebox{$\bot$}\,,\,\framebox{$\top$}\,\\}$ for some
$i\in\\{1,2\\}$. Then $\varphi$ satisfies the translation condition (5).

###### Proof 5.24

It suffices to observe that if at least one of the formulas
$\psi_{1},\psi_{2}$ is either $\,\framebox{$\bot$}\,$ or
$\,\framebox{$\top$}\,$, then the implication subformula
$\psi_{1}\rightarrow\psi_{2}$ trivially satisfies conditions C1’ and C2’ of
Theorem 5.20.

###  5.5 Recursive model checking of ATL${}_{\textup{{}}}^{\ast}$

Algorithm $gmcheck_{rec}(M,\varphi)$;
---
1. If $\varphi$ contains no instance of the comparison operator $\rightarrow$, then return $gmcheck_{tr}(M,\varphi)$; 2. Else, pick the first implication subformula $\varphi_{1}\rightarrow\varphi_{2}$ in $\varphi$, and: $\bullet$ Compute ${\mathcal{V}}_{\varphi_{1}}:=gmcheck_{rec}(M,\varphi_{1})$ and ${\mathcal{V}}_{\varphi_{2}}:=gmcheck_{rec}(M,\varphi_{2})$; $\bullet$ Create an extension $M^{\prime}$ of model $M$ by adding a fresh atomic proposition , and fixing its valuation so that $V($ if ${\mathcal{V}}_{\varphi_{1}}(q)\leq{\mathcal{V}}_{\varphi_{2}}(q)$ and $V($ otherwise; $\bullet$ Create formula $\varphi^{\prime}$ by replacing every occurrence of $\varphi_{1}\rightarrow\varphi_{2}$ by ; $\bullet$ Return $gmcheck_{rec}(M^{\prime},\varphi^{\prime})$.
Figure 9: Recursive global model checking for ATL${}_{\textup{{}}}^{\ast}$

For many model checking instances, the assumptions of Theorem 5.20 do not
hold. In those cases, we cannot translate the multi-valued model checking of
mv-ATL${}^{*}_{\rightarrow}$ formulas to the classical model checking for
ATL${}_{\textup{{}}}^{\ast}$. Then, the simplest solution is to adapt the
standard recursive algorithm that, in order to model-check formula $\varphi$,
proceeds bottom-up from the simplest subformulas, and replaces them with fresh
atomic propositions. In our case, this means that model checking of each
implication formula $\varphi_{1}\rightarrow\varphi_{2}$ consists in computing
the values of $\varphi_{1},\varphi_{2}$ by means of the translation in Section
5.1, and then fixing the valuation of the fresh variable according to their
comparison. The detailed algorithm is presented in Figure 9.

The main disadvantage of the above method compared to the direct translation
method is that it requires computing the values of the new atomic propositions
for all states of the model $M$. In other words, we need to carry out global
model checking, whereas for formulas without the implication operator
$\rightarrow$ both global and local model checking were possible. The method
can be possibly improved if we assume that a specific symbolic model checking
method for two-valued ATL${}_{\textup{{}}}^{\ast}$ is used; we leave a study
of this subject for future work.

Nevertheless, the algorithm presented in Figure 9 has two important
consequences. First, it provides a general linear-time reduction from model
checking mv-ATL${}^{*}_{\rightarrow}$ (resp. mv-ATL→) to model checking
standard 2-valued ATL${}_{\textup{{}}}^{\ast}$ (resp. ATL${}_{\textup{{}}}$).
We state it formally as follows.

###### Theorem 5.25

The one-to-many reduction from multi-valued model checking of mv-
ATL${}^{*}_{\rightarrow}$ to 2-valued model checking of
ATL${}_{\textup{{}}}^{\ast}$ runs in linear time with respect to the size of
the model, the length of the formula, and the number of truth values.

###### Corollary 5.26

Model checking mv-ATL${}^{*}_{\rightarrow}$ (resp. mv-ATL→) is
$\mathbf{{2EXPTIME}}$-complete (resp. $\mathbf{{P}}$-complete) in the size of
the model, the length of the formula, and the number of truth values.

Secondly, we note that correctness of the translation does not depend on the
type of strategies being used in the semantics of mv-
ATL${}^{*}_{\rightarrow}$. As it is, the translation provides a model checking
reduction to the IR variant of ATL${}_{\textup{{}}}^{\ast}$ (perfect
information + perfect recall). If we used memoryless strategies of type
$s_{a}:St\to Act$ instead of perfect recall, the translation would yield
reduction to the Ir variant of ATL${}_{\textup{{}}}^{\ast}$ (perfect
information + imperfect recall [44]). Since the IR and Ir semantics coincide
in 2-valued ATL${}_{\textup{{}}}$ (though not in
ATL${}_{\textup{{}}}^{\ast}$!), we get the following.

###### Theorem 5.27

For mv-ATL→, memory is irrelevant, i.e., its semantics can be equivalently
given by memoryless strategies.

##  6 Multi-valued transitions

In this paper our aim is to propose a framework for a graded interpretation of
logical statements referring to the strategic ability of agents and
coalitions. Until this point, the “graded” truth values have only originated
from non-classical interpretation of atomic propositions and literals.
Typically, this happens because when constructing a model we cannot determine
the truth of some basic statements in absolute terms (as either true or
false). Instead, we assign such basic statements with their ”truth degrees”
(which can be also seen as “weights of evidence”) drawn from a suitable
lattice, which then propagate to more complex formulas.

Another source of non-classical truth values sometimes considered in the
literature is a graded interpretation of transitions. In that case, each
transition is labelled according to its “strength.” An extension of mv-
ATL${}^{*}_{\rightarrow}$ with weighted transitions is discussed in this
section.

###  6.1 Weighted transitions: Potential interpretations

The shift from 2-valued to multi-valued modal logic typically arises when we
extend the domain of interpretation for atomic propositions in _states_ of the
model. The level of truth for , is not crisp anymore, and this propagates to
more complex formulae $\varphi$ via semantic clauses. So far, we have assumed
that the transition relation is crisp, i.e., given states $q,q^{\prime}$ and a
vector of actions $\vec{\alpha}$, the transition from $q$ to $q^{\prime}$
labeled by $\vec{\alpha}$ is either fully included in the model, or is
completely absent from it. An alternative would be to consider multi-valued
transition relations, with transitions that are possible to a certain degree.

There are at least two sensible interpretations of such weighted transitions.
On the one hand, the weight can be interpreted as the strength of evidence
supporting the existence of the transition. This approach has been adopted in
the previous works on multi-valued temporal logics over arbitrary lattices of
truth values [3, 4], with the additional assumption that the weights of
transitions are drawn from the same lattice as the values of propositions. A
characteristic feature of the semantics in [3, 4] is that, whenever the
weights on transitions decrease sufficiently, the value of a temporal formula
must also decrease. Formally, consider a multi-valued transition system $M$, a
state $q$ in $M$, and a formula $\mathsf{A}\mathsf{X}\,\varphi$ such that
$[{\mathsf{A}\mathsf{X}\,\varphi}]_{{M,q}}=x$. Moreover, let $M^{\prime}$ be
the same as $M$ except for the weights of all the outgoing transitions from
$q$ being strictly lower than $x$. Then we have
$[{\mathsf{A}\mathsf{X}\,\varphi}]_{{M^{\prime},q}}<[{\mathsf{A}\mathsf{X}\,\varphi}]_{{M,q}}$.
Analogous characterizations can be shown for all other temporal operators.

On the other hand, the transition weights can be also interpreted as a
qualitative distribution, similarly to quantitative transitions in Markov
chains and Markov decision processes, used in the semantics of probabilistic
temporal logics [45, 35, 19] and their strategic variants [38, 39, 31, 33,
34]. A natural assumption in that case is that the distribution is complete.
In the probabilistic case, it amounts to the weights on the outgoing edges
from $q$ always summing up to $1$. The requirement is essential in models of
multi-agent systems, where establishing what _cannot_ happen is often as
important as reasoning about what can.

In the qualitative case, at a minimum, $[{\varphi}]_{{M,q^{\prime}}}=x$ on all
the successors $q^{\prime}$ of $q$ should imply
$[{\mathsf{A}\mathsf{X}\,\varphi}]_{{M,q}}=x$ (and analogously for other
temporal operators and strategic operators). In particular, if the value of
$\varphi$ is bound to be $\top$ at the next moment – no matter how the systems
evolves – then $\mathsf{A}\mathsf{X}\,\varphi$,
$\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{X}\,\varphi$,
etc., should also evaluate to $\top$. It is easy to see that the semantics in
[3, 4] do not satisfy this requirement.

In the remainder of the section, we outline how the probabilistic approach can
be adapted to arbitrary lattices of transition weights. Our proposal is based
on the concept of _designated paths_ , i.e., paths that are considered
relevant in a given context. We also show that the idea of may/must
abstraction can be seen as a special, 3-valued case of this kind of reasoning.

###  6.2 Weighted transitions in concurrent game structures

######  Definition 6.1 (Weighted multi-valued CGS)

Assume two lattices: an interpreted lattice ${\cal
L}^{+}=(\mbox{L},\leq,\sigma)$ of truth values, and a lattice ${\cal
L}_{t}=(\mbox{L}_{t},\leq_{t})$ for weights that will be assigned to
transitions. A _weighted multi-valued concurrent game structure (wmv-CGS)_
over ${\cal L}^{+}$ and ${\cal L}_{t}$ is a tuple
$M=\langle{{\mathbb{A}\mathrm{gt}},St,Act,d,t,w,Prop,\mathit{V},{\cal
L}^{+},{\cal L}_{t}}\rangle$, where ${\mathbb{A}\mathrm{gt}}$, $St$, $Act$,
$t$, $Prop$ are as in case of an mv-CGS, and $w:t\rightarrow\mbox{L}_{t}$ is a
weight function which maps each individual transition in $t$ (i.e., each tuple
$(q,\alpha_{1},\dots,\alpha_{k},t(q,\alpha_{1},\dots,\alpha_{k}))$ to a value
in $\mbox{L}_{t}$.

The interpretation of mv-ATL${}^{*}_{\rightarrow}$ formulas in a wmv-CGS $M$
as above is parameterized by the set ${\cal D}$ of designated values in ${\cal
L}_{t}$ — the logical values whose assignment to a formula makes it deemed to
be satisfied.

A path in an wmv-CGS is defined analogously as in an mv-CGS. A path
$\lambda=q_{0}q_{1}q_{2}\dots$ is said to be designated if for every $i$ there
are actions $\alpha_{1},\dots,\alpha_{k}$ such that
$t(q_{i},\alpha_{1},\dots,\alpha_{k})=q_{i+1}$ and
$w(q_{i},\alpha_{1},\dots,\alpha_{k},q_{i+1})\in{\cal D}$.

Given ${\cal D}$, we reduce a wmv-CGS $M$ to an mv-CGS

$M_{\cal D}=\langle{{\mathbb{A}\mathrm{gt}},St,Act,d,t_{\cal
D},Prop,\mathit{V},{\cal L}^{+}}\rangle$

where

$t_{\cal
D}(q,\alpha_{1},\dots,\alpha_{k})=\left\\{\begin{array}[]{ll}t(q,\alpha_{1},\dots,\alpha_{k})&\mbox{if
}w(q,\alpha_{1},\dots,\alpha_{k},t(q,\alpha_{1},\dots,\alpha_{k}))\in{\cal
D}\\\ \mbox{undefined}&\mbox{otherwise}\end{array}\right.$

Then any state of $M$ is a state of $M_{\cal D}$, and any designated path in
$M$ is a path in $M_{\cal D}$. As the interpretation of mv-
ATL${}^{*}_{\rightarrow}$ in $M$ we take the interpretation of mv-
ATL${}^{*}_{\rightarrow}$ in $M_{\cal D}$:

For any state or designated path $\xi$ in $M$ and any formula $\varphi$ in mv-
ATL${}^{*}_{\rightarrow}$, we take:

$[{\varphi}]_{{M,\xi,{\cal D}}}=[{\varphi}]_{{M_{\cal D},\xi}}$ (13)

###  6.3 Embedding may/must abstractions

A natural example of many-valued transitions is provided by may-must
transitions: the “may” transitions are only possible, but need not happen,
while the “must” transitions will necessarily take place. This kind of models
were used in [46]. Also, the may/must abstractions presented in [28, 29, 30]
produce models with the same or similar structure and interpretation. Adapting
the notation, those models take the form
$M^{GJ}=\langle{St,Prop,\delta_{must},\delta_{may},V,{\cal L}}\rangle$, where
$St,Prop,V$ are defined as before, ${\cal L}=\\{\mbox{\bf t},\mbox{\bf
f},\mbox{\bf u}\\}$, and $\delta_{must}$, $\delta_{may}\subseteq St\times St$
are transition relations such that $\delta_{must}\subseteq\delta_{may}$. The
language contains negation and conjunction interpreted as in Kleene three-
valued calculus over $\\{\mbox{\bf t},\mbox{\bf f},\mbox{\bf u}\\}$, and the
$AX$ operator interpreted as:

$\begin{array}[]{ll}[{AX\varphi}]_{{M^{GJ},q}}=\left\\{\begin{array}[]{ll}\mbox{\bf
t}&\mbox{if $\forall
s^{\prime}(\delta_{may}(s,s^{\prime})\Rightarrow[{\varphi}]_{{M^{GJ},s^{\prime}}}=\mbox{\bf
t}$})\\\ \mbox{\bf f}&\mbox{if $\exists
s^{\prime}(\delta_{must}(s,s^{\prime})\wedge[{\varphi}]_{{M^{GJ},s^{\prime}}}=\mbox{\bf
f}$})\\\ \mbox{\bf u}&\mbox{otherwise}\end{array}\right.\par\end{array}$

If, following [46], we disregard explicit inclusion of agents and actions in
our approach, then if the transition relation $\delta_{may}$ is a function,
such a model can be represented as an wmv-CGS
$M^{JKP}=\langle{St,\delta_{may},Prop,\mathit{V},{\cal L}^{+},{\cal
L}_{t}}\rangle$ with three-valued transitions, where $LT=\\{\top,U,\bot\\}$,
and the weight function $w:St\times St\rightarrow LT$ is defined by:

$w(s,s^{\prime})=\left\\{\begin{array}[]{ll}\top&\mbox{if
$(s,s^{\prime})\in\delta_{must}$}\\\ U&\mbox{if
$(s,s^{\prime})\in\delta_{may}\setminus\delta_{must}$}\\\
\bot&\mbox{otherwise}\end{array}\right.$

Denote ${\cal D}_{\top}=\\{\top\\},{\cal D}_{U}=\\{U,\top\\}$. We can show
that Godefroid’s-Jagadessan’s semantics based on $M^{GJ}$ can be expressed
using our model $M^{JKP}$ as follows:

###### Lemma 6.2

If $\varphi$ does not contain the $AX$ operator, then:

  1. 1.

$[{\varphi}]_{{M^{GJ},q}}=[{\varphi}]_{{M^{JKP},q,{\cal D}_{\top}}}$

  2. 2.

$[{AX\varphi}]_{{M^{GJ},q}}=\left\\{\begin{array}[]{ll}\mbox{\bf t}&\mbox{if
$[{AX\varphi}]_{{M^{JKP},q,{\cal D}_{U}}}=\mbox{\bf t}$}\\\ \mbox{\bf
f}&\mbox{if $[{AX\varphi}]_{{M^{JKP},q,{\cal D}_{\top}}}=\mbox{\bf f}$}\\\
\mbox{\bf u}&\mbox{otherwise}\end{array}\right.$

###### Proof 6.3

Since both $M^{JKP}$ and $M^{GJ}$ are based on Kleene 3-valued calculus of
propositional formulas, Condition 1 obviously holds. Further, as the
translation of $M^{JKP}$ to $M_{D_{U}}$ preserves all transitions in
$\delta_{may}$, we have $[{AX\varphi}]_{{M^{JKP},q,{\cal D}_{U}}}=\mbox{\bf
t}$ iff $[{\varphi}]_{{M^{JKP},q^{\prime},{\cal D}_{U}}}=\mbox{\bf t}$ for
every $(q,q^{\prime})\in\delta_{may}$. In view of Condition 1, the latter
implies $[{\varphi}]_{{M^{GJ},q^{\prime}}}=\mbox{\bf t}$ for every
$(q,q^{\prime})\in\delta_{may}$. Consequently, the first clause in Condition 2
holds. For the second clause, note that as $M_{D_{\top}}$ only contains
transitions in $\delta_{must}$, then $[{AX\varphi}]_{{M^{JKP},q,{\cal
D}_{\top}}}=\mbox{\bf f}$ iff there is a transition
$(q,q^{\prime})\in\delta_{must}$ such that
$[{\varphi}]_{{M^{JKP},q^{\prime}}}=\mbox{\bf f}$. Then by Condition 1
$[{\varphi}]_{{M^{GJ},q^{\prime}}}=\mbox{\bf f}$, whence
$[{AX\varphi}]_{{M^{GJ},q}}=\mbox{\bf f}$ — and so Condition 2 holds.

###  6.4 Model checking multi-valued CGS with weighted transitions

Fortunately, the introduction of weighted transition, while enriching our
models and making them better suited to some practical applications, does not
introduce any essential complications into model-checking compared to mv-CGS’s
with two-valued transitions. Thus the results obtained in the latter case
carry over to mv-CGS, and we have the following generalization of the
Reduction Theorem 5.5:

###### Theorem 6.4

Let ${\cal L}=(\mbox{L},\leq)$ be an arbitrary finite lattice, ${\cal
L}_{f}=(\mbox{L}_{f},\leq_{f})$ a sublattice of ${\cal L}$, and let
$f:\mbox{L}\rightarrow\mbox{L}_{f}$ a mapping which preserves arbitrary bounds
in ${\cal L}$. Furthermore, let $M=$
$\langle{{\mathbb{A}\mathrm{gt}},St,Act,d,t,w,Prop,{\mathcal{V}},{\cal
L}^{+}}\rangle$ be an wmv-CGS over an interpreted lattice ${\cal
L}^{+}=(\mbox{L},\leq,\sigma)$ over ${\cal C}$, and let
$M_{f}=\langle{{\mathbb{A}\mathrm{gt}},St,Act,d,t,w_{f},Prop,{\mathcal{V}}_{f},(\mbox{L}_{f},\leq_{f},\sigma_{f})}\rangle$
be the mv-CGS obtained from $M$ by “clustering” the truth values in $M$
according to $f$, i.e.:

  1. 1.

$\sigma_{f}(c)=f(\sigma(c))$ for any $c\in\mathcal{C}$,

  2. 2.

$w_{f}(\tau)=f(w(\tau)))$ for any $\tau\in t$, and

  3. 3.

$V_{f}(p,q)=f(V(p,q))$ for any $q\in St$ and $p\in Prop$.

Then, for any state (respectively, path) formula $\varphi$ of mv-
ATL${}^{*}_{\rightarrow}$ over ${\cal L}$, any state (respectively, path)
$\xi$, and any set of designated truth values ${\cal D}$, we have

$[{\varphi}]_{{M,\xi,{\cal D}}}\in
f^{-1}(x)\qquad\mbox{iff}\qquad[{\varphi}]_{{M_{f},\xi,{\cal D}}}=x$ (14)

###### Proof 6.5

Straightforward from Equation (13) and Theorem 5.5.

Note that the conditions of the above theorem (preservation of the bounds plus
Conditions 1 and 3) correspond to those of Theorem 5.4 , with an analogous
Condition 2 for weights added).

This theorem can be used, in a way analogous to that employed for mv-
ATL${}^{*}_{\rightarrow}$ with two-valued transitions, to reduce mv-model
checking for mv-ATL${}^{*}_{\rightarrow}$ with mv-transitions to two-valued
model checking. This is because the semantics of mv-ATL${}^{*}_{\rightarrow}$
with many-valued transitions contains an embedded reduction of models with mv-
transitions to models with two-valued transitions — and for those models we
can again use the reduction based on our threshold functions. Consequently,
the local and global model checking algorithm given in Figure 9 and Figure 8
also carry-over to the case of many-valued transitions.

Like previously, the positive results quoted above apply to formulas which do
not involve the implication operator. For the formulas involving that
operator, the negative result obtained in case of two-valued transitions of
course still holds — because a CGS with two-valued transitions is just a
special case of a CGS with many-valued transitions.

##  7 Multi-valued verification of agents with imperfect information

ATL${}_{\textup{{}}}$ and ATL${}_{\textup{{}}}^{\ast}$ were originally
proposed for reasoning about agents in perfect information scenarios. It can
be argued that realistic multi-agent systems always include some degree of
limited observability [44, 47, 48, 49, 50, 51, 52]. However, model checking of
ATL${}_{\textup{{}}}$ and ATL${}_{\textup{{}}}^{\ast}$ with imperfect
information is hard – more precisely,
$\mathbf{{\Delta_{{2}}^{\mathbf{{P}}}}}$\- to $\mathbf{{PSPACE}}$-complete for
agents playing memoryless strategies [44, 53, 54] and undecidable for agents
with perfect recall [55]. Furthermore, the imperfect information semantics of
strategic ability does not admit standard fixpoint equivalences [56], which
makes incremental synthesis of strategies cumbersome. Practical attempts at
the problem have emerged only recently [57, 58, 59, 60, 61, 62], and the
experimental results show that verification is feasible only for very small
models.

Such hard problems can be potentially tackled by means of approximation
techniques [30, 63]. In particular, abstraction techniques [42, 30, 23] can be
used to cluster multiple states and/or transitions in the system into
_abstract_ states and transitions, thus reducing the model size. However, in
order to be effective, the abstraction must be very coarse, which potentially
results in loss of information about the truth of (some) atomic propositions
and the existence of (some) transitions. This leads to a substantial reduction
of the verification cost, possibly at the expense of introducing non-classical
truth values of propositions in some abstract states, as well as transitions
of various strength. In consequence, multi-valued model checking can be
extremely useful when reasoning about strategies under uncertainty.

Clearly, all the previously cited reasons for using multi-valued verification
(description of the world based on a non-classical notion of truth, lifting
the logical reasoning to a richer domain of answers, inconclusive or
inconsistent information about the system, conflicting evidence coming from
different sources, inconclusive verification procedure, etc.) are also
relevant for agents with uncertainty. In this section, we show that the
framework of mv-ATL${}^{*}_{\rightarrow}$ can be easily extended to the case
of imperfect information.

###  7.1 Logic mv-ATL${}^{*}_{\rightarrow}$ with imperfect information

Let us extend mv-CGS with epistemic indistinguishability relations
$\sim_{1},\dots,\sim_{k}\subseteq St\times St$, one per agent in
${\mathbb{A}\mathrm{gt}}$. The idea is that, whenever $q\sim_{a}q^{\prime}$
and the system is in state $q$, agent $a$ might think that the system is
actually in $q^{\prime}$. Each $\sim_{a}$ is assumed to be an equivalence
relation. We also assume that the resulting model is _uniform_ with respect to
the indistinguishability relations, i.e., $q\sim_{a}q^{\prime}$ implies
$d_{a}(q)=d_{a}(q^{\prime})$. In other words, the choices available to an
agent are identical in the states indistinguishable for that agent.

In a similar way, strategies under imperfect information must specify
identical choices in indistinguishable situations. That is, memoryless
strategies with imperfect information (ir strategies, for short) are functions
$s_{a}:St\to Act$ such that $q\sim_{a}q^{\prime}$ implies
$s_{a}(q)=s_{a}(q^{\prime})$. Moreover, perfect recall strategies with
imperfect information (shortly: iR strategies) are functions $s_{a}:St^{+}\to
Act$ st. $q_{0}\sim_{a}q_{0}^{\prime},\dots,q_{n}\sim_{a}q_{n}^{\prime}$
implies $s_{a}(q_{0}\dots q_{n})=s_{a}(q_{0}^{\prime}\dots q_{n}^{\prime})$.
Again, collective strategies for $A\subseteq{\mathbb{A}\mathrm{gt}}$ are
tuples of individual strategies for $a\in A$. We denote them by
$\Sigma_{A}^{\textit{ir}}$ and $\Sigma_{A}^{\textit{iR}}$, respectively.

The semantics of mv-ATL${}^{*}_{\mathfrak{S}\rightarrow}$, parameterized by
the type of strategies
$\mathfrak{S}=\textit{IR},\textit{Ir},\textit{ir},\textit{iR}$, can be defined
by replacing the clause for the strategic operators from Section 4 as follows:

$[{\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\gamma}]_{{M,q}}^{\mathfrak{S}}\
=\ \bigsqcup_{s_{A}\in\Sigma_{A}^{\mathfrak{S}}}\bigsqcap_{\lambda\in
out(q,s_{A})}\\{{[{\gamma}]_{{M,\lambda}}^{\mathfrak{S}}}\\}$;

$[{[\\![{A}]\\!]\gamma}]_{{M,q}}^{\mathfrak{S}}\ =\
\bigsqcap_{s_{A}\in\Sigma_{A}^{\mathfrak{S}}}\bigsqcup_{\lambda\in
out(q,s_{A})}\\{{[{\gamma}]_{{M,\lambda}}^{\mathfrak{S}}}\\}$.

$(0,0)$$[$$[$$(1,1)$$[$$[$$(2,2)$$(3,3)_{1}$$[$$[$$[$$(3,3)_{2}$$[$$[$$[$$[$$(1,2)$$[$$(2,1)$$[$$(3,1)_{2}$$[$$[$$[$$(3,1)_{1}$$[$$[$$(3,2)_{1}$$[$$(3,2)_{2}$$[$$[$$2$$2$$2$$2$$2$$2$$1,2$$2$$1,2$$2$$1,2$$1,2$$1,2$$1,2$$1,2$$1,2$(N,N)(E,E)(N,E)(E,N)(E,E)(E,N)(N,N)(N,E)(E,N)(E,E)(N,N)(N,E)
Figure 10: Multi-valued model $M_{3}$ for drones with imperfect information.
Epistemic indistinguishability is depicted by dotted lines.

######  Example 7.1 (Drones with partial information)

Consider again the drone model introduced in Example 4.3 and Figure 5. We
assume now that drone $1$ sees its own position but not that of drone $2$,
whereas drone $2$ only sees if the other drone is in the same location but
does not recognize the location itself. Moreover, each drone can identify the
initial state (i.e., $(0,0)$), as well as recognize that it has run out of
battery (states $(3,3)_{1}$ and $(3,3)_{2}$). Finally, drone $2$ – not knowing
its exact position – may try to fly in a direction which is not available for
a given location (e.g., fly North in location $2$). In that case, the attempt
fails, and the drone stays in its current location. The updated mv-CGS $M_{3}$
is presented in Figure 10.

For the formulas from Example 4.4, we now have :

  * •

$[{\langle\\!\langle{1}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{F}\,\prop{pol_{1}}}]_{{M_{2},(0,0)}}^{\textit{ir}}=[{\langle\\!\langle{1}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{F}\,\prop{pol_{1}}}]_{{M_{2},(0,0)}}^{\textit{iR}}=\top$,
as the strategy to fly North in state $(0,0)$, and then East in $(1,1)$ or
$(1,2)$ is uniform for drone $1$;

  * •

$[{\langle\\!\langle{2}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{F}\,\prop{pol_{2}}}]_{{M_{2},(0,0)}}^{\textit{ir}}=[{\langle\\!\langle{2}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{F}\,\prop{pol_{2}}}]_{{M_{2},(0,0)}}^{\textit{iR}}=\top$
(the analogous strategy for drone $2$ is _not_ uniform, but the agent can
achieve the goal by playing $N$ in all the states);

  * •

$[{\langle\\!\langle{1,2}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{F}\,(\prop{target}\land\prop{allvisited}\land(\prop{pol_{1}}\lor\prop{pol_{2}}))}]_{{M_{2},(0,0)}}^{\textit{ir}}=\bot$
because neither of the uniform memoryless strategies leads to a state where
holds;

  * •

$[{\langle\\!\langle{1,2}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{F}\,(\prop{target}\land\prop{allvisited}\land(\prop{pol_{1}}\lor\prop{pol_{2}}))}]_{{M_{2},(0,0)}}^{\textit{iR}}=\top_{d}$
(example strategy: drone $1$ flies North in the first step, and East in the
second, while drone $2$ moves East and then North). $\square$

Objective vs. subjective semantics of ability. We note that the above semantic
rule corresponds to the notion of _objective ability_. That is, given a
strategy, we only look at its outcome paths starting from the current global
state of the system $q$. The alternative, _subjective ability_ , requires the
strategy to succeed on all the paths starting from states indistinguishable
from $q$. Let $\sim_{a}\\!\\!(q)=\\{q^{\prime}\mid q\sim_{a}q^{\prime}\\}$.
This can be formalized by the following adaptation of the semantic rule:

$[{\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\gamma}]_{{M,q}}^{\mathfrak{S}}\
=\ \bigsqcup_{s_{A}\in\Sigma_{A}^{\mathfrak{S}}}\bigsqcap_{a\in
A}\bigsqcap_{q^{\prime}\in\sim_{a}(q)}\bigsqcap_{\lambda\in
out(q^{\prime},s_{A})}\\{{[{\gamma}]_{{M,\lambda}}^{\mathfrak{S}}}\\}$;

$[{[\\![{A}]\\!]\gamma}]_{{M,q}}^{\mathfrak{S}}\ =\
\bigsqcap_{s_{A}\in\Sigma_{A}^{\mathfrak{S}}}\bigsqcup_{a\in
A}\bigsqcup_{q^{\prime}\in\sim_{a}(q)}\bigsqcup_{\lambda\in
out(q^{\prime},s_{A})}\\{{[{\gamma}]_{{M,\lambda}}^{\mathfrak{S}}}\\}$.

A more detailed discussion on the epistemic aspects of strategic ability can
be found in [64, 65]. We leave the proper treatment of diverse epistemic
variants of mv-ATL${}^{*}_{\rightarrow}$ for the future.

###  7.2 Model checking techniques and formal results

We emphasize again that the correctness of the techniques proposed in Section
5 _does not depend on the actual definition of the strategy sets
$\Sigma_{A}$_. In consequence, the results carry over to the imperfect
information case, and the techniques can be applied _in exactly the same way_
to obtain model checking reductions from mv-
ATL${}^{*}_{\mathfrak{S}\rightarrow}$ to the corresponding 2-valued cases.
This demonstrates the power of the translation method that can be directly
applied to a vast array of possible semantics for
ATL${}_{\textup{{}}}^{\ast}$. Again, multi-valued verification of mv-
ATL${}^{*}_{\mathfrak{S}\rightarrow}$ incurs only linear increase in the
complexity compared to the 2-valued case.

##  8 Case study: Multi-valued verification of the drone model

Besides the theoretical results discussed in the preceding sections, we
present an experimental evaluation of our approach to verification of
strategic abilities. To this end, we propose a new scalable benchmark based on
the running example employed throughout the paper. We use the CGS template of
the team of drones patrolling for pollution in a city (cf. Examples 4.3 and
7.1, as well as the graphs in Figures 5 and 10), but with a more complex map
to make the study more realistic. The details and outcomes of the experiments
are presented further on in this section.

###  8.1 Model description

The benchmark is an extension of the drone model used in the previous
sections. To recall, we consider a number of drones flying over a fixed area,
with each drone modeled as a separate agent. The map is represented by a
directed graph that defines the locations $Loc$ and the paths used by the
agents to move between those locations. We employ the map shown in Figure 11.
For the experiments, we assume that the connections between locations are
symmetric (i.e., can be traversed both ways), and hence an undirected graph is
a sufficient representation of the map.

Figure 11: The map used in the experiments

The system consists of a number of drone agents and the environment. The set
of all drones is denoted by $D$. A drone can use its sensors to measure the
pollution at its current location. Moreover, it can communicate with the other
drones at the same and adjacent locations using bluetooth, and obtain their
current readings. The readings from all the ground sensors are broadcasted by
the monitoring center, and hence are available to all drones at all times.
This is modeled by an epistemic indistinguishability relation, with the
following information available to the drone:

  * •

Its current position (i.e., a location number);

  * •

Reading from the drone sensor in its current position;

  * •

Readings from the adjacent drones;

  * •

Readings from all the ground sensors;

  * •

A battery charge level;

  * •

A set of already visited places.

We assume that the time span of the mission is at most $30$ mins (currently,
there are still relatively few types of drones that can fly longer than a
couple of minutes, and they are mostly used in industrial and military
contexts). With this provision, we can assume that the environment is
stationary throughout the mission. That is, while traversing the map the
drones will always get the same readings from a given location.

Each drone can perform five possible actions: _go North_ , _South_ , _East_ ,
_West_ , and _Wait_. Any movement consumes energy. When the battery level
drops to zero, the only action that the drone can perform is _Wait_. This
means it will stay at its current location forever (since our model does not
feature battery recharging). However, such an immobilized drone can still
broadcast information to the nearby drones.

As before, we use multi-valued atomic propositions , $d\in D$, with values
drawn from the lattice ${\bf 2+2\times 2+2\times 2}$. The interpretation of is
given by the combined readings of drone $d$’s sensor and of the ground sensor
at the current location of $d$.

The models are scaled with respect to the following parameters:

  * •

Number of drones;

  * •

Initial battery level (the same for each drone).

###  8.2 Formulas

In the rest of this section,

###### Proposition 169

d will refer to an arbitrary drone in the set $D$. The first formula to be
verified is

$\phi_{1}\quad=\quad\mathsf{E}\mathsf{F}\,$

It says that if drone $d$ _might_ detects pollution to some degree, then $d$
has a strategy to guarantee that this will indeed be the case. Note that the
formula is an implication, and hence – due to the results in Section 5.2 – a
straightforward reduction to classical model checking is problematic. Because
of that, we use the recursive reduction algorithm of Section 5.5. That is, we
split $\phi_{1}$ into its left hand side ($\mathsf{E}\mathsf{F}\,$) and right
hand side
($\langle\\!\langle{d}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{F}\,$). We
also observe that the left hand side of the implication, expressed in ATL and
transformed to the negation normal form, becomes
$[\\![{\emptyset}]\\!]\mathsf{F}\,$. Thus, in order to determine the value of
$\phi_{1}$, we need to carry out multi-valued model checking of the following
two formulas:

  * •

$\phi_{1L}\ =[\\![{\emptyset}]\\!]\mathsf{F}\,$, and

  * •

$\phi_{1R}\
=\langle\\!\langle{d}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{F}\,$,

each of them satisfying the preconditions of Theorem 5.5.

We observe that the above specification is relatively weak: it requires that
if pollution is present somewhere then the drone is able to find it at some
location. In order to allow for a finer-grained specification, we add to the
drone model a family of atomic propositions with classical, 2-valued
interpretation. More precisely, evaluates to $\top$ in the states where drone
$d$ is at location $loc\in Loc$, and to $\bot$ everywhere else. In addition,
we allow for cooperation between the drones. More exactly, we will be looking
at joint strategies of the team of all drones $D$ with the following property:
if any of the drones might detect pollution at location $loc$, then the drones
can ensure that one of them will indeed detect it:

$\phi_{2}\quad=\quad\bigwedge_{loc\in Loc}\
\big{(}\mathsf{E}\mathsf{F}\,\bigvee_{d\in D}($

Again, the formula is an implication, and thus requires separate treatment of
the left and right hand sides of “$\rightarrow$.” Here, we only report the
verification results for the right-hand subformula, i.e.:

  * •

$\phi_{2R}^{loc}\
=\langle\\!\langle{D}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{F}\,\bigvee_{d\in
D}($

for an arbitrary selected value of $loc$.

The considered formulas emphasize the importance of the comparison operator
$\rightarrow$ for actual specification of properties. Many (if not most)
relevant properties of multi-agent systems are expressed as an implication: if
the assumptions are satisfied, the target property should hold as well. The
multi-valued variant of such requirements demands that $\psi$ is satisfied to
at least the same degree as $\varphi$.

###  8.3 Semantics and algorithms

We note that formula $\phi_{1L}$ refers only to the abilities of the empty
coalition, and hence does not involve reasoning about imperfect information.
In consequence, one can as well evaluate it using the perfect information
semantics of mv-ATL∗. Then, the translation in Section 5.1 reduces the multi-
valued verification of $\phi_{1L}$ to model checking of 2-valued
ATL${}_{\textup{{}}}$ with perfect information. We implement the latter by
means of the standard fixpoint algorithm from [2].

In contrast, the semantics of formulas $\phi_{1R}$ and $\phi_{2R}$ refers to
strategies with imperfect information. Accordingly, the translation in Section
5.1 reduces the problem to model checking of 2-valued ATL${}_{\textup{{}}}$
with imperfect information. Since the exact model checking of abilities under
imperfect information is hard, both theoretically [44, 66] and in practice [9,
67, 57], we go around the complexity by using the fixpoint-based approximate
model checking algorithm proposed recently in [63]. That is, the 2-valued
model checking of $\phi_{1R}$ proceeds by a model-independent translation to
its upper and lower variants $\phi_{1R}^{U},\phi_{1R}^{L}$, both of which can
be verified by fixpoint algorithms. If the verification output for
$\phi_{1R}^{U}$ and $\phi_{1R}^{L}$ matches, it is guaranteed correct for
$\phi_{1R}$, too; otherwise, the outcome is inconclusive. The 2-valued model
checking for $\phi_{2R}$ is obtained analogously.

As we will see, the output of the lower and the upper approximation always
matched in our experiments (cf. Figures 14 and 14), thus providing fully
conclusive outcome.

###  8.4 Experimental results

The results of the experiments are presented in Figures 12 (for formula
$\phi_{1L}$), 14 (formula $\phi_{1R}$), and 14 (formula $\phi_{2R}$). For each
of the formulas, we considered several configurations of the drone model. The
main scaling factor was the number of the drones in the system. The second
source of complexity was the initial energy level (the same for every drone).
The initial location on the map was always 0, for all the drones in the
system.

#drones |  |  energy  | #states | tgen |  | tverif | output
---|---|---|---|---|---|---|---
1 |  |  1  | 5 | 0.007 |  | 0.01 | $\top_{g}$
1 |  |  2  | 14 | 0.005 |  | 0.05 | $\top_{d}\sqcup\top_{g}$
1 |  |  3  | 32 | 0.02 |  | 0.10 | $\top_{d}\sqcup\top_{g}$
1 |  |  4  | 61 | 0.04 |  | 0.26 | $\top$
1 |  |  5  | 106 | 0.03 |  | 0.38 | $\top$
1 |  |  10  | 601 | 0.37 |  | 2.13 | $\top$
1 |  |  100  | 16740 | 8.84 |  | 85.91 | $\top$
1 |  |  1000  | 178740 | 85.85 |  | timeout | $-$
2 |  |  1  | 17 | 0.01 |  | 0.08 | $\top_{g}$
2 |  |  2  | 98 | 0.05 |  | 0.54 | $\top_{d}\sqcup\top_{g}$
2 |  |  3  | 422 | 0.34 |  | 2.16 | $\top_{d}\sqcup\top_{g}$
2 |  |  4  | 1263 | 1.23 |  | 6.32 | $\top$
2 |  |  5  | 3288 | 3.83 |  | 16.77 | $\top$
2 |  |  10  | 55757 | 89.23 |  | 719.81 | $\top$
2 |  |  100  | $-$ | timeout |  | $-$ | $-$
3 |  |  1  | 65 | 0.02 |  | 0.46 | $\top_{g}$
3 |  |  2  | 794 | 1.02 |  | 5.34 | $\top_{d}\sqcup\top_{g}$
3 |  |  3  | 6626 | 12.44 |  | 43.09 | $\top_{d}\sqcup\top_{g}$
3 |  |  4  | 31015 | 70.55 |  | 293.59 | $\top$
3 |  |  5  | 122140 | 414.57 |  | 3003.56 | $\top$
3 |  |  10  | $-$ | timeout |  | $-$ | $-$

Figure 12: Experimental results for $\phi_{1L}$

#drones |  |  energy | #states | tgen | Lower approx. | Upper approx.
---|---|---|---|---|---|---
| tverif | output | tverif | output
1 |  |  1  | 5 | 0.008 | 0.03 | $\top_{g}$ | 0.02 | $\top_{g}$
1 |  |  2  | 14 | 0.006 | 0.05 | $\top_{d}\sqcup\top_{g}$ | 0.06 | $\top_{d}\sqcup\top_{g}$
1 |  |  3  | 32 | 0.01 | 0.14 | $\top_{d}\sqcup\top_{g}$ | 0.21 | $\top_{d}\sqcup\top_{g}$
1 |  |  4  | 61 | 0.02 | 0.22 | $\top$ | 0.28 | $\top$
1 |  |  5  | 106 | 0.03 | 0.39 | $\top$ | 0.48 | $\top$
1 |  |  10  | 601 | 0.27 | 2.12 | $\top$ | 2.38 | $\top$
1 |  |  100  | 16740 | 9.70 | 59.27 | $\top$ | 64.40 | $\top$
1 |  |  1000  | 178740 | 92.78 | 615.23 | $\top$ | 669.85 | $\top$
1 |  |  10000  | 1798740 | 890.85 | 6125.77 | $\top$ | 6054.80 | $\top$
1 |  |  12000  | 2158740 | 1122.84 | timeout | $-$ | timeout | $-$
2 |  |  1  | 17 | 0.01 | 0.18 | $\top_{g}$ | 0.10 | $\top_{g}$
2 |  |  2  | 98 | 0.06 | 0.66 | $\top_{d}\sqcup\top_{g}$ | 0.64 | $\top_{d}\sqcup\top_{g}$
2 |  |  3  | 422 | 0.33 | 2.63 | $\top_{d}\sqcup\top_{g}$ | 2.40 | $\top_{d}\sqcup\top_{g}$
2 |  |  4  | 1263 | 1.21 | 8.43 | $\top$ | 7.31 | $\top$
2 |  |  5  | 3288 | 3.53 | 19.08 | $\top$ | 18.19 | $\top$
2 |  |  10  | 55757 | 89.30 | 323.42 | $\top$ | 321.15 | $\top$
2 |  |  100  | $-$ | timeout | $-$ | $-$ | $-$ | $-$
3 |  |  1  | 65 | 0.05 | 0.47 | $\top_{g}$ | 0.52 | $\top_{g}$
3 |  |  2  | 794 | 0.95 | 5.71 | $\top_{d}\sqcup\top_{g}$ | 5.90 | $\top_{d}\sqcup\top_{g}$
3 |  |  3  | 6626 | 12.31 | 55.60 | $\top_{d}\sqcup\top_{g}$ | 50.19 | $\top_{d}\sqcup\top_{g}$
3 |  |  4  | 31015 | 78.63 | 271.55 | $\top$ | 239.28 | $\top$
3 |  |  5  | 122140 | 382.30 | 1719.81 | $\top$ | 932.31 | $\top$
3 |  |  10  | $-$ | timeout | $-$ | $-$ | $-$ | $-$

Figure 13: Experimental results for $\phi_{1R}$

energy |  | #states | tgen | Lower approx. | Upper approx.
---|---|---|---|---|---
| tverif | output | tverif | output
1  |  | 65 | 0.04 | 0.45 | $\bot$ | 0.46 | $\bot$
2  |  | 794 | 1.05 | 5.60 | $\top_{g}$ | 5.43 | $\top_{g}$
3  |  | 6626 | 12.05 | 62.64 | $\top_{g}$ | 45.45 | $\top_{g}$
4  |  | 31015 | 77.23 | 233.45 | $\top_{g}$ | 227.44 | $\top_{g}$
5  |  | 122140 | 379.29 | 951.14 | $\top_{g}$ | 854.41 | $\top_{g}$
6  |  | 349121 | 1276.82 | 2706.15 | $\top_{g}$ | 2423.55 | $\top_{g}$
7  |  | 880562 | 3446.30 | 6383.17 | $\top_{g}$ | 6052.17 | $\top_{g}$
8  |  | 1850861 | 9718.62 | timeout | $-$ | timeout | $-$

Figure 14: Experimental results: $\phi_{2R}^{loc}$ for $\\#drones=3$ and
$loc=7$

The experiments were conducted on an Intel Core i7-6700 CPU with dynamic clock
speed of 2.60–3.50 GHz, 32 GB RAM, running under 64bit Windows 10. The times
are given in seconds; the timeout was set to 2 hours. As the performance
results show, multi-valued verification of strategic ability scales up
similarly to two-valued model checking [63], which confirms the theoretical
results in Section 5.5.

The software used to conduct the experiments can be found at the address
https://github.com/blackbat13/stv. The software is implemented in Python 3. As
it is an on-going development, it does not accept any input language. Instead,
model generators are used. Models are generated as transition graphs and
stored explicitly in the memory.

As the experiments show, the result of the formula depends mostly on the
initial energy of the drones. If given enough energy, drones can visit every
place on the map, hence detecting any pollution. On the other hand, even a
drone with very small capacity of the battery can detect something. As can be
seen in Figures 12 and 14, for the cases in which initial energy of the drones
were less than 3, answer was more informative than simple false, as it would
have been if we had used two-valued logic. It shows that multi-valued logics
can provide the designer or analyst with much more useful information beyond a
simple yes/no answer.

##  9 Conclusions

In this paper we study a variant of alternating-time temporal logic, denoted
as mv-ATL${}^{*}_{\rightarrow}$, where the truth values are taken from an
arbitrary distributive lattice. We argue that multi-valued model checking of
mv-ATL${}^{*}_{\rightarrow}$ specifications can be useful, especially for
systems whose models cannot be fully analyzed due to their complexity and/or
inaccessibility of the relevant information. Other examples include systems
with information coming from multiple, potentially conflicting sources. We
propose the semantics of mv-ATL${}^{*}_{\rightarrow}$ first in the simplest
case of perfect information strategies and models with crisp, classical
transition functions. Then, we show how to extend the framework to the case of
multi-valued transitions, as well as other notions of strategies (in
particular, variants of strategic reasoning for agents with limited
observation capabilities).

In terms of technical results, we prove that our multi-valued semantics of mv-
ATL${}^{*}_{\rightarrow}$ provides a conservative extension of the classical
2-valued variant. More importantly, we propose efficient (i.e., polynomial-
time) translations from multi-valued model checking to the 2-valued case. We
formally characterize the conditions under which the translation can be
carried out by non-recursive one-to-many reduction, and propose a recursive
procedure for the remaining instances of the problem. The proposed techniques
are elegant enough to be directly applicable to other semantic variants of
strategic ability, for example, those referring to imperfect information
scenarios. This allows for non-classical model checking of abilities while
benefiting from the ongoing development of classical model checkers and game
solvers.

Finally, we back up our proposal by a series of experiments in a simulated
scenario of drones patrolling for pollution in a city. Besides promising
performance results, the experiments demonstrate also the use of the _relevant
implication_ , based on comparison of truth values, which is among the main
novel contributions of this paper. The operator can be used to provide a
multi-valued counterpart of material implication, with an intuitive and
appealing interpretation. This is especially important in multi-agent systems
where many relevant properties are indeed based on implication, which makes
them difficult to formalize in the multi-valued case.

In the future, we plan to extend the framework of mv-ATL${}^{*}_{\rightarrow}$
to richer specification languages, such as Strategy Logic [68, 69, 70]. We
would also like to take a closer look at multi-valued models arising from
state and action abstractions, and to the application of multi-valued model
checking to verification of strategic ability under imperfect information.

Acknowledgements. The authors thank Arthur Queffelec for his help in the
implementation of the model checking algorithm. Moreover, Wojciech Jamroga
acknowledges the support of the 7th Framework Programme of the European Union
under the Marie Curie IEF project ReVINK (PIEF-GA-2012-626398). Wojciech
Jamroga, Damian Kurpiewski, and Wojciech Penczek acknowledge the support of
the National Centre for Research and Development (NCBR), Poland, under the
PolLux projects VoteVerif (POLLUX-IV/1/2016) and STV (POLLUX-VII/1/2019).
Damian Kurpiewski and Wojciech Penczek acknowledge also the support of
CNRS/PAN under the project PARTIES.

## References

  * [1] Alur R, Henzinger TA, Kupferman O.  Alternating-Time Temporal Logic.  In: Proceedings of FOCS. IEEE Computer Society Press, 1997 pp. 100–109.
  * [2] Alur R, Henzinger TA, Kupferman O.  Alternating-Time Temporal Logic.  _Journal of the ACM_ , 2002.  49:672–713.  10.1145/585265.585270.
  * [3] Konikowska B, Penczek W.  Model Checking for Multi-Valued Computation Tree Logics.  In: Fitting M, Orłowska E (eds.), Beyond Two: Theory and Applications of Multiple Valued Logic, pp. 193–210. Physica-Verlag, 2003. doi:10.1007/978-3-7908-1769-0_8.