11institutetext: CRIL, Univ Artois and CNRS, Lens, France, 11email:
<EMAIL_ADDRESS>22institutetext: IRIT, CNRS, Toulouse University, France,
22email<EMAIL_ADDRESS>33institutetext: ENS Rennes, France, 33email:
<EMAIL_ADDRESS>
# Base-based Model Checking
for Multi-Agent Only Believing
(long version)††thanks: This work is partially supported by the project epiRL
(“Epistemic Reinforcement Learning”) ANR-22-CE23-0029, the project CoPains
(“Cognitive Planning in Persuasive Multimodal Communication”) ANR-18-CE33-0012
and the AI Chair project Responsible AI (ANR-19-CHIA-0008) both from the
French National Agency of Research. Support from the Natural Intelligence
Toulouse Institute (ANITI) is also gratefully acknowledged.

Tiago de Lima 11 Emiliano Lorini 22 François Schwarzentruber 33

###### Abstract

We present a novel semantics for the language of multi-agent only believing
exploiting belief bases, and show how to use it for automatically checking
formulas of this language and of its dynamic extension with private belief
expansion operators. We provide a PSPACE algorithm for model checking relying
on a reduction to QBF and alternative dedicated algorithm relying on the
exploration of the state space. We present an implementation of the QBF-based
algorithm and some experimental results on computation time in a concrete
example.

##  1 Introduction

Using belief bases for building a semantics for epistemic logic was initially
proposed by Lorini [17, 19]. In [18] it was shown that such a semantics allows
to represent the concept of universal epistemic model which is tightly
connected with the concept of universal type space studied by game theorists
[20]. A qualitative version of the universal type space with no probabilities
involved is defined by Fagin et al. [6] (see also [7]). Broadly speaking, a
universal epistemic model for a given situation is the most general model
which is compatible with that situation. It is the model which only contains
information about the situation and makes no further assumption. From an
epistemic point view, it can be seen as the model with maximal ignorance with
respect to the description of the situation at stake.

Such a universal epistemic model has been shown to be crucial for defining a
proper semantics for the concept of multi-agent only knowing (or believing)
[14, 12], as a generalization of the concept of single-agent only knowing (or
believing) [15].111As usual, the difference between knowledge and belief lies
in the fact that the former is always correct while the latter can be
incorrect. However, the construction of this semantics is far from being
straightforward. Halpern & Lakemeyer [13] use the proof-theoretic notion of
canonical model for defining it. The limitation of the canonical model is its
being infinite thereby not being exploitable in practice. In a more recent
work, Belle & Lakemeyer [2] provided an inductive proof-independent definition
of the semantics for multi-agent only knowing which departs from the standard
semantics of multi-agent epistemic logic based on multi-relational Kripke
structures. Finally, Aucher & Belle [1] have shown how to interpret the
language of multi-agent only knowing on standard Kripke structures. Although
being independent from the proof theory, these last two accounts are fairly
non-standard or quite involved. They rely either on an inductive definition
(Belle & Lakemeyer) or on a complex syntactic representation up to certain
modal depth (Aucher & Belle) of the multi-agent epistemic structure used for
interpreting the multi-agent only knowing language.

In this paper, we concentrate on the logic of multi-agent only believing based
on the logic K for beliefs. We show how to use the belief base semantics and
its construction of the universal model to automatically check formulas of the
corresponding language. The novel contribution of the paper is twofold:

  * •

Although the idea of using belief bases as a semantics for epistemic logic has
been proposed in previous work, this is the first attempt to use them in the
context of the logic of multi-agent only believing and of its extension with
private belief expansion operators.

  * •

Moreover, we are the first to provide a model checking algorithm for the logic
of multi-agent only believing, to implement it and to test it experimentally
on a concrete example. The belief base semantics helped us to accomplish this
task given its compactness and manageability.

##### Outline.

In Section 2, we first recall the belief base semantics introduced in our
previous work [17, 19]. We show how to interpret the language of multi-agent
only believing and how to define the universal model in it. In Section 3, we
introduce an example to illustrate the framework. In Section 4, we move to
model checking formulated in the belief base semantics. We provide a PSPACE
algorithm for model checking relying on a reduction to QBF. In Section 5, we
present an implementation of the QBF-based algorithm and some experimental
results on computation time in the example. In Section 6 we propose an
extension of the setting with private belief expansion operators, and
demonstrate that the model checking problem remains in PSPACE. Section 7
concludes.

##  2 Language and semantics

The multi-agent epistemic language introduced in [19] has two basic epistemic
modalities: one for explicit belief, and another one for implicit belief. An
agent’s explicit belief corresponds to a piece of information in the agent’s
belief base. An agent’s implicit belief corresponds to a piece of information
that is derivable from the agent’s explicit beliefs. In other words, if an
agent can derive $\varphi$ from its explicit beliefs, it implicitly believes
_at least_ that $\varphi$ is true. We consider the extension of this epistemic
language by complementary modalities for implicitly believing _at most_. The
_at least_ and _at most_ modalities can be combined to represent the concept
of _only_ believing.

The semantics over which the language is interpreted exploits belief bases.
Unlike the standard multi-relational Kripke semantics for epistemic logic in
which the agents’ epistemic accessibility relations over possible worlds are
given as primitive, in this semantics they are computed from the agents’
belief bases. Specifically, in this semantics it is assumed that at state $S$
an agent considers a state $S^{\prime}$ possible (or state $S^{\prime}$ is
epistemically accessible to the agent at state $S$) if and only if
$S^{\prime}$ satisfies all formulas included in the agent’s belief base at
$S$. This idea of computing the agents’ accessibility relations from the state
description is shared with the semantics of epistemic logic based on
interpreted systems [8, 16]. However, there is an important difference. While
the interpreted system semantics relies on the abstract notion of an agent’s
local state, in the belief base semantics an agent’s local state is identified
with its concrete belief base.

###  2.1 Semantics

Assume a countably infinite set of atomic propositions
$\mathit{Atm}=\\{p,q,\ldots\\}$ and a finite set of agents
$\textit{Agt}=\\{1,\ldots,n\\}$. We define the language $\mathcal{L}_{0}$ for
explicit belief by the following grammar in Backus-Naur Form (BNF):

$\mathcal{L}_{0}~{}\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}~{}\alpha::=p\mid\lnot\alpha\mid\alpha\land\alpha\mid\triangle_{i}\alpha,$

where $p$ ranges over $\mathit{Atm}$ and $i$ ranges over Agt.
$\mathcal{L}_{0}$ is the language used to represent explicit beliefs. The
formula $\triangle_{i}\alpha$ reads “agent $i$ has the explicit belief that
$\alpha$”. In our semantics, a state is not a primitive notion but it is
decomposed into different elements: one belief base per agent and an
interpretation of propositional atoms.

######  Definition 1 (State)

A state is a tuple
$S=\big{(}(\mathit{B}_{i})_{i\in\textit{Agt}},\mathit{V}\big{)}$ where
$\mathit{B}_{i}\subseteq\mathcal{L}_{0}$ is agent $i$’s belief base, and
$\mathit{V}\subseteq\mathit{Atm}$ is the actual environment. The set of all
states is noted $\mathbf{S}$.

The following definition specifies truth conditions for formulas in
$\mathcal{L}_{0}$.

######  Definition 2 (Satisfaction relation)

Let
$S=\big{(}(\mathit{B}_{i})_{i\in\mathit{Agt}},\mathit{V}\big{)}\in\mathbf{S}$.
Then,

$\displaystyle S\models p$ $\displaystyle\Longleftrightarrow$ $\displaystyle
p\in\mathit{V},$ $\displaystyle S\models\lnot\alpha$
$\displaystyle\Longleftrightarrow$ $\displaystyle S\not\models\alpha,$
$\displaystyle S\models\alpha_{1}\land\alpha_{2}$
$\displaystyle\Longleftrightarrow$ $\displaystyle S\models\alpha_{1}\text{ and
}S\models\alpha_{2},$ $\displaystyle S\models\triangle_{i}\alpha$
$\displaystyle\Longleftrightarrow$ $\displaystyle\alpha\in\mathit{B}_{i}.$

Observe in particular the set-theoretic interpretation of the explicit belief
operator in the previous definition: agent $i$ has the explicit belief that
$\alpha$ if and only if $\alpha$ is included in its belief base.

The following definition introduces the agents’ epistemic relations. They are
computed from the agents’ belief bases.

######  Definition 3 (Epistemic relation)

Let $i\in\mathit{Agt}$. Then, $\mathcal{R}_{i}$ is the binary relation on
$\mathbf{S}$ such that, for all
$S=\big{(}(\mathit{B}_{i})_{i\in\mathit{Agt}},\mathit{V}\big{)},S^{\prime}=\big{(}(\mathit{B}_{i}^{\prime})_{i\in\mathit{Agt}},\mathit{V}^{\prime}\big{)}\in\mathbf{S}$,
we have $S\mathcal{R}_{i}S^{\prime}\text{ if and only if
}\forall\alpha\in\mathit{B}_{i}:S^{\prime}\models\alpha$.

$S\mathcal{R}_{i}S^{\prime}$ means that $S^{\prime}$ is an epistemic
alternative for agent $i$ at $S$, that is to say, $S^{\prime}$ is a state that
at $S$ agent $i$ considers possible. The idea of the previous definition is
that $S^{\prime}$ is an epistemic alternative for agent $i$ at $S$ if and only
if, $S^{\prime}$ satisfies all facts that agent $i$ explicitly believes at
$S$.

The following definition introduces the concept of model, namely a state
supplemented with a set of states, called _context_. The latter includes all
states that are compatible with the agents’ common ground, i.e., the body of
information that the agents commonly believe to be the case [21].

######  Definition 4 (Model)

A model is a pair $(S,\mathit{Cxt})$ with $S\in\mathbf{S}$ and
$\mathit{Cxt}\subseteq\mathbf{S}$. The class of models is noted $\mathbf{M}$.

Note that in a model $(S,\mathit{Cxt})$, the state $S$ is not necessarily an
element of the context $\mathit{Cxt}$ due to the fact that we model belief
instead of knowledge. Therefore, the agents’ common ground represented by the
context $\mathit{Cxt}$ may be incorrect and not include the actual state. If
we modeled knowledge instead of belief, we would have to suppose that
$S\in\mathit{Cxt}$.

Let $\Gamma=(\Gamma_{i})_{i\in\mathit{Agt}}$ where, for every
$i\in\mathit{Agt}$, $\Gamma_{i}$ represents agent $i$’s vocabulary. A
$\Gamma$-universal model is a model containing all states at which an agent
$i$’s explicit beliefs are built from its vocabulary $\Gamma_{i}$. In other
words, an agent’s vocabulary plays a role analogous to that of the notion of
awareness in the formal semantics of awareness [9]. The notion of
$\Gamma$-universal model is defined as follows.

######  Definition 5 (Universal model)

The model $(S,\mathit{Cxt})$ in $\mathbf{M}$ is said to be $\Gamma$-universal
if $S\in\mathit{Cxt}=\mathbf{S}_{\Gamma}$, with
$\mathbf{S}_{\Gamma}=\Big{\\{}\big{(}(\mathit{B}_{i}^{\prime})_{i\in\textit{Agt}},\mathit{V}^{\prime}\big{)}\in\mathbf{S}\mid\forall
i\in\textit{Agt},\mathit{B}_{i}^{\prime}\subseteq\Gamma_{i}\Big{\\}}.$ The
class of $\Gamma$-universal models is noted
$\mathbf{M}_{\mathit{univ}}(\Gamma)$.

$\Gamma=(\Gamma_{i})_{i\in\mathit{Agt}}$ is also called agent vocabulary
profile. Clearly, when $\Gamma=\mathcal{L}_{0}^{n}$, we have
$\mathbf{S}_{\Gamma}=\mathbf{S}$. A model $(S,\mathbf{S})$ in
$\mathbf{M}_{\mathit{univ}}(\mathcal{L}_{0}^{n})$ is a model with maximal
ignorance: it only contains the information provided by the actual state $S$.
For simplicity, we write $\mathbf{M}_{\mathit{univ}}$ instead of
$\mathbf{M}_{\mathit{univ}}(\mathcal{L}_{0}^{n})$.

###  2.2 Language

In this section, we introduce a language for implicitly believing _at most_
and implicitly believing _at least_ on the top of the language
$\mathcal{L}_{0}$ defined above. It is noted $\mathcal{L}$ and defined by:

$\mathcal{L}~{}\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}~{}\varphi::=\alpha\mid\neg\varphi\mid\varphi\land\varphi\mid\Box_{i}\varphi\mid\Box_{i}^{\small\complement}\varphi,$

where $\alpha$ ranges over $\mathcal{L}_{0}$ and $i$ ranges over
$\mathit{Agt}$. The other Boolean constructions $\top$, $\bot$, $\lor$,
$\rightarrow$, $\oplus$, and $\leftrightarrow$ are defined from $\alpha$,
$\neg$ and $\land$ in the standard way.

The formula $\Box_{i}\varphi$ is read “agent $i$ _at least_ implicitly
believes that $\varphi$”, while $\Box_{i}^{\small\complement}\varphi$ is read
“agent $i$ _at most_ implicitly believes that $\neg\varphi$”. Alternative
readings of formulas $\Box_{i}\varphi$ and
$\Box_{i}^{\small\complement}\varphi$ are, respectively, “$\varphi$ is true at
all states that agent $i$ considers possible” and “$\varphi$ is true at all
states that agent $i$ does not consider possible”. The latter is in line with
the reading of the normal modality and the corresponding “window” modality in
the context of Boolean modal logics [10]. The duals of the operators
$\Box_{i}$ and $\Box_{i}^{\small\complement}$ are defined in the usual way, as
follows: $\Diamond_{i}\varphi~{}\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}~{}\neg\Box_{i}\neg\varphi$ and
$\Diamond_{i}^{\small\complement}\varphi~{}\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}~{}\lnot\Box_{i}^{\small\complement}\lnot\varphi$. Formulas in the
language $\mathcal{L}$ are interpreted relative to a model $(S,\mathit{Cxt})$.
(Boolean cases are omitted since they are defined as usual.)

######  Definition 6 (Satisfaction relation (cont.))

Let $(S,\mathit{Cxt})\in\mathbf{M}$. Then:

$\displaystyle(S,\mathit{Cxt})\models\alpha$
$\displaystyle\Longleftrightarrow$ $\displaystyle S\models\alpha,$
$\displaystyle(S,\mathit{Cxt})\models\Box_{i}\varphi$
$\displaystyle\Longleftrightarrow$ $\displaystyle\forall
S^{\prime}\in\mathit{Cxt}:\text{if }S\mathcal{R}_{i}S^{\prime}\text{then
}(S^{\prime},\mathit{Cxt})\models\varphi,$
$\displaystyle(S,\mathit{Cxt})\models\Box_{i}^{\small\complement}\varphi$
$\displaystyle\Longleftrightarrow$ $\displaystyle\forall
S^{\prime}\in\mathit{Cxt}:\text{if
}S\mathcal{R}_{i}^{\complement}S^{\prime}\text{then
}(S^{\prime},\mathit{Cxt})\models\varphi,$

with
$\mathcal{R}_{i}^{\complement}=(\mathbf{S}\times\mathbf{S})\setminus\mathcal{R}_{i}$.

Note that $S\mathcal{R}_{i}^{\complement}S^{\prime}$ just means that at state
$S$ agent $i$ does not consider state $S^{\prime}$ possible. Moreover,
interpretations of the two modalities $\Box_{i}$ and
$\Box_{i}^{\small\complement}$ are restricted to the actual context
$\mathit{Cxt}$. The only believing modality ($\Box_{i}^{o}$) is defined as
follows:

$\displaystyle\Box_{i}^{o}\varphi$
$\displaystyle~{}\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}~{}\Box_{i}\varphi\land\Box_{i}^{\small\complement}\lnot\varphi.$

Notions of satisfiability and validity of $\mathcal{L}$-formulas for the class
of models $\mathbf{M}$ are defined in the usual way: $\varphi$ is satisfiable
if there exists $(S,\mathit{Cxt})\in\mathbf{M}$ such that
$(S,\mathit{Cxt})\models\varphi$, and $\varphi$ is valid if $\lnot\varphi$ is
not satisfiable.

In [18, Theorem 26], it is shown that when restricting to the fragment of the
language $\mathcal{L}$ where formulas containing explicit beliefs are
disallowed (i.e., in the definition of $\mathcal{L}$ $\alpha$ is replaced by
$p$), the set of satisfiable formulas relative to the class
$\mathbf{M}_{\mathit{univ}}$ is the same as the set of satisfiable formulas
relative to the class of qualitative universal type spaces, as defined in [6].
The latter is similar to the class of $k$-structures, as defined by Belle &
Lakemeyer [2].222Although it has not been formally proven, we believe that
Belle & Lakemeyer’s semantics and Fagin et al.’s semantics are nothing but
different formulations of the same class of universal epistemic structures. In
Section 4, we will show that $\Gamma$-universal models of Definition 5 provide
an adequate and compact semantics for model checking formulas of the language
$\mathcal{L}$. But, before delving into model checking, we illustrate our
language with the help of an example.

##  3 Example

We give two variants of the example, the first focused on first-order beliefs
and the second focused on second-order beliefs.

###### Example 1

Agents in $\mathit{Agt}$ are members of a selection committee for an associate
professor position. They have to choose which candidates to admit to the
second round of selection consisting in an interview. Committee members and
candidates work in the same scientific community. Therefore, it is possible
that they co-authored some papers in the past. Assume there are $m$ candidates
$\mathit{Cand}=\\{c_{1},\ldots,c_{m}\\}$. In order to formalize the example we
use atomic propositions of the form $\mathsf{vote}(i{,}c)$, with
$i\in\mathit{Agt}$ and $c\in\mathit{Cand}$, standing for “agent $i$ votes for
candidate $c$”. The first two rules of the game state that each committee
member must vote for exactly one candidate (at least one candidate and no more
than one):

$\displaystyle\alpha_{1}~{}\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}~{}\bigwedge_{i\in\mathit{Agt}}\bigvee_{c\in\mathit{Cand}}\mathsf{vote}(i{,}c),$
$\displaystyle\alpha_{2}~{}\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}~{}\bigwedge_{i\in\mathit{Agt}}\bigwedge_{c,c^{\prime}\in\mathit{Cand},c\neq
c^{\prime}}\big{(}\mathsf{vote}(i{,}c)\rightarrow\neg\mathsf{vote}(i{,}c^{\prime})\big{)}.$

The third rule states that a member of the committee cannot vote for a
candidate with whom she/he co-authored an article in the past:

$\displaystyle\alpha_{3}~{}\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}~{}\bigwedge_{i\in\mathit{Agt}}\bigwedge_{c\in\mathbf{f}(i)}\neg\mathsf{vote}(i{,}c),$

where $\mathbf{f}:\mathit{Agt}\longrightarrow 2^{\mathit{Cand}}$ is a function
mapping each member of the committee to her/his co-authors. A candidate $c$ is
admitted to the interview if and only if at least one member of the committee
has voted for her/him. This is expressed by the following abbreviation:

$\displaystyle\mathsf{adm}(c)~{}\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}~{}\bigvee_{i\in\mathit{Agt}}\mathsf{vote}(i{,}c).$

Let us consider the variant of the example in which the evaluation committee
and the set of candidates have the same cardinality and a committee member co-
authored an article with only her/his matching candidate in the linear order.
That is, we suppose:

$\displaystyle|\mathit{Agt}|=|\mathit{Cand}|>2,\text{ and }$
$\displaystyle\forall i\in\mathit{Agt},\mathbf{f}(i)=\\{c_{i}\\}.$

Furthermore, we suppose that (i) each committee member except the last one
votes for her/his next candidate in the linear order, while the last committee
member $n$ votes for her/his previous candidate $n-1$; (ii) the vote by a
committee member is secret (i.e., a committee member only has epistemic access
to her/his vote), (iii) all committee members know the results of the
selection, namely, which candidates are admitted to the interview and which
are not. The three hypotheses (i), (ii) and (iii) are fully expressed by the
state $S_{0}=\big{(}(\mathit{B}_{i})_{i\in\mathit{Agt}},\mathit{V}\big{)}$
such that, for every $1\leq i<n$,

$\displaystyle\mathit{B}_{i}=$
$\displaystyle\big{\\{}\mathsf{vote}(i{,}c_{i+1}),\neg\mathsf{adm}(c_{1}),\mathsf{adm}(c_{2}),\ldots,\mathsf{adm}(c_{n}),\alpha_{1},\alpha_{2},\alpha_{3}\big{\\}},$

and moreover,

$\displaystyle\mathit{B}_{n}=$
$\displaystyle\big{\\{}\mathsf{vote}(n{,}c_{n-1}),\neg\mathsf{adm}(c_{1}),\mathsf{adm}(c_{2}),\ldots,\mathsf{adm}(c_{n}),\alpha_{1},\alpha_{2},\alpha_{3}\big{\\}},$
$\displaystyle\mathit{V}=$
$\displaystyle\big{\\{}\mathsf{vote}(1{,}c_{2}),\ldots,\mathsf{vote}(n-1{,}c_{n}),\mathsf{vote}(n{,}c_{n-1})\big{\\}}.$

The following holds when $|\mathit{Agt}|=|\mathit{Cand}|=3$:

$(S_{0},\mathbf{S}_{\Gamma})\models\varphi_{0},$

with

$\displaystyle\varphi_{0}~{}\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}~{}$
$\displaystyle\Box_{1}^{o}\psi_{1}\land\bigwedge_{i\in\\{2,3\\}}\Box_{i}^{o}\psi_{2},$
$\displaystyle\psi_{1}~{}\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}~{}$ $\displaystyle\begin{aligned}
&\mathsf{vote}(1{,}c_{2})\land\neg\mathsf{vote}(1{,}c_{1})\land\neg\mathsf{vote}(1{,}c_{3})\\\
&\land\mathsf{vote}(2{,}c_{3})\land\neg\mathsf{vote}(2{,}c_{1})\land\neg\mathsf{vote}(2{,}c_{2})\\\
&\land\mathsf{vote}(3{,}c_{2})\land\neg\mathsf{vote}(3{,}c_{1})\land\neg\mathsf{vote}(3{,}c_{3}),\end{aligned}$
$\displaystyle\psi_{2}~{}\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}~{}$ $\displaystyle\begin{aligned}
&\neg\mathsf{vote}(1{,}c_{1})\land(\mathsf{vote}(1{,}c_{2})\oplus\mathsf{vote}(1{,}c_{3}))\\\
&\land\mathsf{vote}(2{,}c_{3})\land\neg\mathsf{vote}(2{,}c_{1})\land\neg\mathsf{vote}(2{,}c_{2})\\\
&\land\mathsf{vote}(3{,}c_{2})\land\neg\mathsf{vote}(3{,}c_{1})\land\neg\mathsf{vote}(3{,}c_{3}).\end{aligned}$

and $\Gamma_{i}=\mathit{B}_{i}\cup\neg\mathit{B}_{i}$ for every
$i\in\mathit{Agt}$, (where $\neg\mathit{B}_{i}$ is the set of negations of the
formulas in $\mathit{B}_{i}$). $(S_{0},\mathbf{S}_{\Gamma})$ so defined is
nothing but a $\Gamma$-universal model in which the agents’ vocabularies
include all and only those formulas in their actual belief bases and their
negations.

This means that, in the three-agent case, agent $1$ only knows for whom an
agent voted and for whom she/he did not vote, while agent $2$ and agent $3$
only know for whom they voted and for whom they did not vote, and that agent
$1$ voted either for $2$ or for $3$. Therefore, $2$ and $3$ do not know for
whom $1$ voted. Interestingly, when $|\mathit{Agt}|=|\mathit{Cand}|>3$:

$\displaystyle(S_{0},\mathbf{S}_{\Gamma})\not\models\varphi_{0}.$

###### Example 2

It is worth to consider a variant of Example 1 in which agent $1$ has higher-
order explicit beliefs (i.e., explicit beliefs about other agents’ explicit
beliefs). Specifically, we consider a state
$S_{0}^{\prime}=\big{(}(\mathit{B}_{i}^{\prime})_{i\in\mathit{Agt}},\mathit{V}^{\prime}\big{)}$
such that,

$\displaystyle\mathit{B}^{\prime}_{1}=$
$\displaystyle\mathit{B}_{1}\cup\\{\triangle_{2}\lnot\mathsf{adm}(c_{1}),\triangle_{2}\mathsf{adm}(c_{2}),\ldots,\triangle_{2}\mathsf{adm}(c_{n}),\triangle_{2}\alpha_{1},\triangle_{2}\alpha_{2},\triangle_{2}\alpha_{3}\\}$
and, for every $1<i\leq n$: $\displaystyle\mathit{B}_{i}^{\prime}=$
$\displaystyle\mathit{B}_{i},$ $\displaystyle\mathit{V}^{\prime}=$
$\displaystyle\mathit{V},$

where $\mathit{B}_{i}$ and $\mathit{V}$ are defined as above. In other words,
committee member $1$ explicitly knows that committee member $2$ explicitly
knows the rules of the game as well as the results of the selection.

Interestingly, when $|\mathit{Agt}|=|\mathit{Cand}|=3$, the following holds:

$(S^{\prime}_{0},\mathbf{S})\models\Box_{2}^{o}\psi_{2}\land\Box_{1}\Box_{2}\psi_{2}\land\lnot\Box_{1}\Box_{2}^{o}\psi_{2}.$

In words, in the three-agent case, at $S_{0}^{\prime}$, committee member $2$
only knows that $\psi_{2}$, committee member $1$ knows that $2$ knows
$\psi_{2}$, but $1$ does not know that $2$ only knows that $\psi_{2}$.

##  4 Model checking

The model checking problem is defined in our framework as follows:

input:

an agent vocabulary profile $\Gamma=(\Gamma_{i})_{i\in\mathit{Agt}}$ with
$\Gamma_{i}$ finite for every $i\in\mathit{Agt}$, a finite state $S_{0}$ in
$\mathbf{S}_{\Gamma}$, and a formula $\varphi_{0}\in\mathcal{L}$;

output:

yes if $(S_{0},\mathbf{S}_{\Gamma})\models\varphi_{0}$; no otherwise.

###### Remark 1

We suppose w.l.o.g. that outer most subformulas of $\varphi_{0}$ of the form
$\triangle_{i}\alpha$ are such that $\alpha\in\Gamma_{i}$. If this is not the
case for some subformulas $\triangle_{i}\alpha$, then the subformula
$\triangle_{i}\alpha$ will be false anyway and can be replaced by $\bot$.

####  4.0.1 Direct PSPACE algorithm

Figure 1 shows an algorithm $mc(S,\Gamma,\varphi)$ that checks whether
$(S,\mathbf{S}_{\Gamma})\models\varphi$. Note that $\mathbf{S}_{\Gamma}$ is
not computed explicitly, but implicitly represented by $\Gamma$. In the
algorithm, states $S$ are represented as vectors of bits indicating for all
$i$, for each element $\alpha$ of $\Gamma_{i}$ whether $\alpha$ belongs to
$i$’s base in $S$ or not. It also encodes the valuation over atomic
propositions appearing in $\Gamma$ and $\varphi_{0}$. The states $S$
manipulated by the algorithm are of size polynomial in the size of the input.
The loop for all $S^{\prime}\in\mathbf{S}_{0}$ such that
$S\mathcal{R}_{i}S^{\prime}$ works as follows. We consider all the vectors
$S^{\prime}$. Each such vector $S^{\prime}$ represents a state in
$\mathbf{S}_{\Gamma}$. For each $S^{\prime}$ we check in polynomial time
whether $S\mathcal{R}_{i}S^{\prime}$.

function $mc(S,\Gamma,\varphi)$ match $\varphi$ do
case $p$: return $p\in\mathit{V}$ case $\triangle_{i}\alpha$: return
$\alpha\in\mathit{B}_{i}$ case $\lnot\psi$: return not $mc(S,\Gamma,\psi)$
case $\psi_{1}\land\psi_{2}$: return $mc(S,\Gamma,\psi_{1})$ and
$mc(S,\Gamma,\psi_{2})$ case $\Box_{i}\psi$: for all
$S^{\prime}\in\mathbf{S}_{\Gamma}$ such that $S\mathcal{R}_{i}S^{\prime}$ do
if not $mc(S^{\prime},\Gamma,\psi)$ return false return true case
$\Box_{i}^{\small\complement}\psi$: for all $S^{\prime}\in\mathbf{S}_{\Gamma}$
such that $S\mathcal{R}_{i}^{\complement}S^{\prime}$ do
if not $mc(S^{\prime},\Gamma,\psi)$ return false return true

Figure 1: Generic algorithm for model checking $\mathcal{L}$-formulas.

####  4.0.2 Reduction to TQBF

We propose a reduction to TQBF (true quantified binary formulas). We introduce
TQBF propositional variables $x_{\alpha,k}$ for all $\alpha\in\mathcal{L}_{0}$
and for all integers $k$. The variables indexed by $k$ are said to be of level
$k$. They correspond to the recursive nesting in the procedure $mc$ described
in Figure 1 for the cases $\Box_{i}\varphi$ and
$\Box_{i}^{\small\complement}\varphi$. For instance, $x_{\alpha,k}$ is true if
$\alpha$ is true at some state at depth $k$. Let $X_{k}$ be the set of
formulas of level $k$. More precisely, $X_{k}$ contains exactly formulas
$x_{\triangle_{i}\alpha,k}$ with $\alpha\in\Gamma_{i}$ for any agent $i$, and
$x_{p,k}$ with $p$ appearing in $\Gamma$ or $\varphi_{0}$.

###### Definition 7

We define the function $tr$ that maps any formula of $\mathcal{L}$ to a QBF-
formula by $tr(\varphi_{0}):=tr_{0}(\varphi_{0})$ with:

  * •

$tr_{k}(p)=x_{p,k}$

  * •

$tr_{k}(\lnot\varphi)=\lnot tr_{k}(\varphi)$

  * •

$tr_{k}(\varphi\land\psi)=tr_{k}(\varphi)\land tr_{k}(\psi)$

  * •

$tr_{k}(\triangle_{i}\alpha)=x_{\triangle_{i}\alpha,k}$

  * •

$tr_{k}(\Box_{i}\varphi)=\forall X_{k+1}(R_{i,k}\rightarrow
tr_{k+1}(\varphi))$

  * •

$tr_{k}(\Box_{i}^{\small\complement}\varphi)=\forall X_{k+1}(\lnot
R_{i,k}\rightarrow tr_{k+1}(\varphi))$

where:

$R_{i,k}:=\bigwedge_{\alpha\in\Gamma_{i}}x_{\triangle_{i}\alpha,k}\rightarrow
tr_{k+1}(\alpha).$

The translation $tr_{k}(\Box_{i}\varphi)$ corresponds to case
$\Box_{i}\varphi$ in the algorithm. State $S$ (resp. $S^{\prime}$) is
represented by the truth values of variables in $X_{k}$ (resp. $X_{k+1}$).
Formula $R_{i,k}$ reformulates $S\mathcal{R}_{i}S^{\prime}$.

###### Proposition 1

Let $\varphi_{0}\in\mathcal{L}$ and $S_{0}=((B_{i})_{i\in\mathit{Agt}},V)$.
The following two statements are equivalent:

  * •

$(S_{0},\mathbf{S}_{\Gamma})\models\varphi_{0}$

  * •

$\exists X_{0}(\operatorname{desc}_{S_{0}}(X_{0})\land tr_{0}(\varphi_{0}))$
is QBF-true,

where:

$\operatorname{desc}_{S_{0}}(X_{0}):=\bigwedge_{i\in\mathit{Agt}}\left(\bigwedge_{\alpha\in
B_{i}}x_{\triangle_{i}\alpha,0}\land\bigwedge_{\alpha\in\Gamma_{i}\setminus
B_{i}}\lnot x_{\triangle_{i}\alpha,0}\right)\land\bigwedge_{p\in
V}x_{p,0}\land\bigwedge_{p\not\in V}\lnot x_{p,0}.$

###### Proof

Let $\operatorname{val}_{S}(X_{k})$ represent the unique valuation on $X_{k}$
satisfying $\operatorname{desc}_{S}(X_{k})$. We prove by induction on the
structure of $\varphi$ that $(S,\mathbf{S}_{\Gamma})\models\varphi\text{ iff
}\operatorname{val}_{S}(X_{k})\models tr_{k}(\varphi)$, for all $k$.

Induction base. Let $\varphi=p$, for some $p\in\mathit{Atm}$. We have
$(S,\mathbf{S}_{\Gamma})\models p$ iff $p\in V$ iff
$x_{k,p}\in\operatorname{val}_{S}(X_{k})$ iff
$\operatorname{val}_{S}(X_{k})\models tr_{k}(p)$.

Induction step. The cases for operators $\lnot$ and $\land$ are
straightforward. We proceed with the modal operators in the language:

  * •

Let $\varphi=\triangle_{i}\alpha$. We have:
$(S,\mathbf{S}_{\Gamma})\models\triangle_{i}\alpha$ iff $\alpha\in B_{i}$ iff
$x_{k,\triangle_{i}\alpha}\in\operatorname{val}_{S}(X_{k})$ iff
$\operatorname{val}_{S}(X_{k})\models tr_{k}(\triangle_{i}\alpha)$.

  * •

Let $\varphi=\Box_{i}\psi$. We denote by
$\operatorname{val}_{S}(X_{k})+\operatorname{val}_{S^{\prime}}(X_{k+1})$ the
valuation obtained by concatenating the valuation
$\operatorname{val}_{S}(X_{k})$ and $\operatorname{val}_{S^{\prime}}(X_{k+1})$
(we take the truth values of propositions in $X_{k}$ from the former and the
truth values of propositions in $X_{k+1}$ from the latter). We have:

$\displaystyle(S,\mathbf{S}_{\Gamma})\models\Box_{i}\psi$
$\displaystyle\iff\text{ for all $S^{\prime}\in\mathbf{S}_{\Gamma}$,
$S\mathcal{R}_{i}S^{\prime}$ implies
}(S^{\prime},\mathbf{S}_{\Gamma})\models\psi$ $\displaystyle\iff\text{ for all
$S^{\prime}\in\mathbf{S}_{\Gamma}$, $S\mathcal{R}_{i}S^{\prime}$ implies
}\operatorname{val}_{S^{\prime}}(X_{k+1})\models tr_{k+1}(\psi)$
$\displaystyle\iff\text{ for all
$S^{\prime}\in\mathbf{S}_{\Gamma}$}\operatorname{val}_{S}(X_{k})+\operatorname{val}_{S^{\prime}}(X_{k+1})\models
R_{i,k}\rightarrow tr_{k+1}(\psi)$
$\displaystyle\iff\operatorname{val}_{S}(X_{k})\models\forall
X_{k+1},R_{i,k}\rightarrow tr_{k+1}(\psi)$
$\displaystyle\iff\operatorname{val}_{S}(X_{k})\models tr_{k}(\Box_{i}\alpha)$

  * •

Let $\varphi=\Box_{i}^{\small\complement}\varphi$. The proof is analogous to
that for operator $\Box_{i}$ above. In particular, we use relation
$\mathcal{R}_{i}^{\complement}$ and formula $\lnot R_{i,k}$.

Therefore, $(S_{0},\mathbf{S}_{\Gamma})\models\varphi_{0}$ iff
$\operatorname{val}_{S_{0}}(X_{0})\models tr_{0}(\varphi)$. In addition,
$\operatorname{val}_{S_{0}}(X_{0})\models tr_{0}(\varphi)$ is equivalent to
$\exists X_{0}(\operatorname{desc}_{S_{0}}(X_{0})\land tr_{0}(\varphi_{0}))$
is QBF-true. This concludes the proof.∎

In [18], it is proved that the previous model checking problem formulated in
the belief base semantics is PSPACE-hard, already for the fragment of
$\mathcal{L}$ with only “at least” implicit belief operators, but with no “at
most” implicit belief operators involved. Thus, the fact that the generic
model checking problem given in Figure 1 runs in polynomial space as well as
Proposition 1 allow us to state the following complexity result.

###### Theorem 4.1

Model checking $\mathcal{L}$-formulas is PSPACE-complete.

##  5 Implementation and experimental results

We implemented a symbolic model checker,333Available at
https://src.koda.cnrs.fr/tiago.de.lima/lda/ which uses the translation to
TQBF. The resulting TQBF is then translated into a binary decision diagram
(BDD), in the same way as done in [3]. The program is implemented in Haskell
and the BDD library used is HasCacBDD [11]. It was compiled with GHC 9.2.7 in
a MacBook Air with a 1.6 GHz Dual-Core Intel Core i5 processor and 16 GB of
RAM, running macOS Ventura 13.3.1.

$cands=voters=|\mathit{Agt}|$ | $3$ | $4$ | $5$ | $6$ | $7$ | $8$ | $9$ | $10$
---|---|---|---|---|---|---|---|---
$|\mathit{Atm}|$ | $9$ | $16$ | $25$ | $36$ | $49$ | $64$ | $81$ | $100$
$ratoms$ | $100$ | $164$ | $244$ | $340$ | $452$ | $580$ | $724$ | $884$
$states$ | $2^{309}$ | $2^{672}$ | $2^{1245}$ | $2^{2076}$ | $2^{3213}$ | $2^{4704}$ | $2^{6597}$ | $2^{8940}$
Execution time (sec.) | $0.076$ | $0.015$ | $0.026$ | $0.047$ | $0.066$ | $0.101$ | $0.157$ | $0.248$

$cands=voters=|\mathit{Agt}|$ | $3$ | $4$ | $5$ | $6$ | $7$ | $8$ | $9$ | $10$
---|---|---|---|---|---|---|---|---
$|\mathit{Atm}|$ | $9$ | $16$ | $25$ | $36$ | $49$ | $64$ | $81$ | $100$
$ratoms$ | $133$ | $210$ | $305$ | $418$ | $549$ | $698$ | $865$ | $1050$
$states$ | $2^{408}$ | $2^{856}$ | $2^{1550}$ | $2^{2544}$ | $2^{3892}$ | $2^{5648}$ | $2^{7866}$ | $2^{10600}$
Execution time (sec.) | $0.081$ | $0.063$ | $0.334$ | $3.066$ | $17.588$ | $90.809$ | KO | KO

Table 1: Symbolic model checker performance on Examples 1 (above) and 2
(below).

Table 1 shows the performance of the model checker on the examples of Section
3. It shows execution times for different instances. For both examples, the
size of the model ($states$) is given by the number of possible valuations
times the number of possible multi-agent belief bases:
$2^{|\mathit{Atm}|}\times(2^{ratoms})^{|\mathit{Agt}|}$. The value of $ratoms$
is the number of “relevant atoms”. There is one such atom for each formula in
$\Gamma$, each propositional variable appearing in $\Gamma$ and in the input
formula, each formula $\alpha$ that is a sub-formula of the input formula,
plus one atom for each formula $\triangle_{i}\alpha$ such that
$\alpha\in\Gamma$. The number of states gives an idea of the size of the
search space for modal formulas. In principle, to check a formula of the form
$\Box^{o}\varphi$, one must check $\varphi$ in every state of the model.
Because of that, a naive implementation cannot be used. Indeed, in our tests
with such a solution, no instance could be solved under the timeout of 10
minutes.

One can notice that the model checker is slower in the case of $3$ candidates
than in the case of $4$ candidates (and in Example 1 the latter is true even
up to $7$ candidates). The reason is that the input formula is true for $3$
candidates, whereas it is false on all the other cases. Checking that a box
formula is false is easier, because the checker needs to find only one state
where the formula in the scope of the box operator is false. Also note that
instances of Example 1 are solved much faster than those of Example 2. This is
due to two factors. First, Example 2 has larger belief bases, which imply a
larger number of states. Second, the input formula of the second example has a
larger modal depth, which obliges the checker to generate a larger search
tree.

##  6 Dynamic extension

In this section, we present a simple extension of the language $\mathcal{L}$
by dynamic operators for modeling the agents’ belief dynamics of private type.
Similar operators were introduced in [19]. The novel result of this section is
to show that adding them to the language $\mathcal{L}$ does not increase
complexity of the model checking problem. More generally, we provide a simple
dynamic extension of the static language of implicitly believing _at least_
and implicitly believing _at most_ whose model checking problem remains in
PSPACE.

The extended language is noted $\mathcal{L}^{+}$ and is defined by the
following grammar:

$\mathcal{L}^{+}~{}\stackrel{{\scriptstyle\mbox{\scriptsize def}}}{{=}}~{}$ | $\varphi$ | $::=$ | $\alpha\mid\neg\varphi\mid\varphi\wedge\varphi\mid\Box_{i}\varphi\mid\Box_{i}^{\small\complement}\varphi\mid[+_{i}\alpha]\varphi,$
---|---|---|---

where $\alpha$ ranges over $\mathcal{L}_{0}$ and $i$ ranges over
$\mathit{Agt}$.

Events of type $+_{i}\alpha$ are called informative events. In particular,
$+_{i}\alpha$ is the event of agent $i$ privately expanding its belief base
with $\alpha$.

The formula $[+_{i}\alpha]\varphi$ is read “$\varphi$ holds after the
informative event $+_{i}\alpha$ has occurred”. It has the following semantic
interpretation relative to a model.

######  Definition 8 (Satisfaction relation, cont.)

Let $S=(\mathit{B}_{1},\ldots,\mathit{B}_{n},\mathit{V})\in\mathbf{S}$ and let
$(S,\mathit{Cxt})\in\mathbf{M}$. Then:

$\displaystyle(S,\mathit{Cxt})\models[+_{i}\alpha]\varphi$
$\displaystyle\Longleftrightarrow$
$\displaystyle(S^{+_{i}\alpha},\mathit{Cxt})\models\varphi,$

where $\mathit{B}_{i}^{+_{i}\alpha}=\mathit{B}_{i}\cup\\{\alpha\\}\text{ and
}\mathit{B}_{j}^{+_{i}\alpha}=\mathit{B}_{j}\text{ for all }j\neq i$.

Intuitively speaking, the private belief expansion of $i$’s belief base by
$\alpha$ simply consists in agent $i$ adding the information that $\alpha$ to
its belief base, while all other agents keep their belief bases unchanged. Let
us go back to the Example 1 we introduced in Section 3 to illustrate the
expressiveness of our dynamic extension.

###### Example 3

It is worth noting that private belief dynamics allow agents to gather new
information and to gain new knowledge. Suppose in the three-agent variant of
the example agent $2$ and agent $3$ privately learn that $1$ voted for $2$.
This ensures that there is no longer any information asymmetry between agent
$1$ and agents $2$ and $3$. Formally, we have

$(S_{0},\mathbf{S}_{\Gamma})\models\big{[}+_{2}\mathsf{vote}(1{,}2)\big{]}\big{[}+_{3}\mathsf{vote}(1{,}2)\big{]}\chi_{0},$

where

$\displaystyle\chi_{0}~{}\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}~{}$
$\displaystyle\bigwedge_{i\in\\{1,2,3\\}}\Box_{i}^{o}\psi_{1},$

and $\psi_{1}$, $S_{0}$, $\mathbf{S}_{\Gamma}$ are defined as in Example 1 in
Section 3. This means that, in the three-agent variant of the example, after
agent $2$ and agent $3$ privately learn that agent $1$ voted for $2$,
everybody only knows for whom an agent voted and for whom she/he did not vote.

As the following proposition highlights, we have reduction principles for the
dynamic operators.

###### Proposition 2

The following equivalences are valid for the class $\mathbf{M}$:

$\displaystyle[+_{i}\alpha]p\leftrightarrow p$
$\displaystyle[+_{i}\alpha]\neg\varphi\leftrightarrow\neg[+_{i}\alpha]\varphi$
$\displaystyle[+_{i}\alpha](\varphi_{1}\wedge\varphi_{2})\leftrightarrow\big{(}[+_{i}\alpha]\varphi_{1}\wedge[+_{i}\alpha]\varphi_{2}\big{)}$
$\displaystyle[+_{i}\alpha]\triangle_{j}\beta\leftrightarrow\triangle_{j}\beta\text{
if }i\neq j\text{ or }\alpha\neq\beta$
$\displaystyle[+_{i}\alpha]\triangle_{i}\alpha\leftrightarrow\top$
$\displaystyle[+_{i}\alpha]\Box_{j}\varphi\leftrightarrow\Box_{j}\varphi\text{
if }i\neq j$
$\displaystyle[+_{i}\alpha]\Box_{i}\varphi\leftrightarrow\Box_{i}(\alpha\rightarrow\varphi)$
$\displaystyle[+_{i}\alpha]\Box_{j}^{\small\complement}\varphi\leftrightarrow\Box_{j}^{\small\complement}\varphi\text{
if }i\neq j$
$\displaystyle[+_{i}\alpha]\Box_{i}^{\small\complement}\varphi\leftrightarrow\big{(}\Box_{i}(\neg\alpha\rightarrow\varphi)\wedge\Box_{i}^{\small\complement}\varphi\big{)}$

###### Proof

We only prove cases $\Box_{i}\varphi$ and
$\Box_{i}^{\small\complement}\varphi$, since other cases are straightforward.

$\displaystyle(S,\mathit{Cxt})\models[+_{i}\alpha]\Box_{i}\varphi$
$\displaystyle\Longleftrightarrow$
$\displaystyle(S^{+_{i}\alpha},\mathit{Cxt})\models\Box_{i}\varphi,$
$\displaystyle\Longleftrightarrow$ $\displaystyle\forall
S^{\prime}\in\mathit{Cxt}:\text{if
}S^{+_{i}\alpha}\mathcal{R}_{i}S^{\prime}\text{ then
}(S^{\prime},\mathit{Cxt})\models\varphi,$ $\displaystyle\Longleftrightarrow$
$\displaystyle\forall S^{\prime}\in\mathit{Cxt}:\text{if
}S\mathcal{R}_{i}S^{\prime}\text{ and }S^{\prime}\models\alpha\text{ then
}(S^{\prime},\mathit{Cxt})\models\varphi,$ $\displaystyle\Longleftrightarrow$
$\displaystyle(S,\mathit{Cxt})\models\Box_{i}(\alpha\rightarrow\varphi).$
$\displaystyle(S,\mathit{Cxt})\models[+_{i}\alpha]\Box_{i}^{\small\complement}\varphi$
$\displaystyle\Longleftrightarrow$
$\displaystyle(S^{+_{i}\alpha},\mathit{Cxt})\models\Box_{i}^{\small\complement}\varphi,$
$\displaystyle\Longleftrightarrow$ $\displaystyle\forall
S^{\prime}\in\mathit{Cxt}:\text{if
}S^{+_{i}\alpha}\mathcal{R}_{i}^{\complement}S^{\prime}\text{ then
}(S^{\prime},\mathit{Cxt})\models\varphi,$ $\displaystyle\Longleftrightarrow$
$\displaystyle\forall S^{\prime}\in\mathit{Cxt}:\text{if
}S\mathcal{R}_{i}^{\complement}S^{\prime}\text{ or
}(S\mathcal{R}_{i}S^{\prime}\text{ and }S^{\prime}\models\neg\alpha)\text{
then }$ $\displaystyle(S^{\prime},\mathit{Cxt})\models\varphi,$
$\displaystyle\Longleftrightarrow$
$\displaystyle(S,\mathit{Cxt})\models\Box_{i}(\neg\alpha\rightarrow\varphi)\wedge\Box_{i}^{\small\complement}\varphi.\
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \squareforqed$

Model checking for formulas in the language $\mathcal{L}^{+}$ is analogous to
model checking for formulas in $\mathcal{L}$ we defined in Section 4. The
valid equivalences in Proposition 2 could be used to find a procedure for
reducing model checking for formulas in $\mathcal{L}^{+}$ to model checking
for formulas in $\mathcal{L}$. The problem is that such reduction is
exponential due to the fact that every time we find a formula of type
$[+_{i}\alpha]\Box_{i}^{\small\complement}\varphi$ we have to duplicate it
into two parts $\Box_{i}(\neg\alpha\rightarrow\varphi)$ and
$\Box_{i}^{\small\complement}\varphi$.

Fortunately we can easily adapt the generic algorithm presented in Section 4
in order to obtain a PSPACE procedure for model checking formulas of the
language $\mathcal{L}^{+}$. It is sufficient to add the following case for the
dynamic operators to the main routine of the algorithm in Figure 1:

$\displaystyle\mathbf{case}\ [+_{i}\alpha]\psi:\mathbf{return}\
mc(S^{+_{i}\alpha},\Gamma,\psi)$

The resulting algorithm clearly runs in polynomial space. Thus, we can
generalize the complexity result given in Theorem 4.1 to the language
$\mathcal{L}^{+}$.

###### Theorem 6.1

Model checking $\mathcal{L}^{+}$-formulas is PSPACE-complete.

##  7 Conclusion

This paper describes optimal procedures for model checking multi-agent only
believing formulas. As far as we know, we are the first to tackle the problem
of automating model checking for the logic of multi-agent only believing or
knowing. We implemented these procedures and presented some experimental
results on computation time. Moreover, we extended the formalism with private
belief expansion operators and showed that model checking remains PSPACE-
complete. In the future, we plan to implement the dynamic extension presented
in Section 6 and to extend the setting to introspective agents whose logic of
belief (resp. knowledge) is K45 (resp. S5). Last but not least, we intend to
apply our semantics for multi-agent only believing and model checking approach
to epistemic planning. We believe that the compactness of our semantics can
offer an advantage in terms of ease of implementation compared to the multi-
relational Kripke semantics traditionally used in the context of epistemic
planning [4, 5].

## References

  * [1] Aucher, G., Belle, V.: Multi-agent only knowing on planet kripke. In: Yang, Q., Wooldridge, M.J. (eds.) Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015. pp. 2713–2719. AAAI Press (2015), http://ijcai.org/Abstract/15/384
  * [2] Belle, V., Lakemeyer, G.: Multi-agent only-knowing revisited. In: Lin, F., Sattler, U., Truszczynski, M. (eds.) Principles of Knowledge Representation and Reasoning: Proceedings of the Twelfth International Conference, KR 2010, Toronto, Ontario, Canada, May 9-13, 2010. AAAI Press (2010), http://aaai.org/ocs/index.php/KR/KR2010/paper/view/1361
  * [3] van Benthem, J., van Eijck, J., Gattinger, M., Su, K.: Symbolic model checking for dynamic epistemic logic - S5 and beyond. Journal of Logic and Computation 28(2), 367–402 (2018)
  * [4] Bolander, T., Andersen, M.B.: Epistemic planning for single- and multi-agent systems. Journal of Applied Non-Classical Logics 21(1), 656–680 (2011)
  * [5] Bolander, T., Jensen, M.H., Schwarzentruber, F.: Complexity results in epistemic planning. In: Yang, Q., Wooldridge, M.J. (eds.) Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015. pp. 2791–2797. AAAI Press (2015), http://ijcai.org/Abstract/15/395
  * [6] Fagin, R., , Halpern, J.Y., , Vardi, M.Y.: A model-theoretic analysis of knowledge. Journal of the ACM 38(2), 382–428 (1991). https://doi.org/10.1145/103516.128680
  * [7] Fagin, R., Geanakoplos, J., Halpern, J.Y., , Vardi, M.Y.: The hierarchical approach to modeling knowledge and common knowledge. International Journal of Game Theory 28(3), 331–365 (1999)
  * [8] Fagin, R., Halpern, J., Moses, Y., Vardi, M.: Reasoning about Knowledge. MIT Press, Cambridge (1995)
  * [9] Fagin, R., Halpern, J.Y.: Belief, awareness, and limited reasoning. Artificial Intelligence 34(1), 39–76 (1987)
  * [10] Gargov, G., Passy, S.: A note on boolean modal logic. In: Petkov, P.P. (ed.) Mathematical Logic, pp. 299–309. Springer, Boston, MA (1990). https://doi.org/10.1007/978-1-4613-0609-2_21, https://doi.org/10.1007/978-1-4613-0609-2_21
  * [11] Gattinger, M.: HasCacBDD (2023), https://github.com/m4lvin/HasCacBDD, version 0.1.0.4, Feb. 3, 2023
  * [12] Halpern, J.Y.: Reasoning about only knowing with many agents. In: Fikes, R., Lehnert, W.G. (eds.) Proceedings of the 11th National Conference on Artificial Intelligence. Washington, DC, USA, July 11-15, 1993. pp. 655–661. AAAI Press / The MIT Press (1993), http://www.aaai.org/Library/AAAI/1993/aaai93-098.php
  * [13] Halpern, J.Y., Lakemeyer, G.: Multi-agent only knowing. J. Log. Comput. 11(1), 41–70 (2001). https://doi.org/10.1093/logcom/11.1.41, https://doi.org/10.1093/logcom/11.1.41
  * [14] Lakemeyer, G.: All they know: A study in multi-agent autoepistemic reasoning. In: Bajcsy, R. (ed.) Proceedings of the 13th International Joint Conference on Artificial Intelligence. Chambéry, France, August 28 - September 3, 1993\. pp. 376–381. Morgan Kaufmann (1993), http://ijcai.org/Proceedings/93-1/Papers/053.pdf
  * [15] Levesque, H.J.: All I know: A study in autoepistemic logic. Artif. Intell. 42(2-3), 263–309 (1990). https://doi.org/10.1016/0004-3702(90)90056-6, https://doi.org/10.1016/0004-3702(90)90056-6
  * [16] Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: an open-source model checker for the verification of multi-agent systems. International Journal on Software Tools for Technology Transfer 19, 9–30 (2017)
  * [17] Lorini, E.: In praise of belief bases: Doing epistemic logic without possible worlds. In: Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence (AAAI-18). pp. 1915–1922. AAAI Press (2018)
  * [18] Lorini, E.: Exploiting belief bases for building rich epistemic structures. In: Moss, L.S. (ed.) Proceedings of the Seventeenth Conference on Theoretical Aspects of Rationality and Knowledge (TARK 2019). EPTCS, vol. 297, pp. 332–353 (2019)
  * [19] Lorini, E.: Rethinking epistemic logic with belief bases. Artificial Intelligence 282 (2020). https://doi.org/https://doi.org/10.1016/j.artint.2020.103233
  * [20] Mertens, J.F., Zamir, S.: Formulation of bayesian analysis for games with incomplete information. International Journal of Game Theory 14, 1–29 (1985). https://doi.org/https://doi.org/10.1007/BF01770224
  * [21] Stalnaker, R.: Common ground. Linguistics and Philosophy 25(5-6), 701–721 (2002)


# Quantum and classical query complexities for determining connectedness of
matroids

Xiaowei Huang  Institute of Quantum Computing and and Software, School of
Computer Science and Engineering, Sun Yat-sen University, Guangzhou 510006,
China  Shiguang Feng  Institute of Quantum Computing and and Software, School
of Computer Science and Engineering, Sun Yat-sen University, Guangzhou 510006,
China  Lvzhou<EMAIL_ADDRESS>Institute of Quantum Computing and
and Software, School of Computer Science and Engineering, Sun Yat-sen
University, Guangzhou 510006, China

###### Abstract

Connectivity is a fundamental structural property of matroids, and has been
studied algorithmically over 50 years. In 1974, Cunningham proposed a
deterministic algorithm consuming $O(n^{2})$ queries to the independence
oracle to determine whether a matroid is connected. Since then, no algorithm,
not even a random one, has worked better. To the best of our knowledge, the
classical query complexity lower bound and the quantum complexity for this
problem have not been considered. Thus, in this paper we are devoted to
addressing these issues, and our contributions are threefold as follows: (i)
First, we prove that the randomized query complexity of determining whether a
matroid is connected is $\Omega(n^{2})$ and thus the algorithm proposed by
Cunningham is optimal in classical computing. (ii) Second, we present a
quantum algorithm with $O(n^{3/2})$ queries, which exhibits provable quantum
speedups over classical ones. (iii) Third, we prove that any quantum algorithm
requires $\Omega(n)$ queries, which indicates that quantum algorithms can
achieve at most a quadratic speedup over classical ones. Therefore, we have a
relatively comprehensive understanding of the potential of quantum computing
in determining the connectedness of matroids.

Keywords: matroid, connectivity, query complexity, quantum computing

##  1 Introduction

The concept of matroid was originally introduced by Whitney [38] in 1935 as a
generalization of the concepts of linear spaces and graphs. Now matroids have
become ubiquitous in modern mathematics and computer science, and have various
applications in geometry, topology, network theory, coding theory and quantum
computing, especially in combinatorial optimization [2, 3, 16, 20, 25, 26,
32]. In combinatorial optimization, many important problems can be described
and solved based on matroid structures, which include greedy algorithms [14],
matroid intersection problem [10, 15, 24], matroid partition problem [10, 13],
etc. In addition, many matroid problems are interesting and valuable in their
own right from an algorithmic viewpoint.

###  1.1 Connectivity of Matroid

Connectivity is a fundamental structural property of matroids. The notion of
connectivity in matroid theory derived from the connectivity of graphs [35].
Since then, much work has been devoted to matroid connectivity, and it has
become one of the most interesting directions in matroid theory [5, 9, 29, 30,
31, 36].

Let $M$ be a matroid on the ground set $E$ with rank function $r$. A partition
$\\{E_{1},E_{2}\\}$ of $E$ is an _$m$ -separation_ of $M$ ($m\geq 1$), if
$\min\\{|E_{1}|,|E_{2}|\\}\geq m$ and $r(E_{1})+r(E_{2})-r(E)\leq m-1.$ The
_connectivity_ of $M$, denoted by $\lambda(M)$, is the minimum $k$ such that
$M$ has a $k$-separation. If $M$ has no such $k$, then $\lambda(M)=\infty$. In
general, a matroid $M$ is said to be _$k$ -connected_ for $k\geq 2$, if
$\lambda(M)\geq k$. A 2-connected matroid is usually called a _connected_ or
_non-separable_ matroid (see Definition 3).

###  1.2 Motivation and Problem Statement

Quantum computers have been shown to outperform classical computers in solving
some problems with significant application value [17, 33]. Discovering more
problems for which quantum computers exhibit speedups over classical ones is
one of the primary goals in the field of quantum computing. Considering
matroids are abstractions of some mathematical structures common to graph and
linear space, it is of great interest and meaningful to explore what matroid
problems can be faster solved on quantum computers than classical ones. To the
best of our knowledge, there are only few discussions on potential quantum
speedups in solving matroid problems [18, 19, 23]. Therefore, in this paper we
are trying to advance research in this direction. We investigate both quantum
and classical query complexities for determining whether a matroid is
connected, which is formally described as follows:

_Connected Matroid Problem (CMP). Given a matroid $M$ accessed by the
independence oracle, determine whether $M$ is connected._

Determining whether a graph is biconnected222An undirected graph is called
biconnected if there are two vertex-disjoint paths between any two vertices,
that is the graph is still connected after deleting any one vertex. is a
fundamental problem in graph theory. Biconnected graphs are instances of
connected matroids. A graph is biconnected if and only if the corresponding
cycle matroid is connected. It is of importance to study the Connected Matroid
Problem.

###  1.3 Our Contributions

Given a matroid $M=(E,\mathcal{I})$ with $|E|=n$ accessed by the independence
oracle, we prove the following main results.

  1. 1.

Any randomized algorithm that determines whether $M$ is connected with bounded
error 1/3 needs at least $\Omega(n^{2})$ queries to the independence oracle
(see Theorem 1).

  2. 2.

There is a quantum algorithm that determines whether $M$ is connected with
bounded error 1/3 using $O(n^{3/2})$ queries to the independence oracle (see
Theorem 2).

  3. 3.

Any quantum algorithm that determines whether $M$ is connected with bounded
error 1/3 needs at least $\Omega(n)$ queries to the independence oracle (see
Theorem 3).

Based on these results, we have a relatively comprehensive understanding of
the potential of quantum computing in determining the connectedness of
matroids. For the problem of determining whether a matroid is connected, one
can see that (i) Cunningham’s deterministic algorithm is optimal in classical
computing, (ii) quantum computers exhibit provable quantum speedups over
classical ones, and (iii) quantum computers can achieve at most a quadratic
speedup over classical ones.

To prove the lower bounds, we construct a disconnected matroid from a
connected matroid with the least number of bases (also known as the minimal
matroid [11]) by removing a base (see Lemma 7). Intuitively, the resulting
disconnected matroid and the minimal matroid are relatively hard to
distinguish. This is the keypoint for the proof of both the quantum and
classical lower bounds.

###  1.4 Related Work

In 1974, Cunningham [8] first considered CMP and proposed an algorithm using
$O(n^{2})$ queries to the independence oracle, where $n$ is the cardinality of
the ground set. In 1977, Krogdahl [22] proposed an algorithm similar to that
of Cunningham with the same query complexity when studying the dependence
graphs of bases in matroids. Bixby and Cunningham [5] gave an algorithm for
determining 3-connected. For $k>3$, Cunningham [8] presented an algorithm to
determine whether a matroid is $k$-connected. Jensen and Korte [21] showed
that there is no polynomial query algorithm to compute the connectivity of a
matroid.

Since Cunningham proposed the $O(n^{2})$ algorithm for CMP in 1974, no
algorithm, not even a random one, has worked better. As far as we know, the
classical query complexity lower bound and the quantum complexity for this
problem have not been considered. It is not known whether Cunningham’s
algorithm is optimal and whether there are more efficient quantum algorithms
to determine the connectedness of matroids.

###  1.5 Organization

The remainder of this paper is organized as follows. In Section 2, some basic
concepts in matroid theory and query model are introduced. In Section 3, we
prove the lower bound on randomized query complexity. In Section 4, we give a
quantum algorithm determining the connectedness of matroids. In Section 5, we
prove the lower bound on quantum query complexity. In Section 6, we conclude
this paper.

##  2 Preliminaries

Notations: Let $E$ be a finite set, $A\subseteq E$, and $x\in E$. We use
$|E|$, $A+x$, and $A-x$ to denote the cardinality of $E$, the set
$A\cup\\{x\\}$, and the set $A-\\{x\\}$, respectively. For a positive integer
$n$, we use $[n]$ to denote the set $\\{1,\dots,n\\}$. For a string
$x\in\\{0,1\\}^{n},i\in[n]$, $x_{i}$ denotes the $i$-th bit of $x$.

###  2.1 Matroid Theory

Here we give some basic definitions and concepts on matroids. Matroid theory
is established as a generalization of linear algebra and graph theory. Some
concepts are similar to those of linear algebra or graphs. We refer the reader
to [28] and [37] for more details about matroid theory.

######  Definition 1 (Matroid).

A _matroid_ is a combinational object defined by the tuple $M=(E,\mathcal{I})$
on the finite ground set $E$ and $\mathcal{I}\subseteq 2^{E}$ such that the
following properties hold:

  1. I0.

$\emptyset\in\mathcal{I}$;

  2. I1.

If $A^{\prime}\subseteq A$ and $A\in\mathcal{I}$, then
$A^{\prime}\in\mathcal{I}$;

  3. I2.

For any two sets $A,B\in\mathcal{I}$ with $|A|<|B|$, there exists an element
$x\in B-A$ such that $A+x\in\mathcal{I}$.

The members of $\mathcal{I}$ are the _independent_ sets of $M$. The subsets of
$E$ not belonging to $\mathcal{I}$ are called _dependent_. A _base_ of $M$ is
a maximal independent set, and the collection of bases is denoted by
$\mathcal{B}(M)$. A _circuit_ of $M$ is a minimal dependent set, and the
collection of circuits is denoted by $\mathcal{C}(M)$.

######  Definition 2 (Rank).

The _rank function_ of a matroid $M=(E,\mathcal{I})$ is the function
$r:2^{E}\rightarrow\mathbb{Z}$ defined by

$r(A)=\max\Big{\\{}|X|:X\subseteq
A,X\in\mathcal{I}\Big{\\}}\;\;\;\;\;\;(A\subseteq E).$ (1)

The rank of $M$, denoted by $r(M)$, is $r(E)$.

######  Lemma 1 (Base Axioms).

A non-empty collection $\mathcal{B}$ of subsets of $E$ is the set of bases of
a matroid on $E$ if and only if it satisfies the following condition:

  * (B1)

If $B_{1},B_{2}\in\mathcal{B}$ and $x\in B_{1}-B_{2}$, then there exists $y\in
B_{2}-B_{1}$ such that $B_{1}+y-x\in\mathcal{B}$.

######  Lemma 2 (Circuit Axioms).

A non-empty collection $\mathcal{C}$ of subsets of $E$ is the set of circuits
of a matroid on $E$ if and only if it satisfies the following conditions:

  * (C1)

If $X,Y\in\mathcal{C}$ and $X\neq Y$, then $X\nsubseteq Y$.

  * (C2)

If $C_{1},C_{2}$ are distinct members of $\mathcal{C}$ and $z\in C_{1}\cap
C_{2}$, then there exists $C_{3}\in\mathcal{C}$ such that
$C_{3}\subseteq(C_{1}\cup C_{2})-z$.

The proofs of the two lemmas above can be found in [28, 37].

######  Fact 1.

Let $M=(E,\mathcal{I})$ be a matroid. If $B$ is a base of $M$ and $x\in E-B$,
then there exists a unique circuit $C(x,B)$ such that

${C(x,B)}\subseteq{B}+x,\text{ and }x\in{C(x,B)}.$

The circuit $C(x,B)$ is called the fundamental circuit of $x$ in the base $B$.

######  Definition 3 (Connected Matroid).

A matroid $M=(E,\mathcal{I})$ with rank function $r$ is called _connected_ if
every nonempty proper subset $A$ of $E$ satisfies

$r(A)+r(E-A)>r(E).$

Otherwise $M$ is _disconnected_.

######  Lemma 3.

A matroid $M=(E,\mathcal{I})$ is _connected_ if and only if for every pair of
distinct elements $x$ and $y$ of $E$ there is a circuit of $M$ containing $x$
and $y$.

The proof of Lemma 3 can be found in [28, 37].

######  Definition 4 (Independence Oracle).

Let $M=(E,\mathcal{I})$ be a matroid. An _independence oracle_ of $M$ is a
function $O_{i}:2^{E}\rightarrow\\{0,1\\}$, for $S\in E$, such that

$O_{i}(S)=\left\\{\begin{array}[]{ll}1&\text{if}\;S\in\mathcal{I},\\\
0&\text{otherwise}.\end{array}\right.$

In the quantum setting, we also use $O_{i}$ as the quantum independence oracle
that maps $|S\rangle|b\rangle$ to $|S\rangle|b\oplus O_{i}(S)\rangle$.

###  2.2 Query Models and Quantum Computing

In this subsection, we briefly introduce the query complexity for
deterministic, randomized, and quantum computing models. For more details
about the query complexity and quantum computing, we refer the reader to [7,
27].

#### Decision Tree

Let $f:\\{0,1\\}^{n}\rightarrow\\{0,1\\}$ be a Boolean function. A
_(deterministic) decision tree_ (which is also called a deterministic query
algorithm) for $f$ is a binary tree $T$ in which each internal node is
labelled with a variable $x_{i}$, and has two outgoing edges labelled with 0
and 1, respectively. Each leaf node is labelled with 0 or 1. Given an input
$x$, the tree $T$ is evaluated as follows. Start at the root node, say with
label $x_{j}$, get the value of $x_{j}$ by querying $x$, if $x_{j}=1$ then
choose the subtree reached by taking the 1-edge, otherwise, choose the subtree
reached by taking the 0-edge. Repeat the procedure recursively until a leaf
node is reached. The label of the leaf node is $f(x)$.

With the decision tree, we can define the complexity measures for $f$.

######  Definition 5.

The cost of a deterministic decision tree $T$ on an input $x$, denoted by
$cost(T,x)$, is the number of queries made on $x$ when evaluating $T$.

######  Definition 6.

The deterministic query complexity of a function $f$, denoted by $D(f)$, is

$D(f)=\min_{T\in\mathcal{T}}\max_{x\in\\{0,1\\}^{n}}cost(T,x),$ (2)

where $\mathcal{T}$ is the set of decision trees that compute $f$.

#### Randomized Decision Tree

There are two equivalent ways to define a randomized decision tree. The first
way is to define a randomized decision tree in which the branch taken at each
node is determined by the query value or a random coin flip (possibly biased).
The second is to define a randomized decision tree as a probability
distribution $P$ over deterministic decision trees. The randomized decision
tree is evaluated by choosing a deterministic decision tree according to $P$.

We say that a randomized decision tree computes $f$ with bounded-error if its
output equals $f(x)$ with probability at least 2/3, for all
$x\in\\{0,1\\}^{n}$.

######  Definition 7.

The cost of a randomized decision tree over a probability distribution $P$ on
an input $x$, denoted by $cost(P,x)$, is the expected number of queries made
on $x$ over $P$,

$cost(P,x)=\sum_{T\in\mathcal{T}}P(T)cost(T,x).$ (3)

######  Definition 8.

The randomized query complexity of a function $f$, denoted by $R(f)$, is

$R(f)=\min_{P\in\mathcal{P}}\max_{x\in\\{0,1\\}^{n}}cost(P,x),$ (4)

where $\mathcal{P}$ is the set of probability distributions over deterministic
decision trees that compute $f$ with bounded-error.

Let $A$ be a deterministic algorithm that outputs 1 or 0 for any input $x$ of
the domain of $f$, let $\epsilon(A,x)=0$ if $A$ outputs $f(x)$, and
$\epsilon(A,x)=1$ otherwise.

######  Definition 9.

Let $\mu$ be a probability distribution over the domain of $f$. We say that a
deterministic algorithm $A$ computes $f$ over $\mu$ if

$\sum_{x\sim\mu}\mu(x)\epsilon(A,x)<1/3.$

######  Definition 10.

Let $\mu$ be a probability distribution over the domain of $f$. The
distributional query complexity of $f$ on $\mu$, denoted by $D_{\mu}(f)$, is

$D_{\mu}(f)=\min_{A\in\mathcal{A}_{\mu}}\sum_{x\sim\mu}\mu(x)cost(A,x),$

where $\mathcal{A}_{\mu}$ is the set of deterministic algorithms that compute
$f$ over $\mu$.

######  Lemma 4 (Yao’s minimax principle [39]).

Let $\mathcal{D}\subseteq\\{0,1\\}^{n}$, for any Boolean function
$f:\mathcal{D}\rightarrow\\{0,1\\}$,

  * (1)

$D_{\mu}(f)\leq R(f)$ for every distribution $\mu$ over $\mathcal{D}$, and

  * (2)

$D_{\mu}(f)=R(f)$ for some distribution $\mu$ over $\mathcal{D}$.

In general, it is difficult to find the randomized query complexity of a
problem directly. Yao’s minimax principle gives a possible way to find the
randomized query complexity, which is one of the most commonly used methods.

#### Quantum Decision Tree

Let $x$ be a binary string of length $n$. In the quantum query models [4], we
use $O_{x}$ to denote the query oracle for $x$, and define $O_{x}$ as a
unitary operation

$O_{x}:|i,y\rangle\rightarrow|i,y\oplus{x_{i}}\rangle,$ (5)

where $y$ is one qubit, $i$ is an index of $\lceil\log n\rceil$ qubits for
every bit of $x$, the variable $x_{i}$ denotes the $i$-th bit of $x$, and
$\oplus$ is the _exclusive-or_ operator.

A _quantum decision tree_ on an input $x$ runs as follows: start with an
initial state $\ket*{\vv{0}}$, then apply a unitary operation $U_{0}$ to the
state, then apply a query $O_{x}$, then apply another unitary operation
$U_{1}$, and so on. Thus, a $T$-query quantum decision tree corresponds to a
sequence $U=U_{T}O_{x}\cdots O_{x}U_{1}O_{x}U_{0}$ of unitary operations
$\\{U_{i}:i=0,\dots,T\\}$ and $O_{x}$. Here each $U_{i}$ $(0\leq i\leq T)$ is
a unitary operation that is independent of $x$. The result is obtained by
measuring the final state $U\ket*{\vv{0}}$.

We say that a $T$-query quantum decision tree computes $f$ with bounded-error
if the computing result equals $f(x)$ with probability at least 2/3. The
quantum query complexity of a function $f$, denoted by $Q(f)$, is the least
$T$ such that there is a $T$-query quantum decision tree that computes $f$
(with bounded-error 1/3). Note that the quantum query complexity only
considers the number of queries to the oracle $O_{x}$, but not $U_{i}$.

######  Fact 2.

$Q(f)\leq R(f)\leq D(f)$.

##  3 Lower Bound on Randomized Query Complexity

In this section, we prove the randomized query complexity of CMP. We first
introduce a special class of connected matroids of rank $r$ on $n$ elements
with $r(n-r)+1$ bases that are studied by Dinolt [11]. This kind of matroid is
called _minimal matroid_. Then we prove a key result, Lemma 7, which shows
that a disconnected matroid can be obtained by removing any base of a minimal
matroid. Intuitively, the resulting disconnected matroid and the minimal
matroid are relatively hard to distinguish. This is the keypoint for the proof
of both quantum and classical lower bounds.

######  Lemma 5 ([11]).

A connected matroid with rank $r$ on a ground set with cardinality $n$ has at
least $r(n-r)+1$ bases. For any positive integers $n$ and $r$ with $n>r$,
there exists one (up to isomorphism) connected matroid $M=(E,\mathcal{I})$
with $|E|=n,r(E)=r$ and $|\mathcal{B}(M)|=r(n-r)+1$.

######  Lemma 6 ([11]).

Let $r$ and $n$ be two integers with $0<r<n$, and
$E=\\{e_{1},\dots,e_{r},e_{r+1},\dots,e_{n}\\}$,
$E_{0}=\\{e_{1},\dots,e_{r}\\}$,
$\overline{E_{0}}=E-E_{0}=\\{e_{r+1},\dots,e_{n}\\}$,
$\mathcal{C}=\\{E_{0}+e_{j}:e_{j}\in\overline{E_{0}}\\}$$\cup$
$\\{\\{e_{j},e_{j^{\prime}}\\}:e_{j},e_{j^{\prime}}\in\overline{E_{0}},j\neq
j^{\prime}\\}$. Then $\mathcal{C}$ is the set of circuits of a minimal matroid
on $E$ with rank $r$.

###### Proof.

By the Circuit Axioms, it is easy to verify that $\mathcal{C}$ is the set of
circuits of a matroid on $E$ with rank $r$. We denote the matroid by
$M(\mathcal{C})$. For any two distinct elements $x$ and $y$ of $E$, it is not
hard to find an element of $\mathcal{C}$ that contains both $x$ and $y$. This
implies that $M(\mathcal{C})$ is connected.

Furthermore, we can get the set $\mathcal{B}(M(\mathcal{C}))$ of bases of
$M(\mathcal{C})$ is

$\mathcal{B}(M(\mathcal{C}))=\\{E_{0}\\}\cup\\{E_{0}-e_{i}+e_{j}:e_{i}\in
E_{0},e_{j}\in\overline{E_{0}}\\},$

and $|\mathcal{B}(M(\mathcal{C}))|=r(n-r)+1$. Therefore, $M(\mathcal{C})$ is a
minimal matroid. ∎

In the following, we prove a fundamental lemma that is used to prove the lower
bounds of both the quantum and classical query complexity. Generally, the
removal (a base) operation is not a well-defined operation on matroids. But
for some special matroids (for instance, the minimal matroids), we can
construct new matroids by the removal operations.

######  Lemma 7.

Let $M$ be the minimal matroid defined by $\mathcal{C}$ on $E$ as in the proof
of Lemma 6, $\mathcal{B}$ the set of bases of $M$. Then for any
$B\in\mathcal{B}$, there is a disconnected matroid $M_{B}$ on $E$ with rank
$r$ such that $\mathcal{B}-B$ is the set of bases of $M_{B}$.

###### Proof.

We prove that the set $\mathcal{B}-B$ satisfies the condition in the Base
Axioms. For $r<n$, it is easy to see that $\mathcal{B}-B$ is not empty. To
prove $\mathcal{B}-B$ satisfies the condition (B1), we proceed by considering
the following two cases.

Case 1. If $B=E_{0}$, we show that $\mathcal{B}_{1}=$
$\mathcal{B}-B=\\{E_{0}-e_{i}+e_{j}:e_{i}\in
E_{0},e_{j}\in\overline{E_{0}}\\}$ satisfies the Base Axioms. Let
$B_{1}=E_{0}-x_{1}+y_{1}$ and $B_{2}=E_{0}-x_{2}+y_{2}$, where $x_{1},x_{2}\in
E_{0}$ and $y_{1},y_{2}\in\overline{E_{0}}$. Assume that $B_{1}\neq B_{2}$.

(1)

If $x_{1}=x_{2}$, then it implies $y_{1}\neq y_{2}$. We have
$B_{1}+y_{2}-y_{1}=B_{2}\in\mathcal{B}_{1}$.

(2)

If $y_{1}=y_{2}$, then it implies $x_{1}\neq x_{2}$. We have
$B_{1}+x_{1}-x_{2}=B_{2}\in\mathcal{B}_{1}$.

(3)

If $x_{1}\neq x_{2}$ and $y_{1}\neq y_{2}$, then
$B_{1}-B_{2}=\\{x_{2},y_{1}\\},B_{2}-B_{1}=\\{x_{1},y_{2}\\}$. We have
$B_{1}+x_{1}-x_{2}=E_{0}-x_{2}+y_{1}\in\mathcal{B}_{1}$.

Thus, we can see that $\mathcal{B}_{1}$ satisfies the Base Axioms.

Case 2. If $B=E_{0}-x+y$ for $x\in E_{0},y\in\overline{E_{0}}$, we show that
$\mathcal{B}_{2}=\mathcal{B}-B$ satisfies the Base Axioms. It is easy to check
that $B_{1}+y-x=B_{2}\in\mathcal{B}_{2}$ if
$B_{1}=E_{0},B_{2}=E_{0}-x^{\prime}+y^{\prime}\neq B$ for $x^{\prime}\in
E_{0}$ and $y^{\prime}\in\overline{E_{0}}$.

Let $B_{1}=E_{0}-x_{1}+y_{1}\neq B$ and $B_{2}=E_{0}-x_{2}+y_{2}\neq B$, where
$x_{1},x_{2}\in E_{0}$ and $y_{1},y_{2}\in\overline{E_{0}}$. Assume that
$B_{1}\neq B_{2}$. The cases $x_{1}=x_{2}$ and $y_{1}=y_{2}$ are the same as
(1) and (2) in Case 1, respectively. If $x_{1}\neq x_{2}$ and $y_{1}\neq
y_{2}$, then $B_{1}-B_{2}=\\{x_{2},y_{1}\\}$ and
$B_{2}-B_{1}=\\{x_{1},y_{2}\\}$. We have
$B_{1}+x_{1}-y_{1}=E_{0}\in\mathbf{B}_{2}$. Thus, we can see that
$\mathcal{B}_{2}$ satisfies the Base Axioms.

Combining Case 1 and Case 2, we know that for any $B\in\mathcal{B}$,
$\mathcal{B}-B$ is the set of bases of a matroid on $E$ with rank $r$. We
denote this matroid as $M_{B}$. Because $r(M_{B})=r$ and
$|\mathcal{B}-B|=r(n-r)$, by Lemma 5, it follows that $M_{B}$ is disconnected.
∎

The following theorem is the main result of this section.

######  Theorem 1.

Given a matroid $M$ on a ground set with cardinality $n$ accessed by the
independence oracle, any randomized algorithm that determines whether $M$ is
connected with bounded error $1/3$ needs at least $\Omega(n^{2})$ queries to
the independence oracle.

###### Proof.

We shall show that the lower bound of the distributional complexity of CMP is
$\Omega(n^{2})$. Then by Yao’s minimax principle, we have
$R(\textbf{CMP})=\Omega(n^{2})$.

Let $M$ be a minimal matroid with rank $r$ on a ground set of cardinality $n$,
$N=r(n-r)+1$, $\mathcal{B}=\\{B_{i}:i\in[N]\\}$ the set of bases of $M$. For
any $B\in\mathcal{B}$, let $M_{B}$ be the matroid whose set of bases is
determined by the set $\mathcal{B}-B$ as defined in Lemma 7.

We begin by picking the input distribution $x\sim\mu$ defined as follows:

  * (1)

Sample $i\in[N]$ uniformly at random.

  * (2)

Set $x=M$ or $x=M_{B_{i}}$ with probability $\frac{1}{2}$.

Fix any deterministic algorithm $A$ computing CMP on the distribution $\mu$
with bounded error $1/3$. We use $T$ to denote the number of queries made by
$A$. Let $K=\\{i_{1},\dots,i_{T}\\}$ be the set of queries made by $A$ where
the answer to every one of these queries is 1 (this means that what we are
querying is a base of the input matroid). Since $A$ is deterministic, the set
$K$ is fixed and well-defined. For any input $x\sim\mu$ to the algorithm $A$,
we have

$\Pr(i\in K)=\frac{|K|}{N}=\frac{T}{N}.$ (6)

Define $E(x)$ as the event that the algorithm $A$ succeeds on computing $x$.
At the same time, conditioned on $i\notin K$, the input is $M$ or $M_{B_{i}}$
with probability $\frac{1}{2}$. Hence,

$\Pr(E(x)|i\notin K)=\frac{1}{2}.$ (7)

Combining the above, we have

$\begin{array}[]{rcl}2/3&\leq&\Pr(E(x))_{x\sim\mu}\\\ &=&\Pr(i\in
K)\Pr(E(x)|i\in K)+\Pr(i\notin K)\Pr(E(x)|i\notin K)\\\
&\leq&\frac{T}{N}+(1-\frac{T}{N})\cdot\frac{1}{2},\end{array}$ (8)

which implies $T\geq N/3$. When $r=n/2$, we get $T>n^{2}/12$. Consequently,
$D_{\mu}(\textbf{CMP})=\Omega(n^{2})$, thus the randomized query complexity of
CMP is $\Omega(n^{2})$. ∎

##  4 Quantum Algorithm for Determining Connected Matroids

In this section, we give a quantum algorithm to determine whether a matroid is
connected. Firstly, we introduce the partial representation of matroids and
the corresponding bipartite graphs. The relation between the connectedness of
matroids and the connectedness of the corresponding bipartite graphs is given
in Lemma 8. This leads to an efficient algorithm to determine the
connectedness of matroids. Secondly, we construct the oracle for the adjacency
matrix model of the corresponding bipartite graph from the independence oracle
of the matroid. Finally, we introduce the quantum search algorithm in Lemma 9.
Combining the above, we give a quantum algorithm.

##### Partial Representation.

Partial representation is introduced by Truemper [34]. Let $M$ be a matroid on
a finite ground set $E$, and $B$ a base of $M$. The _partial representation_
of $M$ with respect to $B$ is a $\\{0,1\\}$-matrix $P$ with rows indexed on
elements $x\in B$ and columns indexed on elements $y\in\overline{B}=E-B$ such
that the entry $P(x,y)$ is 1 if and only if $x\in C(y,B)$, otherwise $P(x,y)$
is 0. A bipartite graph $G(P)$ derived from $P$ is obtained by setting one
node for each row and column of $P$ and one edge for each nonzero entry.
Krogdahl [22] proved the relationship of the connectedness between $M$ and
$G(P)$ in Lemma 8.

######  Lemma 8 ([22]).

Let $M$ be a matroid, $B$ a base of $M$, $P$ the partial representation
corresponding to $B$ and $G(P)$ the associated bipartite graph. Then $M$ is
connected if and only if $G(P)$ is connected.

Based on an idea similar to Lemma 8, Cunningham [8] gave a very pretty and
efficient algorithm determining whether a matroid is connected, which takes
$O(|E|^{2})$ queries to the independence oracle.

##### Adjacency Matrix Model.

In the adjacency matrix model, an undirected graph $G=(V,A)$ is given as an
adjacency matrix $P\in\\{0,1\\}^{|V|\times|V|}$ such that $P_{ij}=1$ if and
only if $(v_{i},v_{j})\in A$ for $v_{i},v_{j}\in V$.

Let $M$ be a matroid on $E$, $B$ a base of $M$, $P$ the partial representation
corresponding to $B$ and $G(P)$ the associated bipartite graph. Since $G(P)$
is a bipartite graph, $P$ is essentially the adjacency matrix of $G(P)$.
Therefore, it is not difficult to construct an oracle $O$ that accesses $P$
from the independence oracle $O_{i}$ as follows:

$\displaystyle
O(j,k)=\left\\{\begin{array}[]{ll}O_{i}(B+k-j)&\text{if}\;\;j\in
B\;\;\text{and}\;\;k\in\overline{B},\\\ 0&\text{otherwise}.\end{array}\right.$
(11)

In [12], Dürr et al. give a quantum algorithm to determine the connectedness
of graphs and show that the quantum query complexity is $\Theta(n^{3/2})$ in
the adjacency matrix model, where $n$ is the number of vertices in the graph.
Since we only need to determine the connectedness of $G(P)$ without finding
its spanning tree, and deal with bipartite graphs, we give a quantum algorithm
that is actually more efficient with the quantum depth-first search method.

##### Quantum search.

A search problem on a set $[n]$ with $n$ elements is a subset $J\subseteq[n]$
with the characteristic function $f:[n]\rightarrow\\{0,1\\}$ such that

$f(x)=\left\\{\begin{array}[]{ll}1&\text{if}\;x\in J,\\\
0&\text{otherwise}.\end{array}\right.$

Any $x\in J$ is called a solution of the search problem.

######  Lemma 9 (Grover’s algorithm [6, 17]).

Let $J$ be a search problem on a set $[n]$ with $n$ elements, $|J|=k$ and $f$
the characteristic function of $J$. Given a search space $S\subseteq[n]$ with
$|S|=N$, the expected quantum query complexity for finding one solution of $J$
is $O(\sqrt{N/k})$ for $k>0$. Whether $J\cap S$ is empty can be determined in
$O(\sqrt{N})$ quantum queries to $f$ with success probability at least 2/3.

Our main result in this section is as follows.

######  Theorem 2.

Given a matroid $M$ on a ground set with cardinality $n$ accessed by the
independence oracle, there is a quantum algorithm that determines whether $M$
is connected with bounded error $1/3$ using $O(n^{3/2})$ queries to the
independence oracle.

###### Proof.

Consider Algorithm 1, after finding a base $B$ of $M$ using a greedy
algorithm, it uses the depth-first search method to determine whether the
associated bipartite graph is connected. In Line 5, the oracle $O$ used by
Grover’s algorithm is defined by Equation (11). Thus, it is not difficult to
see the correctness of Algorithm 1.

Algorithm 1 A quantum algorithm deciding whether a matroid is connected.

0: A matroid $M$ accessed through the independence oracle $O_{i}$.

0: YES if $M$ is connected, otherwise NO.

1: $B\leftarrow\;$Find a base of $M$ with greedy algorithm.

2: Let $s\in B$, PUSH($S$,$s$).//S is a stack, and PUSH, TOP, and POP are
operations of the stack.

3: while $S$ is not empty do

4: $u\leftarrow$ TOP($S$).

5: Use Grover’s algorithm to find an unmarked vertex $v$ with $O(u,v)=1$.

6: if such a vertex $v$ exists then

7: PUSH($S$,$v$)

8: else

9: $t\leftarrow$ POP($S$), mark $t$ as visited.

10: end if

11: end while

12: if all the vertices are visited then

13: return YES.

14: else

15: return NO.

16: end if

Next, we prove the query complexity of Algorithm 1. Let $M$ be defined on $E$
whose cardinality is $n$, $|B|=r$, and $\overline{B}=E-B$. Finding a base $B$
of $M$ needs $O(n)$ queries to the independence oracle. For any $s\in B$,
every vertex is discovered by the depth-first search at most once. In the
adjacency matrix model, if $u\in B$, then the next vertex is found by
$O(\sqrt{n-r})$ quantum queries to the independence oracle. If
$u\in\overline{B}$, it takes $O(\sqrt{r})$ queries. The total query is
$O(n)+(n-r)O(\sqrt{n-r})+rO(\sqrt{r})$, which is bounded by $O(n^{3/2})$. ∎

##  5 Lower Bound on Quantum Query Complexity

In this section, we prove the quantum query complexity of CMP. Firstly, we
introduce the quantum adversary method proposed by Ambainis [1] in Lemma 10,
which is one of the common methods to prove the lower bound of quantum query
complexity. In order to use the quantum adversary method to prove the quantum
query complexity of CMP, we need to encode matroids to 0-1 strings as done in
graphs, where each bit represents a subset of the ground set. Then we can
express CMP by a Boolean function. And the function is a partial function
since not every string is a representation of a matroid. Combining Lemma 6 and
Lemma 7, we can give a lower bound for quantum complexity of CMP.

######  Lemma 10 (Ambainis’s quantum adversary method [1]).

Let $f$ be a function of $n$ $\\{0,1\\}$-valued variables, and $X,Y$ two sets
of inputs such that $f(x)\neq f(y)$ if $x\in X$ and $y\in Y$. Let $R\subseteq
X\times Y$ be a relation such that

  * 1.

for every $x\in X$, there are at least $m$ different $y\in Y$ such that
$(x,y)\in R$;

  * 2.

for every $y\in Y$, there are at least $m^{\prime}$ different $x\in X$ such
that $(x,y)\in R$;

  * 3.

for every $x\in X$ and $i\in[n]$, there are at most $l$ different $y\in Y$
such that $(x,y)\in R$ and $x_{i}\neq y_{i}$;

  * 4.

for every $y\in Y$ and $i\in[n]$, there are at most $l^{\prime}$ different
$x\in X$ such that $(x,y)\in R$ and $x_{i}\neq y_{i}$.

Then any quantum algorithm computing $f$ with bounded error 1/3 takes at least
$\Omega(\sqrt{\frac{mm^{\prime}}{ll^{\prime}}})$ queries.

Our main result in this section is as follows.

######  Theorem 3.

Given a matroid $M$ on a ground set with cardinality $n$ accessed by the
independence oracle, any quantum algorithm that determines whether $M$ is
connected with bounded error $1/3$ needs at least $\Omega(n)$ queries to the
independence oracle.

###### Proof.

Let $E$ be a finite ground set with cardinality $n$, $\mathcal{M}$ the set of
matroids on $E$. We define a mapping

$\chi:\mathcal{M}\rightarrow\\{0,1\\}^{2^{n}},$ (12)

for every matroid $M\in\mathcal{M}$. Let $\chi(M)$ be the unique string
encoding $M$, where different bits represent different subsets of $E$ and the
appearance of ‘1’ indicates that the corresponding subset is an independent
set of $M$.

Define a Boolean function

$f:\mathcal{D}\rightarrow\\{0,1\\}$ (13)

that computes the connectedness of matroids on $E$, where
$\mathcal{D}\subseteq\\{0,1\\}^{2^{n}}$ contains the valid strings encoding
the matroids on $E$. For any $x\in\mathcal{D}$, $f(x)=1$ indicates that the
matroid encoded by $x$ is connected, otherwise $f(x)=0$. Let $M_{0}$ be a
minimal matroid of rank $n/2$ on $E$, and $\mathcal{B}$ the set of bases of
$M_{0}$. Let $X=\\{\chi(M_{0}\\}$, $Y=\\{\chi(M_{B}):B\in\mathcal{B}\\}$,
where $M_{B}$ is a disconnected matroid defined in Lemma 7. By Lemma 10, we
can see that any quantum algorithm computing $f$ with bounded error 1/3 takes
at least $\Omega(\sqrt{|X||Y|})=\Omega(n)$ queries. ∎

##  6 Conclusion

In this paper, we consider the query complexity and quantum algorithm for
determining the connectedness of matroids. We show that the randomized query
complexity is $\Omega(n^{2})$ and thus the deterministic algorithm proposed by
Cunningham is optimal. We also give a quantum algorithm taking $O(n^{3/2})$
queries and prove that the quantum query complexity is $\Omega(n)$, which
indicates that quantum algorithms can achieve at most a quadratic speedup over
classical ones. Therefore, we have a relatively comprehensive understanding of
the potential of quantum computing in determining the connectedness of
matroids. Obviously, there is still a gap between the lower and upper bounds
of the quantum query complexity. It is quite possible to believe that this
quantum lower bound is not the optimal one. Finding a tight lower bound for
the quantum query complexity of this problem can be the future work of our
research.

## References

  * [1] Ambainis, A., and Spalek, R. Quantum algorithms for matching and network flows.  In STACS 2006, 23rd Annual Symposium on Theoretical Aspects of Computer Science, Marseille, France, February 23-25, 2006, Proceedings (2006), B. Durand and W. Thomas, Eds., vol. 3884 of Lecture Notes in Computer Science, Springer, pp. 172–183.
  * [2] Amy, M., Maslov, D., and Mosca, M. Polynomial-time t-depth optimization of clifford+t circuits via matroid partitioning.  IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 33, 10 (2014), 1476–1489.
  * [3] Bassoli, R., Marques, H., Rodriguez, J., Shum, K. W., and Tafazolli, R. Network coding theory: A survey.  IEEE Commun. Surv. Tutorials 15, 4 (2013), 1950–1978.
  * [4] Beals, R., Buhrman, H., Cleve, R., Mosca, M., and de Wolf, R. Quantum lower bounds by polynomials.  In 39th Annual Symposium on Foundations of Computer Science, FOCS ’98, November 8-11, 1998, Palo Alto, California, USA (1998), IEEE Computer Society, pp. 352–361.
  * [5] Bixby, R. E., and Cunningham, W. H. Matroids, graphs, and $3$-connectivity.  In Graph theory and related topics (Proc. Conf., Univ. Waterloo, Waterloo, Ont., 1977) (1979), Academic Press, New York-London, pp. 91–103.
  * [6] Boyer, M., Brassard, G., Høyer, P., and Tapp, A. Tight bounds on quantum searching.  Fortschritte der Physik: Progress of Physics 46, 4-5 (1998), 493–505.
  * [7] Buhrman, H., and de Wolf, R. Complexity measures and decision tree complexity: a survey.  Theor. Comput. Sci. 288, 1 (2002), 21–43.
  * [8] Cunningham, W. H. A combinatorial decomposition theory.  ProQuest LLC, Ann Arbor, MI, 1974.  Thesis (Ph.D.)–University of Waterloo (Canada).
  * [9] Cunningham, W. H. On matroid connectivity.  J. Combin. Theory Ser. B 30, 1 (1981), 94–99.
  * [10] Cunningham, W. H. Improved bounds for matroid partition and intersection algorithms.  SIAM J. Comput. 15, 4 (1986), 948–957.
  * [11] Dinolt, G. W. An extremal problem for non-separable matroids.  In Théorie des matroïdes (Rencontre Franco-Britannique, Brest, 1970), Lecture Notes in Math., Vol. 211. Springer, Berlin, 1971, pp. 31–49.
  * [12] Dürr, C., Heiligman, M., HOyer, P., and Mhalla, M. Quantum query complexity of some graph problems.  SIAM Journal on Computing 35, 6 (2006), 1310–1328.
  * [13] Edmonds, J. Matroid partition.  In Mathematics of the Decision Sciences, Parts 1, 2 (Seminar, Stanford, Calif., 1967). Amer. Math. Soc., Providence, R.I., 1968, pp. 335–345.
  * [14] Edmonds, J. Matroids and the greedy algorithm.  Mathematical programming 1, 1 (1971), 127–136.
  * [15] Edmonds, J. Matroid intersection.  vol. 4. 1979, pp. 39–49.  Discrete optimization (Proc. Adv. Res. Inst. Discrete Optimization and Systems Appl., Banff, Alta., 1977), I.
  * [16] Edmonds, J. R. Matroids and the greedy algorithm.  Math. Program. 1, 1 (1971), 127–136.
  * [17] Grover, L. K. A fast quantum mechanical algorithm for database search.  In Proceedings of the Twenty-Eighth Annual ACM Symposium on the Theory of Computing, Philadelphia, Pennsylvania, USA, May 22-24, 1996 (1996), G. L. Miller, Ed., ACM, pp. 212–219.
  * [18] Huang, X., Luo, J., and Li, L. Quantum speedup and limitations on matroid properties.  arXiv preprint arXiv:2111.12900 (2021).
  * [19] Huang, X., Zhang, S., and Li, L. Quantum algorithms for identifying hidden strings with applications to matroid problems.  arXiv preprint arXiv:2211.10667 (2022).
  * [20] Iri, M. Applications of matroid theory.  In Mathematical Programming The State of the Art, XIth International Symposium on Mathematical Programming, Bonn, Germany, August 23-27, 1982 (1982), A. Bachem, B. Korte, and M. Grötschel, Eds., Springer, pp. 158–201.
  * [21] Jensen, P. M., and Korte, B. Complexity of matroid property algorithms.  SIAM J. Comput. 11, 1 (1982), 184–190.
  * [22] Krogdahl, S. The dependence graph for bases in matroids.  Discrete Mathematics 19, 1 (1977), 47–59.
  * [23] Kulkarni, R., and Santha, M. Query complexity of matroids.  In Algorithms and Complexity, 8th International Conference, CIAC 2013, Barcelona, Spain, May 22-24, 2013. Proceedings (2013), P. G. Spirakis and M. J. Serna, Eds., vol. 7878 of Lecture Notes in Computer Science, Springer, pp. 300–311.
  * [24] Lawler, E. L. Matroid intersection algorithms.  Math. Programming 9, 1 (1975), 31–56.
  * [25] Lawler, E. L. Combinatorial optimization: networks and matroids.  Holt, Rinehart and Winston, New York-Montreal, Que.-London, 1976.
  * [26] Mann, R. L. Simulating quantum computations with tutte polynomials.  CoRR abs/2101.00211 (2021).
  * [27] Nielsen, M. A., and Chuang, I. L. Quantum Computation and Quantum Information: 10th Anniversary Edition.  Cambridge University Press, 2010.
  * [28] Oxley, J. Matroid theory, second ed., vol. 21 of Oxford Graduate Texts in Mathematics.  Oxford University Press, Oxford, 2011.
  * [29] Oxley, J. G. On matroid connectivity.  Quart. J. Math. Oxford Ser. (2) 32, 126 (1981), 193–208.
  * [30] Oxley, J. G. On some extremal connectivity results for graphs and matroids.  Discrete Math. 41, 2 (1982), 181–198.
  * [31] Seymour, P. D. On the connectivity function of a matroid.  J. Combin. Theory Ser. B 45, 1 (1988), 25–30.
  * [32] Shepherd, D., and Bremner, M. J. Temporally unstructured quantum computation.  Proceedings: Mathematical, Physical and Engineering Sciences 465, 2105 (2009), 1413–1439.
  * [33] Shor, P. W. Algorithms for quantum computation: Discrete logarithms and factoring.  In 35th Annual Symposium on Foundations of Computer Science, Santa Fe, New Mexico, USA, 20-22 November 1994 (1994), IEEE Computer Society, pp. 124–134.
  * [34] Truemper, K. Partial matroid representations.  European Journal of Combinatorics 5, 4 (1984), 377–394.
  * [35] Tutte, W. T. Connectivity in graphs.  Mathematical Expositions, No. 15. University of Toronto Press, Toronto, Ont.; Oxford University Press, London, 1966.
  * [36] Tutte, W. T. Connectivity in matroids.  Canadian J. Math. 18 (1966), 1301–1324.
  * [37] Welsh, D. J. A. Matroid theory.  L. M. S. Monographs, No. 8. Academic Press [Harcourt Brace Jovanovich, Publishers], London-New York, 1976.
  * [38] Whitney, H. On the abstract properties of linear dependence.  American Journal of Mathematics 57, 3 (1935), 509–533.
  * [39] Yao, A. C. Probabilistic computations: Toward a unified measure of complexity (extended abstract).  In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977 (1977), IEEE Computer Society, pp. 222–227.