11institutetext: ISTI–CNR, Pisa, Italy

# A Sound and Complete Refinement Relation for Non-reducible Modal Transition
Systems

Davide Basile

###### Abstract

Modal Transition Systems (MTS) are a well-known formalism that extend Labelled
Transition Systems (LTS) with the possibility of specifying necessary and
permitted behaviour. Whenever two MTS are not in modal refinement relation, it
could still be the case that the set of implementations of one MTS is included
in the set of implementations of the other. The challenge of devising an
alternative notion of modal refinement that is both sound and complete with
respect to the set of implementations, without disregarding valuable
implementations, remains open. In this paper, we address this challenge. We
introduce a subset of MTS called Non-reducible Modal Transition Systems
(NMTS), together with a novel refinement relation $\preceq_{n}$ for NMTS. We
show that $\preceq_{n}$ is sound and also complete with respect to its set of
implementations. We illustrate through examples how the additional constraints
imposed by NMTS are necessary for achieving completeness. Furthermore, we
discuss a property holding for NMTS whose implementations are non-
deterministic. We show that any implementation obtained through $\preceq_{m}$
but disregarded by $\preceq_{n}$ is violating this property.

##  1 Introduction

Modal Transition Systems (MTS) [13] extend Labelled Transition Systems (LTS)
[9] by distinguishing two types of transitions, meant to describe necessary
and optional behaviour in a system specification by means of transitions that
must _necessarily_ be implemented and transitions that may _optionally_ be
implemented. MTS come with a concept of _refinement_ , which represents a step
of the design process, namely the one in which some optional behaviour is
discarded while other optional behaviour becomes necessary. Stepwise
refinement of an MTS eventually results in an _implementation_ , which is an
LTS in which no further refinement is possible. Refinement of MTS is critical
for enabling formal reasoning on the correctness of a system’s design and
implementation, by enabling gradually refining an abstract specification into
a concrete one, ensuring that each step is correct. MTS are a well-known
specification theory and significant advances have been made so far [1, 10].

It is known that the (modal) refinement of MTS is not complete (cf., e.g.,
[12]). In other words, there are cases in which two MTS are not in a
refinement relation although the set of implementations of one MTS is included
in the set of implementations of the other MTS (this relation is known as
thorough refinement). Furthermore, while determining MTS refinement can be
computed in polynomial time, determining thorough refinement of MTS requires
EXPTIME [7]. In [12], the problem of proposing an alternative notion of modal
refinement that is both sound and complete with respect to its set of
implementations is left open [12]. An important aspect is to argue that the
considered set of implementations is also interesting from a practical point
of view (i.e., no valuable implementation is disregarded).

In this paper, we address this long-standing challenge by proposing a subset
of MTS, called _Non-reducible Modal Transition Systems_ (NMTS) together with
their alternative notion of modal refinement $\preceq_{n}$ that is both sound
and complete with respect to its set of implementations. A fundamental insight
behind NMTS is that states non-deterministically reachable through the
execution of identical sequences of actions are related. Specifically, the
outgoing transitions sharing the same action label also share the same
modality. Furthermore, when a refinement step deactivates one optional
transition, this leads to the deactivation of all other transitions that share
the same label from all other related (source) states.

The contributions of this paper are:

  1. 1.

we introduce NMTS, a subset of MTS. In NMTS, the transitions sharing the same
action label are constrained to also share the same modality whenever they are
reachable by the same sequence of actions;

  2. 2.

we equip NMTS with an alternative notion of modal refinement, called NMTS
refinement. The refinement of NMTS is derived from modal refinement by
imposing an additional constraint on the optional transitions of the system to
be refined;

  3. 3.

we provide different examples of MTS instances that fail to meet the
requisites for being either NMTS or refinements of NMTS. These examples show
that the constraints imposed by NMTS and their refinement are necessary to
achive a sound and complete refinement relation;

  4. 4.

we formally prove the soundness (Theorem 3.2) and completeness (Theorem 3.3)
of NMTS refinement;

  5. 5.

we introduce the _non-reducible non-determinism_ property concerning optional,
non-deterministic actions. This non-determinism is inherent in such actions
and should be preserved in any implementation where the action remains active.
All implementations accepted by the standard MTS refinement, but discarded by
the NMTS refinement, are showed to be implementations violating the non-
reducible non-determinism property.

### Overview

Section 2 introduces background on MTS and modal refinement. Section 3
presents Non-reducible MTS (NMTS) and their refinement, proving that NMTS
refinement is both sound and complete. Section 4 discusses the property of
non-reducible non-determinism, showing that the implementations discarded by
NMTS refinement but accepted by modal refinement are violating this property.
Section 5 discusses the related work, while Section 6 concludes the paper and
discusses future work.

##  2 Background

We start by discussing some background on MTS. The standard definition of MTS
accounts for two sets of transitions, _permitted_ (or _may_) transitions,
denoted by $\Delta_{\Diamond}$, and _necessary_ (or _must_) transitions,
denoted by $\Delta_{\Box}$, such that
$\Delta_{\Box}\subseteq\Delta_{\Diamond}$, i.e., all (necessary) transitions
are permitted. A transition $(q,a,q^{\prime})\\!\in\\!\Delta_{\Diamond}$ is
also denoted as $q\xrightarrow{a}_{\Diamond}q^{\prime}$ and likewise
$q\xrightarrow{a}_{\Box}q^{\prime}$ if
$(q,a,q^{\prime})\\!\in\\!\Delta_{\Box}$. The reader may be misled to think
that $q\xrightarrow{a}_{\Diamond}q^{\prime}$ excludes
$q\xrightarrow{a}_{\Box}q^{\prime}$, and vice versa that
$q\xrightarrow{a}_{\Box}q^{\prime}$ excludes
$q\xrightarrow{a}_{\Diamond}q^{\prime}$. However, the first statement is not
always true and the second is always false, since
$\Delta_{\Box}\\!\subseteq\\!\Delta_{\Diamond}$. For our purpose, it is
irrelevant to indicate that a transition is permitted. For the sake of
simplifying the presentation, we thus opt for a slightly revised definition of
MTS, where we partition the set of transitions into _optional_ and _necessary_
transitions, and no longer indicate the fact that all transitions are
_permitted_.

######  Definition 1 (MTS)

A _Modal Transition System (MTS)_ $S$ is a 5-tuple
$S=(Q,A,\overline{q},\Delta_{\scalebox{1.1}{$\circ$}},\Delta_{\Box})$, with
set $Q$ of states, set $A$ of actions, initial state $\overline{s}\in Q$, and
transition relation $\Delta\subseteq Q\times A\times Q$ partitioned into
_optional transitions_ , denoted by $\Delta_{\scalebox{1.1}{$\circ$}}$, and
_necessary transitions_ , denoted by $\Delta_{\Box}$, i.e.,
$\Delta_{{\scalebox{1.1}{$\circ$}}}\cap\Delta_{\Box}=\emptyset$. If
$(s,a,s^{\prime})\in\Delta_{\scalebox{1.1}{$\circ$}}$, then we also write
$s\xrightarrow{a}_{\scalebox{1.1}{$\circ$}}s^{\prime}$, and likewise we also
write $s\xrightarrow{a}_{\Box}s^{\prime}$ for
$(s,a,s^{\prime})\in\Delta_{\Box}$. We write $s\xrightarrow{a}s^{\prime}$ when
$(s,a,s^{\prime})\in\Delta$. We may omit the target state when it is
immaterial.

Note that the standard definition of MTS is
$(Q,A,\overline{q},\Delta_{\Diamond},\Delta_{\Box})$, where
$\Delta_{\Diamond}=\Delta_{\scalebox{1.1}{$\circ$}}\cup\Delta_{\Box}$. An LTS
is an MTS where $\Delta_{\scalebox{1.1}{$\circ$}}=\emptyset$. In the sequel,
the conversion from an MTS (and NMTS, cf. Section 3)
$(Q,A,\overline{q},\Delta_{\scalebox{1.1}{$\circ$}},\Delta_{\Box})$ with
$\Delta_{\scalebox{1.1}{$\circ$}}=\emptyset$ to an LTS
$(Q,A,\overline{q},\Delta)$ with $\Delta=\Delta_{\Box}$ is implicit. Moreover,
we will use subscripts or superscripts to indicate the origin of an element of
a tuple, i.e.,
$S=(Q_{S},A_{S},\overline{s},\Delta^{\scalebox{1.1}{$\circ$}}_{S},\Delta^{\Box}_{S})$.
We now define modal refinement of MTS.

######  Definition 2 (modal refinement)

An MTS $S$ is a _(modal) refinement_ of an MTS $T$, denoted by
$S\preceq_{m}T$, if and only if there exists a _refinement relation_ ${\cal
R}\subseteq Q_{S}\times Q_{T}$ such that $(\overline{s},\overline{t})\in{\cal
R}$ and for all $(s,t)\in{\cal R}$, the following holds:

  1. 1.

whenever $t\xrightarrow{a}_{{\Box}}t^{\prime}$, for some
$t^{\prime}\\!\in\\!Q_{T}$ and $a\\!\in\\!A_{T}$, then $a\\!\in\\!A_{S}$,
$\exists\,s^{\prime}\\!\in\\!Q_{S}:s\xrightarrow{a}_{{\Box}}s^{\prime}$, and
$(s^{\prime},t^{\prime})\in{\cal R}$, and

  2. 2.

whenever $s\xrightarrow{a}s^{\prime}$, for some $s^{\prime}\\!\in\\!Q_{S}$ and
$a\\!\in\\!A_{S}$, then $a\\!\in\\!A_{T}$,
$\exists\,t^{\prime}\\!\in\\!Q_{T}:t\xrightarrow{a}t^{\prime}$, and
$(s^{\prime},t^{\prime})\in{\cal R}$.

We also say that $S$ (modally) refines $T$ when $S\preceq_{m}T$.

Intuitively, $S$ modally refines $T$ if any necessary transition of $T$ can be
mimicked by a necessary transition of $S$, and every transition of $S$ can be
mimicked by a transition of $T$. The set of implementations of an MTS $S$,
written $Impl_{m}(S)$ is defined as the set of LTS $I$ such that
$I\preceq_{m}S$. Indeed, LTS cannot be further refined and are considered
implementations. In other words, every LTS refinement of an MTS $S$ is an
_implementation_ of $S$.

In [12], it is shown that $S\preceq_{m}T$ implies $Impl_{m}(S)\subseteq
Impl_{m}(T)$. In other words, modal refinement is _sound_ , i.e., each time an
MTS $S$ modally refines an MTS $T$, it follows that the set of implementations
of $T$ also contains the implementations of $S$. However, the contrary is not
true, i.e., modal refinement is not _complete_. Figure 1, reproduced from [7],
shows an example where the set of implementations of $T$ also contains the
implementations of $S$, but $S$ does not modally refine $T$.

$\overline{s}$$s_{1}$$a$$a$$\overline{t}$$t_{1}$$t_{2}$$a$$a$$a$ Figure 1:
From left two right, two MTS $S$ and $T$ such that $S\not\preceq_{m}T$ and
$Impl_{m}(S)\subseteq Impl_{m}(T)$, showing that modal refinement is not
complete (reproduced from [7]). Dashed arcs are used to depict optional
transitions ($\Delta_{\scalebox{1.1}{$\circ$}}$), while solid arcs depict
necessary transitions ($\Delta_{\Box}$).

##  3 Non-Reducible MTS Refinement

$\overline{s}$$s_{1}$$s_{2}$$s_{3}$$s_{4}$$s_{5}$$c$$c$$a$$a$$b$$\overline{t}$$t_{1}$$t_{2}$$t_{3}$$t_{4}$$t_{5}$$c$$c$$a$$a$$b$
Figure 2:  From left two right, two MTS $S$ and $T$ such that
$Impl_{m}(S)\subseteq Impl_{m}(T)$ but $S\not\preceq_{m}T$. Both $S$ and $T$
are not NMTS because $f^{\Box}_{S}(c)\cap
f^{\scalebox{1.1}{$\circ$}}_{S}(c)=\\{a\\}$ and $f^{\Box}_{T}(c)\cap
f^{\scalebox{1.1}{$\circ$}}_{T}(c)=\\{a\\}$

All examples documented in the literature (e.g., [7, 12]), which demonstrate
that modal refinement is not complete (e.g., Figure 1), involve the
utilization of a non-deterministic choice within the system under refinement.
This non-deterministic choice, such as the outgoing transitions from state
$\overline{t}$ in $T$ (as depicted in Figure 1), is subsequently eliminated in
the refined system, as it is the case in Figure 1 for system $S$.

Consider Figure 2. Similarly to Figure 1, it shows an example of two MTS $S$
and $T$ such that the implementations of $S$ are included into the
implementations of $T$, although $S$ and $T$ are not in modal refinement
relation. Figure 2 differs from Figure 1 (and all other similar examples in
the literature) in that it preserves the non-deterministic choices of $T$
within $S$. In $T$, the states $t_{1}$ and $t_{2}$ are reachable by executing
the same action $c$ and both exhibit outgoing transitions labeled as $a$.
Nonetheless, these two transitions do not share the same modality.

### NMTS

In this section, we identify the subset of MTS that exclusively discards
systems as those in Figure 2. Indeed, Figure 2 shows how such MTS instances
can result in a violation of completeness. We introduce _Non-reducible Modal
Transition Systems_ (NMTS). In NMTS, whenever a sequence of actions leads non-
deterministically to different states, all these states are interconnected by
the requirement that transitions associated with the same action must also
have the same modality.

In the following, let $w=a_{1}\ldots a_{n}$ be a sequence of actions in
$A^{*}$. The sequence of transitions $\overline{s}\xrightarrow{a_{1}}s_{1}$,
$s_{1}\xrightarrow{a_{2}}s_{2}$, $\ldots$, $s_{n-1}\xrightarrow{a_{n}}s$ is
written as $\overline{s}\xrightarrow{w}s$. Furthermore, we write
$\overline{s}\not\xrightarrow{w}s$ when it is not possible to reach $s$ from
$\overline{s}$ through the sequence of actions $w$.

######  Definition 3 (NMTS)

A _Non-reducible Modal Transition System (NMTS)_ $S$ is a 6-tuple
$S=(Q,A,\overline{q},\Delta,f_{\Box},f_{\scalebox{1.1}{$\circ$}})$, with set
$Q$ of states, set $A$ of actions, initial state $\overline{s}\in Q$, and
transition relation $\Delta\subseteq Q\times A\times Q$, where $\Delta$ is
partitioned into $\Delta_{\scalebox{1.1}{$\circ$}}$, the set of _optional_
transitions, and $\Delta_{\Box}$, the set of _necessary_ transitions, i.e.,
$\Delta_{{\scalebox{1.1}{$\circ$}}}\cap\Delta_{\Box}=\emptyset$. Functions
$f_{\Box}:A^{*}\mapsto 2^{A}$ and $f_{\scalebox{1.1}{$\circ$}}:A^{*}\mapsto
2^{A}$ are such that

  * •

for all $w\in A^{*}$ such that $\overline{s}\xrightarrow{w}s$ it holds that
$f_{\Box}(w)\cap f_{\scalebox{1.1}{$\circ$}}(w)=\emptyset$,

  * •

for all $w_{1},w_{2}\in A^{*}$ whenever $\overline{s}\xrightarrow{w_{1}}s$ and
$\overline{s}\xrightarrow{w_{2}}s$ then $f_{\Box}(w_{1})=f_{\Box}(w_{2})$,
$f_{\scalebox{1.1}{$\circ$}}(w_{1})=f_{\scalebox{1.1}{$\circ$}}(w_{2})$,

  * •

whenever $(s,a,s^{\prime})\in\Delta$ there exists $w\in A^{*}$ such that
$\overline{s}\xrightarrow{w}s$ and either

    * –

$a\in f_{\Box}(w)$, and in this case $(s,a,s^{\prime})\in\Delta_{\Box}$, or

    * –

$a\in f_{\scalebox{1.1}{$\circ$}}(w)$, and in this case
$(s,a,s^{\prime})\in\Delta_{\scalebox{1.1}{$\circ$}}$.

  * •

whenever $a\in f_{\Box}(w)\cup f_{\scalebox{1.1}{$\circ$}}(w)$ for some $w\in
A^{*}$ there exists a state $s\in Q_{S}$ such that
$\overline{s}\xrightarrow{w}s$ and $(s,a,s^{\prime})\in\Delta$ for some
$s^{\prime}\in Q_{S}$.

We write $f(w)$ to denote $f_{\Box}(w)\cup f_{\scalebox{1.1}{$\circ$}}(w)$.

Definition 3 enhances Definition 1 by including two functions, namely
$f_{\Box}$ and $f_{\scalebox{1.1}{$\circ$}}$. These functions serve a dual
purpose. Firstly, they establish a connection between states reachable through
the execution of identical sequences of actions. Secondly, they constraint
outgoing transitions from interconnected states that are sharing the same
label to also share the same modality.

Note that NMTS are a stric subset of MTS because in NMTS, for all $w\in A^{*}$
such that $\overline{s}\xrightarrow{w}s$, the condition $f_{\Box}(w)\cap
f_{\scalebox{1.1}{$\circ$}}(w)=\emptyset$ holds (as defined in Definition 3).
In contrast, within MTS, it is possible to have $f_{\Box}(w)\cap
f_{\scalebox{1.1}{$\circ$}}(w)\neq\emptyset$. If we were to remove this
constraint from Definition 3, then NMTS would become equivalent to MTS.

$\overline{s}$$s_{1}$$s_{2}$$s_{3}$$s_{4}$$s_{5}$$c$$c$$a$$a$$b$$\overline{t}$$t_{1}$$t_{2}$$t_{3}$$t_{4}$$t_{5}$$t_{6}$$c$$c$$a$$a$$a$$b$

.
$\overline{i}$$i_{1}$$i_{2}$$i_{3}$$i_{4}$$i_{5}$$c$$c$$a$$a$$b$

Figure 3:  Top row, from left two right, two NMTS $S$ and $T$ such that
$Impl_{m}(S)\subseteq Impl_{m}(T)$ but $S\not\preceq_{m}T$. Furthermore,
$S\not\preceq_{n}T$ and $Impl_{n}(S)\not\subseteq Impl_{n}(T)$. Bottom row, an
implementation $I$ such that $I\preceq_{n}S$, $I\not\preceq_{n}T$, but
$I\preceq_{m}T$

Consider Figure 3. In contrast to Figure 2, Figure 3 presents two systems,
denoted as $S$ and $T$, satisfying the conditions of Definition 3 (i.e., $S$
and $T$ are NMTS), and satisfying the conditions $Impl_{m}(S)\subseteq
Impl_{m}(T)$ and $S\not\preceq_{m}T$. Similarly to Figure 2, also in Figure 3
the non-deterministic choice in state $t_{1}$ in $T$ is maintained in state
$s_{1}$ in $S$. Figure 3 proves that, for achieving completeness, it is not
sufficient to constrain MTS to be NMTS. In the following, we will show that it
also necessary to introduce constraints on the refinement relation between
NMTS.

### NMTS refinement

We now introduce NMTS modal refinement $\preceq_{n}$. In contrast to standard
modal refinement, an additional condition is introduced, which applies to the
optional transitions within the system undergoing refinement. If an optional
transition is deactivated during the refinement process, it is required that
this deactivation applies uniformly to all other optional transitions sharing
the same action. This uniform deactivation rule applies across all source
states reachable through the same sequence of actions.

######  Definition 4 (NMTS refinement)

An NMTS $S$ is an NMTS refinement of another NMTS $T$, denoted as
$S\preceq_{n}T$, if there exists a refinement relation ${\cal R}\subseteq
Q_{S}\times Q_{T}$ between the states of the two systems such that
$(\overline{s},\overline{t})\in\mathcal{R}$ and for all $(s,t)\in\mathcal{R}$
there exists $w\in A^{*}_{S}$ such that $\overline{s}\xrightarrow{w}s$ and
$\overline{t}\xrightarrow{w}t$ and

  1. 1.

whenever $t\xrightarrow{a}_{\Box}t^{\prime}$ (for some $t^{\prime}\in Q_{T}$,
$a\in f^{\Box}_{T}(w)$), then $a\in f^{\Box}_{S}(w)$ and there exists a state
$s^{\prime}\in Q_{S}$ such that $s\xrightarrow{a}_{\Box}s^{\prime}$ and
$(s^{\prime},t^{\prime})\in{\cal R}$.

  2. 2.

whenever $t\xrightarrow{a}_{{\scalebox{1.1}{$\circ$}}}t^{\prime}$ (for some
$t^{\prime}\in Q_{T}$, $a\in f^{\scalebox{1.1}{$\circ$}}_{T}(w)$), then one of
the following holds:

     * •

$a\not\in f_{S}(w)$

     * •

$a\in f_{S}(w)$ and there exists a state $s^{\prime}\in Q_{S}$ such that
$s\xrightarrow{a}s^{\prime}$ and $(s^{\prime},t^{\prime})\in{\cal R}$.

  3. 3.

whenever $s\xrightarrow{a}s^{\prime}$ (for some $s^{\prime}\in Q_{S}$, $a\in
f_{S}(w)$), then $a\in f_{T}(w)$, and there exists a state $t^{\prime}\in
Q_{T}$ such that $t\xrightarrow{a}t^{\prime}$ and
$(s^{\prime},t^{\prime})\in{\cal R}$.

$\overline{i}$$i_{1}$$i_{2}$$i_{3}$$i_{4}$$i_{5}$$c$$c$$a$$a$$b$$\overline{i}^{\prime}$$i_{1}^{\prime}$$i_{2}^{\prime}$$i_{3}^{\prime}$$i_{4}^{\prime}$$c$$c$$a$$a$
Figure 4:  Two LTS $I$ and $I^{\prime}$ both implementations of the MTS $S$
and $T$ of Figure 2. The set $Impl_{n}(S)$ contains all and only LTS that are
strongly bisimilar to either $I$ or $I^{\prime}$. It follows that
$Impl_{n}(S)\subseteq Impl_{n}(T)$, and $S\not\preceq_{n}T$ (under the
assumption that $\preceq_{n}$ is also applicable to MTS)

As discussed earlier, Figure 3 shows that the further constraint imposed by
Definition 3 is not sufficient to achieve completeness of modal refinement.
Figure 2 and Figure 4 show that the additional constraint imposed by
Definition 4 on the refinement relation, when considered independently, is
also not sufficient to achieve completeness. Indeed, if we switch
$\preceq_{m}$ with $\preceq_{n}$ in Figure 2, as showed in Figure 4, it would
still hold that $Impl_{n}(S)\subseteq Impl_{n}(T)$ and $S\not\preceq_{n}T$,
because $S$ and $T$ are not NMTS. In other words, the example in Figure 2
proves that if non-deterministic MTS do not meet the criteria to be classified
as NMTS, then it is possible to build an example, as the one in Figure 2,
showing that both modal refinement and NMTS refinement are not complete.

In summary, the examples in Figure 2 and Figure 3 show that the constraints on
MTS and their refinement provided by Definition 3 and Definition 4 are both
required to achieve completeness. By either dropping the constraints on MTS
(i.e., Definition 3) or on their refinement (i.e., Definition 4), it is
possible to demonstrate that the resulting refinement relation is not
complete. In Theorem 3.3, we will prove that the constraints imposed by
Definition 3 and Definition 4 are also sufficient to achieve completeness of
the refinement relation.

$\overline{s}$$s_{1}$$s_{2}$$s_{3}$$a$$b$$a$$\overline{t}$$t_{1}$$t_{2}$$a$$b$
Figure 5: Two MTS $S$ and $T$ such that $S\preceq_{m}T$, $S\not\preceq_{n}T$.
Furthermore, $T\preceq_{m}S$ and $T\not\preceq_{n}S$. In both directions,
$\overline{s}\xrightarrow{a}_{\scalebox{1.1}{$\circ$}}s_{2}$,
$\overline{t}\xrightarrow{a}_{\scalebox{1.1}{$\circ$}}t_{1}$,
$t_{1}\xrightarrow{b}_{\scalebox{1.1}{$\circ$}}t_{2}$, $b\in f_{S}(a)$ and
$s_{2}\not\xrightarrow{b}$

Figure 5 depicts another example showcasing the differences between
$\preceq_{m}$ and $\preceq_{n}$. Consider the LTS $I_{T}$ obtained by
switching all transitions of $T$ (in Figure 5) to must. Clearly,
$I_{T}\preceq_{n}T$, but $I_{T}\not\preceq_{n}S$ (note that this is not true
for the case of $\preceq_{m}$).

Due to the coinductive nature of Definition 3, similarly to the complexity of
deciding modal refinement or strong bisimulation, also the complexity of
deciding an NMTS refinement is polynomial, provided that the input includes
the functions $f_{\Box}$ and $f_{\scalebox{1.1}{$\circ$}}$.

### Remark

Note that as an alternative characterisation, the condition outlined in
Definition 3 (namely, $f_{\Box}(w)\cap
f_{\scalebox{1.1}{$\circ$}}(w)\neq\emptyset$) can be omitted, at the cost of
modifying the refinement relation $\preceq_{n}$ to a new form, call it
$\preceq_{n}^{\prime}$, modified as follows. In $\preceq_{n}^{\prime}$,
whenever $a\in f_{\Box}(w)\cap f_{\scalebox{1.1}{$\circ$}}(w)$ for some $a\in
A$, all transitions reachable via $w$ and labeled with $a$ are treated as
necessary, even if they are declared optional. We argue that while this
alternative characterisation would enable the inclusion of all MTS and not a
limited subset, it would introduce ambiguity. This is because it would permit
to denote a necessary transition $\delta$ as optional whenever there exists
another necessary transition $\delta^{\prime}$ with the same action as
$\delta$ and reachable through the execution of the same sequence of actions.
Therefore, whenever in an MTS it holds that $a\in f_{\Box}(w)\cap
f_{\scalebox{1.1}{$\circ$}}(w)$ for some $a\in A$, rather than considering all
transitions reachable via $w$ and labeled with $a$ as necessary, even if they
are denoted as optional, we opt to exclude such MTS from consideration.

We show that $\preceq_{n}$ is a conservative extension of $\preceq_{m}$.

###### Theorem 3.1

Let $S$ and $T$ be two NMTS. If $S\preceq_{n}T$ then $S\preceq_{m}T$.

###### Proof

Let $\mathcal{R}$ be proving $S\preceq_{n}T$. It holds that
$(\overline{s},\overline{t})\in\mathcal{R}$. Furthermore, for any
$(s,t)\in\mathcal{R}$, by hypothesis there exists some $w\in A^{*}_{S}$ such
that $\overline{s}\xrightarrow{w}s$ and $\overline{t}\xrightarrow{w}t$.
Furthermore:

  * •

whenever $t\xrightarrow{a}_{\Box}t^{\prime}$, it holds that $a\in
f^{\Box}_{S}(w)$ (therefore $a\in A_{S}$), $s\xrightarrow{a}_{\Box}s^{\prime}$
and $(s^{\prime},t^{\prime})\in\mathcal{R}$;

  * •

whenever $s\xrightarrow{a}s^{\prime}$ it holds that $a\in f_{T}(w)$ (therefore
$a\in A_{T}$), $t\xrightarrow{a}t^{\prime}$ and it holds that
$(s^{\prime},t^{\prime})\in\mathcal{R}$.∎

Consider Figure 3. Since $S\not\preceq_{m}T$, by Theorem 3.1 it follows that
$S\not\preceq_{n}T$.

We now show the relations between the functions $f^{\Box}$ and
$f^{\scalebox{1.1}{$\circ$}}$ of two systems in NMTS refinement relation.

###### Lemma 1

Let $S$ and $T$ be two NMTS such that $S\preceq_{n}T$. For all $w\in
A^{*}_{S}$ such that $\overline{s}\xrightarrow{w}s$, it holds that
$f^{\scalebox{1.1}{$\circ$}}_{S}(w)\subseteq
f^{\scalebox{1.1}{$\circ$}}_{T}(w)$, $f^{\Box}_{T}(w)\subseteq
f^{\Box}_{S}(w)$ and $f^{\Box}_{S}(w)\setminus f^{\Box}_{T}(w)\subseteq
f^{\scalebox{1.1}{$\circ$}}_{T}(w)\setminus
f^{\scalebox{1.1}{$\circ$}}_{S}(w)$.

###### Proof

Each action $A_{S}$ appears in some transition in $\Delta_{S}$ (there are no
redundant elements in $A_{S}$). By hypothesis $S\preceq_{n}T$ and by point 3
of Definition 4 it holds that $A_{S}\subseteq A_{T}$ (we assume that all
states are reachable, i.e., there are no redundant states). We first prove
that for all $w\in A^{*}_{S}$ such that $\overline{s}\xrightarrow{w}s$ it
holds $f^{\Box}_{T}(w)\subseteq f^{\Box}_{S}(w)$. By contradiction, assume
that there exists some $w\in A^{*}_{S}$ such that
$\overline{s}\xrightarrow{w}s$ and $a\in f^{\Box}_{T}(w)\setminus
f^{\Box}_{S}(w)$. Hence, by Definition 3 there exists a transition
$\delta\in\Delta^{\Box}_{T}$ labelled with $a$ for some $t\in Q_{T}$ source
state of $\delta$ such that $\overline{t}\xrightarrow{w}t$. By hypothesis,
there must be some $s\in Q_{S}$ such that $(s,t)\in\mathcal{R}$, where
$\mathcal{R}$ is the NMTS refinement relation for $S\preceq_{n}T$. By
Definition 4 it holds that $s\xrightarrow{a}_{\Box}s^{\prime}\in\Delta_{S}$
and $a\in f^{\Box}_{S}(w)$. We reached a contradiction.

We now show that for all $w\in A^{*}_{S}$ such that
$\overline{s}\xrightarrow{w}s$ it holds
$f^{\scalebox{1.1}{$\circ$}}_{S}(w)\subseteq
f^{\scalebox{1.1}{$\circ$}}_{T}(w)$. By contradiction, assume that there
exists some $w\in A^{*}_{S}$ with $\overline{s}\xrightarrow{w}s$ and an action
$a\in f^{\scalebox{1.1}{$\circ$}}_{S}(w)\setminus
f^{\scalebox{1.1}{$\circ$}}_{T}(w)$. Hence, there exists a transition
$\delta\in\Delta_{\scalebox{1.1}{$\circ$}}^{S}$ reachable via $w$ and labelled
with $a$. Let $s$ be the source state of $\delta$. By Definition 4, since
$A_{S}\subseteq A_{T}$, for some $t\in Q_{T}$ it holds that
$\overline{t}\xrightarrow{w}t$ and $(s,t)\in\mathcal{R}$. By Definition 4 it
holds that $t\xrightarrow{a}t^{\prime}\in\Delta_{T}$. Since $a\not\in
f^{\scalebox{1.1}{$\circ$}}_{T}(w)$, it must be the case that $a\in
f^{\Box}_{T}(w)$, hence $a\in f^{\Box}_{S}(w)$. We reached a contradiction.

Finally, we prove that for all $w\in A^{*}_{S}$ such that
$\overline{s}\xrightarrow{w}s$ it holds $f^{\Box}_{S}(w)\setminus
f^{\Box}_{T}(w)\subseteq f^{\scalebox{1.1}{$\circ$}}_{T}(w)\setminus
f^{\scalebox{1.1}{$\circ$}}_{S}(w)$. Let $a\in f^{\Box}_{S}(w)\setminus
f^{\Box}_{T}(w)$. Since $f^{\Box}_{S}(w)\cap
f^{\scalebox{1.1}{$\circ$}}_{S}(w)=\emptyset$, we have $a\not\in
f^{\scalebox{1.1}{$\circ$}}_{S}(w)$. Moreover, there exists some transition
$s\xrightarrow{a}s^{\prime}\in\Delta_{S}$ with $\overline{s}\xrightarrow{w}s$.
By Definition 4, for some $t\in Q_{T}$ it holds that
$\overline{t}\xrightarrow{w}t$ , $(s,t)\in\mathcal{R}$,
$t\xrightarrow{a}t^{\prime}\in\Delta_{T}$, $a\in f_{T}(w)$ and
$(s^{\prime},t^{\prime})\in\mathcal{R}$. Since $a\in f^{\Box}_{S}(w)\setminus
f^{\Box}_{T}(w)$, it must be the case that $a\in
f^{\scalebox{1.1}{$\circ$}}_{T}(w)$. ∎

We now show that, similarly to $\preceq_{m}$, also $\preceq_{n}$ is a
preorder.

###### Lemma 2

The relation $\preceq_{n}$ is a preorder.

###### Proof

Let $S$ be an NMTS. Clearly, $\\{(s,s)\mid s\in Q_{S}\\}$ shows that
$S\preceq_{n}S$. Let $T$ and $U$ be two NMTS such that $S\preceq_{n}T$ and
$T\preceq_{n}U$.

We now prove that the relation
$\mathcal{R}=\\{(s,u)\mid(s,t)\in\mathcal{R}_{S\preceq_{n}T},(t,u)\in\mathcal{R}_{T\preceq_{n}U},t\in
Q_{T}\\}$ shows that $S\preceq_{n}U$. Clearly
$(\overline{s},\overline{u})\in\mathcal{R}$. Whenever $(s,u)\in\mathcal{R}$
for some $w\in A^{*}_{S}$ where $\overline{s}\xrightarrow{w}s$ and
$\overline{u}\xrightarrow{w}u$ then:

  * •

if $u\xrightarrow{a}_{\Box}u^{\prime}$, by
$(t,u)\in\mathcal{R}_{T\preceq_{n}U}$ it holds
$t\xrightarrow{a}_{\Box}t^{\prime}$ and
$(t^{\prime},u^{\prime})\in\mathcal{R}_{T\preceq_{n}U}$. By
$(s,t)\in\mathcal{R}_{S\preceq_{n}T}$ it holds
$s\xrightarrow{a}_{\Box}s^{\prime}$, $(s^{\prime},t^{\prime})\in
R_{S\preceq_{n}T}$. Therefore, $(s^{\prime},u^{\prime})\in\mathcal{R}$;

  * •

if $u\xrightarrow{a}_{\scalebox{1.1}{$\circ$}}u^{\prime}$ by
$(t,u)\in\mathcal{R}_{T\preceq_{n}U}$ we distinguish two cases:

    * –

either $a\not\in f_{T}(w)$. By $(s,t)\in\mathcal{R}_{S\preceq_{n}T}$ and Lemma
1 (i.e., $f_{S}(w)\subseteq f_{T}(w)$), it follows $a\not\in f_{S}(w)$;

    * –

$a\in f_{T}(w)$, $t\xrightarrow{a}t^{\prime}$ and
$(t^{\prime},u^{\prime})\in\mathcal{R}_{T\preceq_{n}U}$. By
$(s,t)\in\mathcal{R}_{S\preceq_{n}T}$ either, $a\not\in f_{S}(w)$ or $a\in
f_{S}(w)$ $s\xrightarrow{a}s^{\prime}$,
$(s^{\prime},t^{\prime})\in\mathcal{R}_{S\preceq_{n}T}$ and
$(s^{\prime},u^{\prime})\in\mathcal{R}$;

  * •

if $s\xrightarrow{a}s^{\prime}$ by $(s,t)\in\mathcal{R}_{S\preceq_{n}T}$ it
follows that $t\xrightarrow{a}t^{\prime}$ and
$(s^{\prime},t^{\prime})\in\mathcal{R}_{S\preceq_{n}T}$. By
$(t,u)\\!\in\\!\mathcal{R}_{T\preceq_{n}U}$ it follows that
$u\xrightarrow{a}u^{\prime}$ and
$(t^{\prime},u^{\prime})\\!\in\\!\mathcal{R}_{T\preceq_{n}U}$. Hence
$(s^{\prime},u^{\prime})\\!\in\\!\mathcal{R}$.

∎

Given an MTS $S$ we denote with $Impl_{n}(S)$ the set of LTS $I$ such that
$I\preceq_{n}S$. The soundness of $\preceq_{n}$ is straightforward.

######  Theorem 3.2 ($\preceq_{n}$ soundness)

Let $S$ and $T$ be two MTS. If $S\preceq_{n}T$ then $Impl_{n}(S)\subseteq
Impl_{n}(T)$.

###### Proof

Pick an implementation $I\preceq_{n}S$, since $S\preceq_{n}T$ by transitivity
$I\preceq_{n}T$. ∎

Before proceeding to prove the completeness of $\preceq_{n}$, we establish two
auxiliary lemmata. The first lemma demonstrates that a refinement can occur by
either asserting (i.e., switching to necessary) or removing a set of optional
transitions that are reachable through the same sequence of actions and share
the same action label.

###### Lemma 3

Let $S$ be an NMTS and let
$S^{\prime}=(Q_{S^{\prime}},A_{S^{\prime}},\overline{s},\Delta_{S^{\prime}},f^{\Box}_{S^{\prime}},f^{\scalebox{1.1}{$\circ$}}_{S^{\prime}})$
be obtained from $S$ as follows:

  * •

there exists a sequence $w\in A^{*}_{S}$ such that
$\overline{s}\xrightarrow{w}s$ for some $s\in Q_{S}$ and

  * •

$\forall w^{\prime}\in A^{*}_{S}$ such that $(i)\exists s^{\prime}\in
Q_{S}.\overline{s}\xrightarrow{w}s^{\prime}$ and $(ii)$
$\forall\\!s^{\prime\prime}\\!\in\\!Q_{S}.\overline{s}\\!\not\xrightarrow{w}\\!s^{\prime\prime}\vee\overline{s}\\!\not\xrightarrow{w^{\prime}}\\!s^{\prime\prime}$,
it holds that $f^{\Box}_{S^{\prime}}(w^{\prime})=f^{\Box}_{S}(w^{\prime})$ and
$f^{\scalebox{1.1}{$\circ$}}_{S^{\prime}}(w^{\prime})=f^{\scalebox{1.1}{$\circ$}}_{S}(w^{\prime})$
and

  * •

there exists $a\in f^{\scalebox{1.1}{$\circ$}}_{S}(w)$ such that $a\not\in
f^{\scalebox{1.1}{$\circ$}}_{S^{\prime}}(w)$ and either $a\in
f^{\Box}_{S^{\prime}}(w)$ (assert action) or $a\not\in
f^{\Box}_{S^{\prime}}(w)$ (remove action).

Furthermore $Q_{S^{\prime}}=\\{s\mid s\in Q_{S},s\text{ is reachable in
}S^{\prime}\\}$ and $A_{S^{\prime}}=\\{a\mid a\in
A_{S},\linebreak(s,a,s^{\prime})~{}\in~{}\Delta_{S^{\prime}}\text{ for some
}s,s^{\prime}\in Q_{S^{\prime}}\\}$. It holds that $S^{\prime}\preceq_{n}S$.

###### Proof

Let $\mathcal{R}=\\{(s,s)\mid s\in Q_{S^{\prime}}\\}$. We show that
$\mathcal{R}$ proves $S^{\prime}\preceq_{n}S$. Trivially
$(\overline{s},\overline{s})$. Furthermore, for all couples
$(s,s)\in\mathcal{R}$ such that $\overline{s}\not\xrightarrow{w}s$ the
outgoing transitions of $s$ are identical in $S$ and $S^{\prime}$ and the
conditions in Definition 4 hold trivially. When $(s,s)\in\mathcal{R}$ is such
that $\overline{s}\xrightarrow{w}s$ it holds that:

  * •

whenever $s\xrightarrow{a^{\prime}}_{\Box}s^{\prime}\in\Delta_{S}$
($a^{\prime}\in f^{\Box}_{S}(w)$), we need to show that $a\neq a^{\prime}$,
otherwise, in case of remove, we would have $a\not\in
f^{\Box}_{S^{\prime}}(w)$. Since $a\in f^{\scalebox{1.1}{$\circ$}}_{S}(w)$ and
$f^{\scalebox{1.1}{$\circ$}}_{S}(w)\cap f^{\Box}_{S}(w)=\emptyset$, it follows
that $a\neq a^{\prime}$, $a^{\prime}\in f^{\Box}_{S^{\prime}}(w)$,
$s\xrightarrow{a^{\prime}}_{\Box}s^{\prime}\in\Delta_{S^{\prime}}$ and
$(s^{\prime},s^{\prime})\in\mathcal{R}$;

  * •

whenever
$s\xrightarrow{a^{\prime}}_{\scalebox{1.1}{$\circ$}}s^{\prime}\in\Delta_{S}$
($a^{\prime}\in f^{\scalebox{1.1}{$\circ$}}_{S}(w)$), if $a\neq a^{\prime}$
then $a\in f^{\scalebox{1.1}{$\circ$}}_{S^{\prime}}(w)$,
$s\xrightarrow{a^{\prime}}_{\scalebox{1.1}{$\circ$}}s^{\prime}\in\Delta_{S^{\prime}}$
and $(s^{\prime},s^{\prime})\in\mathcal{R}$. Otherwise, $a\not\in
f^{\scalebox{1.1}{$\circ$}}_{S^{\prime}}(w)$;

  * •

whenever $s\xrightarrow{a^{\prime}}s^{\prime}\in\Delta_{S^{\prime}}$
($a^{\prime}\in f_{S}(w)$), then $a^{\prime}\in f_{S}(w)$,
$s\xrightarrow{a^{\prime}}s^{\prime}\in\Delta_{S}$ and
$(s^{\prime},s^{\prime})\in\mathcal{R}$. ∎

The second lemma shows the conditions under which it is possible to switch a
set of necessary transitions (whose source state is reachable by the same
sequence of actions) to optional ones, whilst preserving NMTS refinement.

###### Lemma 4

Let $S$ and $T$ be two NMTS such that $S\\!\preceq_{n}\\!T$, where for some
$s\in Q_{S}$ there exists a sequence
$w\\!\in\\!A^{*}_{S}.\overline{s}\xrightarrow{w}s$ such that
$a\\!\in\\!f^{\Box}_{S}(w)\setminus f^{\Box}_{T}(w)$. It holds
$S^{\prime}\\!\preceq_{n}\\!T$, where
$S^{\prime}\\!=\\!(Q_{S},A_{S},\overline{s},\Delta_{S^{\prime}},f^{\Box}_{S^{\prime}},f^{\scalebox{1.1}{$\circ$}}_{S^{\prime}})$
and:

  * •

$\forall w^{\prime}\in A^{*}_{S}$ such that $(i)\exists s^{\prime}\in
Q_{S}.\overline{s}\xrightarrow{w}s^{\prime}$ and $(ii)$
$\forall\\!s\\!\in\\!Q_{S}.\overline{s}\\!\not\xrightarrow{w}\\!s\vee\overline{s}\\!\not\xrightarrow{w^{\prime}}\\!s$,
it holds that $f^{\Box}_{S^{\prime}}(w^{\prime})=f^{\Box}_{S}(w^{\prime})$ and
$f^{\scalebox{1.1}{$\circ$}}_{S^{\prime}}(w^{\prime})=f^{\scalebox{1.1}{$\circ$}}_{S}(w^{\prime})$
and

  * •

$f^{\Box}_{S^{\prime}}(w)=f^{\Box}_{S}(w)\setminus\\{a\\}$ and
$f^{\scalebox{1.1}{$\circ$}}_{S^{\prime}}(w)=f^{\scalebox{1.1}{$\circ$}}_{S}(w)\cup\\{a\\}$.

###### Proof

Firstly, since $S\preceq_{n}T$, by Lemma 1, for all $w^{\prime}\in A^{*}_{S}$
such that $\overline{s}\xrightarrow{w^{\prime}}s$, it holds
$f^{\Box}_{S}(w^{\prime})\setminus f^{\Box}_{T}(w^{\prime})\subseteq
f^{\scalebox{1.1}{$\circ$}}_{T}(w^{\prime})\setminus
f^{\scalebox{1.1}{$\circ$}}_{S}(w^{\prime})$. Therefore, by hypothesis, $a\in
f^{\scalebox{1.1}{$\circ$}}_{T}(w)$. Assume that $\mathcal{R}$ proves
$S\preceq_{n}T$. Then, we show that the relation $\mathcal{R}$ also proves
$S^{\prime}\preceq_{n}T$. Firstly,
$(\overline{s},\overline{t})\in\mathcal{R}$. For all $(s,t)\in\mathcal{R}$
such that $\overline{s}\not\xrightarrow{w}s$ and
$\overline{t}\not\xrightarrow{w}t$, we have that the outgoing transitions of
$s$ in $S^{\prime}$ are identical to those in $S$, and the conditions in
Definition 4 hold trivially. Otherwise, for all $(s,t)\in\mathcal{R}$ such
that $\overline{s}\xrightarrow{w}s$ and $\overline{t}\xrightarrow{w}t$ it
holds:

  1. 1.

Whenever $t\xrightarrow{a^{\prime}}t^{\prime}\in\Delta_{T}$:

    1. (a)

if $a^{\prime}\in f^{\Box}_{T}(w)$, by hypothesis it holds $a^{\prime}\neq a$.
Since $(s,t)\in\mathcal{R}$, it holds $a^{\prime}\in
f^{\Box}_{S^{\prime}}(w)$,
$s\xrightarrow{a^{\prime}}_{\Box}s^{\prime}\in\Delta_{S^{\prime}}$ and
$(s^{\prime},t^{\prime})\in\mathcal{R}$;

    2. (b)

if $a^{\prime}\in f^{\scalebox{1.1}{$\circ$}}_{T}(w)$ and $a^{\prime}\in
f_{S}(w)$, then $a^{\prime}\in f_{S^{\prime}}(w)$ and by
$(s,t)\in\mathcal{R}$, it holds
$s\xrightarrow{a^{\prime}}s^{\prime}\in\Delta_{S^{\prime}}$ and
$(s^{\prime},t^{\prime})\in\mathcal{R}$;

    3. (c)

if $a^{\prime}\in f^{\scalebox{1.1}{$\circ$}}_{T}$ and $a^{\prime}\not\in
f_{S}(w)$, then by construction also $a^{\prime}\not\in f_{S^{\prime}}(w)$;

  2. 2.

whenever $s\xrightarrow{a^{\prime}}s^{\prime}\in\Delta_{S^{\prime}}$, then by
construction $a^{\prime}\in f_{S}(w)$, thus
$s\xrightarrow{a^{\prime}}s^{\prime}\in\Delta_{S}$, and since
$(s,t)\in\mathcal{R}$, we have
$t\xrightarrow{a^{\prime}}t^{\prime}\in\Delta_{T}$ and
$(s^{\prime},t^{\prime})\in\mathcal{R}$. ∎

We are now ready to prove the main result of this section, the completeness of
$\preceq_{n}$.

######  Theorem 3.3 ($\preceq_{n}$ completeness)

$Impl_{n}(S)\subseteq Impl_{n}(T)$ implies $S\preceq_{n}T$.

###### Proof

Let
$I_{S}=(Q_{S},A_{S},\overline{s},\Delta_{I_{S}},f^{\scalebox{1.1}{$\circ$}}_{I_{S}},f^{\Box}_{I_{S}})$,
where for all $w\in A^{*}_{S}.f^{\Box}_{I_{S}}(w)=f_{S}(w)$,
$f^{\scalebox{1.1}{$\circ$}}_{I_{S}}=\emptyset$ be the implementation obtained
from $S$ by repeatedly applying until exhaustion the assert operation from
Lemma 3. By Lemma 3, $I_{S}\preceq_{n}S$, therefore $I_{S}\in Impl_{n}(S)$. By
hypothesis, $I_{S}\preceq_{n}T$. Note that $I_{S}$ is an implementation since
$\Delta^{\scalebox{1.1}{$\circ$}}_{I_{S}}=\emptyset$, whilst
$\Delta^{\Box}_{I_{S}}=\Delta_{S}$.

Let
$I_{S}^{\prime}=(Q_{S}^{\prime},A_{S}^{\prime},\overline{s},\Delta_{I_{S^{\prime}}},f^{\scalebox{1.1}{$\circ$}}_{I_{S}^{\prime}},f^{\Box}_{I_{S}^{\prime}})$
be the implementation computed from $S$ by repeatedly applying until
exhaustion the remove operation from Lemma 3. It holds that for all $w\in
A^{*}_{S}$, $f^{\Box}_{I_{S}^{\prime}}(w)=f^{\Box}_{S}(w)$,
$f^{\scalebox{1.1}{$\circ$}}_{I_{S}^{\prime}}(w)=\emptyset$,
$\Delta^{\scalebox{1.1}{$\circ$}}_{I_{S^{\prime}}}=\emptyset$,
$\Delta^{\Box}_{I_{S^{\prime}}}=\Delta^{\Box}_{S}$. By Lemma 3, it holds that
$I_{S}^{\prime}\preceq_{n}S$, therefore $I_{S}^{\prime}\in Impl_{n}(S)$. By
hypothesis $I_{S}^{\prime}\preceq_{n}T$.

For any $w\in A^{*}_{S}$ such that $\overline{s}\xrightarrow{w}s$ by Lemma 1
and $f^{\Box}_{T}(w)\subseteq f^{\Box}_{I_{S}^{\prime}}(w)=f^{\Box}_{S}(w)$ it
holds $f^{\scalebox{1.1}{$\circ$}}_{S}(w)\cap f^{\Box}_{T}(w)=\emptyset$.

If for all $w\in A^{*}_{S}$ such that $\overline{s}\xrightarrow{w}s$ it holds
$f^{\scalebox{1.1}{$\circ$}}_{S}(w)=\emptyset$, then since
$f^{\scalebox{1.1}{$\circ$}}_{S}(w)\cap f^{\Box}_{S}(w)=\emptyset$ we have
that $S=I_{S}$ and the thesis follows. Hence, assume that for some $s\in
Q_{S}$ such that $\overline{s}\xrightarrow{w}s$, $w\in A^{*}_{S}$, it holds
$f^{\scalebox{1.1}{$\circ$}}_{S}(w)\neq\emptyset$. We perform two nested
iteration loops. In the external loop, we iterate on the states in the set
$P\\!=\\!\\{s\\!\mid\\!s\\!\in\\!Q_{S},w\\!\in\\!A^{*}_{S},\overline{s}\\!\xrightarrow{w}\\!s$,
$f^{\scalebox{1.1}{$\circ$}}_{S}(w)\\!\neq\\!\emptyset$ $\\}$. We start by
selecting an $s^{1}\in Q_{S}$ and $w^{1}\in A^{*}_{S}$ such that
$\overline{s}\xrightarrow{w^{1}}s^{1}$ and
$f^{\scalebox{1.1}{$\circ$}}_{S}(w^{1})\neq\emptyset$. In the internal loop,
for each selected state, we iterate on the actions $a\in
f^{\scalebox{1.1}{$\circ$}}_{S}(w^{1})$. We pick an action $a\in
f^{\scalebox{1.1}{$\circ$}}_{S}(w^{1})$, thus $a\not\in f^{\Box}_{T}(w^{1})$
and $a\in f^{\Box}_{I_{S}}(w^{1})$. From $I_{S}$, $T$, and $a$ by applying
Lemma 4 we obtain an NMTS
$S^{1}_{1}=(Q_{S},A_{S},\overline{s},\Delta_{S^{1}_{1}},f^{\Box}_{S^{1}_{1}},f^{\scalebox{1.1}{$\circ$}}_{S^{1}_{1}})$
such that for all $w^{\prime}$ with
$\overline{s}\not\xrightarrow{w^{\prime}}s^{1}$ it holds
$f^{\Box}_{S^{1}_{1}}(w^{\prime})=f^{\Box}_{I_{S}}(w^{\prime})$,
$f^{\scalebox{1.1}{$\circ$}}_{S^{1}_{1}}(w^{\prime})=f^{\scalebox{1.1}{$\circ$}}_{I_{S}}(w^{\prime})=\emptyset$.
Furthermore,
$f^{\Box}_{S^{1}_{1}}(w^{1})=f^{\Box}_{I_{S}}(w^{1})\setminus\\{a\\}$,
$f^{\scalebox{1.1}{$\circ$}}_{S^{1}_{1}}(w^{1})=\\{a\\}$. By Lemma 4, since
$I_{S}\preceq_{n}T$, $a\in f^{\Box}_{I_{S}}(w^{1})\setminus
f^{\Box}_{T}(w^{1})$, it holds $S^{1}_{1}\preceq_{n}T$.

We re-iterate (internal iteration) and pick the next action. From $S^{1}_{1}$,
$T$, and an action $b\in f^{\scalebox{1.1}{$\circ$}}_{S}(w^{1})$, $b\not\in
f^{\Box}_{T}(w^{1})$ such that $b\neq a$, hence $b\in
f^{\Box}_{S^{1}_{1}}(w^{1})$, we build an NMTS
$S^{2}_{1}=(Q_{S},A_{S},\overline{s},\Delta_{S^{2}_{1}},f^{\Box}_{S^{2}_{1}},f^{\scalebox{1.1}{$\circ$}}_{S^{2}_{1}})$
such that for all $w^{\prime}$ with
$\overline{s}\not\xrightarrow{w^{\prime}}s^{1}$ it holds
$f^{\Box}_{S^{2}_{1}}(w^{\prime})=f^{\Box}_{S^{1}_{1}}(w^{\prime})$,
$f^{\scalebox{1.1}{$\circ$}}_{S^{2}_{1}}(w^{\prime})=f^{\scalebox{1.1}{$\circ$}}_{S^{1}_{1}}(w^{\prime})$,
and $f^{\Box}_{S^{2}_{1}}(w^{1})=f^{\Box}_{S^{1}_{1}}(w^{1})\setminus\\{b\\}$,
$f^{\scalebox{1.1}{$\circ$}}_{S^{2}_{1}}(w^{1})=f^{\scalebox{1.1}{$\circ$}}_{S^{1}_{1}}(w^{1})\cup\\{b\\}=\\{a,b\\}$.
By Lemma 4, since $S^{1}_{1}\preceq_{n}T$, $b\in f^{\Box}_{S^{1}_{1}}(w^{1})$
and $b\not\in f^{\Box}_{T}(w^{1})$, it holds $S^{2}_{1}\preceq_{n}T$.

We re-iterate (internal iteration) for all actions in
$f^{\scalebox{1.1}{$\circ$}}_{S}(w^{1})$. We obtain an NMTS
$S^{n}_{1}=(Q_{S},A_{S},\overline{s},\Delta_{S^{n}_{1}},f^{\Box}_{S^{n}_{1}},f^{\scalebox{1.1}{$\circ$}}_{S^{n}_{1}})$
where $|f^{\scalebox{1.1}{$\circ$}}_{S}(w^{1})|=n$ such that
$f^{\Box}_{S^{n}_{1}}(w^{1})=f^{\Box}_{S}(w^{1})$,
$f^{\scalebox{1.1}{$\circ$}}_{S^{n}_{1}}(w^{1})=f^{\scalebox{1.1}{$\circ$}}_{S}(w^{1})$.

We repeat again the (external) iteration for all states in $P$. At the second
(external) iteration, we pick a state $s^{2}\in P$ and a sequence of actions
$w^{2}\in A_{S}^{*}$ such that $\overline{s}\xrightarrow{w^{2}}s^{2}$,
$f^{\scalebox{1.1}{$\circ$}}_{S}(w^{2})\neq\emptyset$ and
$\overline{s}\not\xrightarrow{w^{2}}s^{i}$ for all $i<2$. If this last
condition is not satisfied (i.e., for all $w^{2}\in A_{S}^{*}$ it holds that
$\overline{s}\xrightarrow{w^{2}}s^{i}$ for some $i<2$) then we skip this
iteration and continue with the next (the external counter is incremented
nonetheless). We pick an action $a\in f^{\scalebox{1.1}{$\circ$}}_{S}(w^{2})$,
thus $a\not\in f^{\Box}_{T}(w^{2})$ and $a\in
f^{\Box}_{S^{n}_{1}}(w^{2})=f^{\Box}_{I_{S}}(w^{2})$. From $S^{n}_{1}$, $T$,
and $a$ we build an NMTS
$S^{1}_{2}=(Q_{S},A_{S},\overline{s},\Delta_{S^{1}_{2}},f^{\Box}_{S^{1}_{2}},f^{\scalebox{1.1}{$\circ$}}_{S^{1}_{2}})$
such that for all $w^{\prime}$ with
$\overline{s}\not\xrightarrow{w^{\prime}}s^{2}$ it holds
$f^{\Box}_{S^{1}_{2}}(w^{\prime})=f^{\Box}_{S^{n}_{1}}(w^{\prime})$,
$f^{\scalebox{1.1}{$\circ$}}_{S^{1}_{2}}(w^{\prime})=f^{\scalebox{1.1}{$\circ$}}_{S^{n}_{1}}(w^{\prime})$,
and $f^{\Box}_{S^{1}_{2}}(w^{2})=f^{\Box}_{S^{n}_{1}}(w^{2})\setminus\\{a\\}$,
$f^{\scalebox{1.1}{$\circ$}}_{S^{1}_{2}}(w^{2})=\\{a\\}$. By Lemma 4, since
$S^{n}_{1}\preceq_{n}T$, $a\in f^{\Box}_{S^{n}_{1}}(w^{2})$ and $a\not\in
f^{\Box}_{T}(w^{2})$, it holds $S^{1}_{2}\preceq_{n}T$. At the end of the
second (external) iteration we obtain an NMTS $S^{m}_{2}$ where
$m=|f^{\scalebox{1.1}{$\circ$}}_{S}(w^{2})|$ such that
$f^{\Box}_{S^{m}_{2}}(w^{i})=f^{\Box}_{S}(w^{i})$,
$f^{\scalebox{1.1}{$\circ$}}_{S^{m}_{2}}(w^{i})=f^{\scalebox{1.1}{$\circ$}}_{S}(w^{i})$
for $i\in\\{1,2\\}$.

Every subsequent (external) iteration starts by reusing the last NMTS computed
at the previous (external) iteration. Let $o=|P|$ (recall that we incremented
the external counter also when skipping some element of $P$), and
$p=|f^{\scalebox{1.1}{$\circ$}}_{S}(w^{o})|$, where $w^{o}$ is the trace
selected at the last, $o$-th iteration of the procedure. The returned NMTS
$S^{p}_{o}=(Q_{S},A_{S},\overline{s},\Delta_{S^{p}_{o}},f^{\Box}_{S^{p}_{o}},f^{\scalebox{1.1}{$\circ$}}_{S^{p}_{o}})$
is such that for all $w\in A^{*}_{S}$,
$f^{\Box}_{S^{p}_{o}}(w)=f^{\Box}_{S}(w)$,
$f^{\scalebox{1.1}{$\circ$}}_{S^{p}_{o}}(w)=f^{\scalebox{1.1}{$\circ$}}_{S}(w)$,
and by Definition 3, $\Delta_{S^{p}_{o}}=\Delta_{S}$. Therefore,
$S^{p}_{o}=S$. It follows that $S\preceq_{n}T$. ∎

A practical consequence of Theorem 3.3 is that the complexity of deciding
$Impl_{n}(S)\subseteq Impl_{n}(T)$ is equivalent to the complexity of deciding
$S\preceq_{n}T$.

##  4 Non-determinism of NMTS is Non-reducible

In the previous section, we showed how the further constraints imposed on MTS
and their refinement (i.e., Definition 3 and Definition 4) are necessary and
sufficient to obtain a sound and complete refinement relation. An important
challenge discussed in [12] is to argue that the considered set of
implementations is also interesting from a practical point of view (i.e., no
valuable implementation is disregarded by $\preceq_{n}$).

In this section we discuss a property concerning non-deterministic optional
transitions that is violated by all implementations accepted by $\preceq_{m}$
and discarded by $\preceq_{n}$. MTS allow to express transitions that must be
enabled in all implementations. In this case, the presence of non-determinism
is unaltered in all implementations, because must transitions cannot be
disabled. Conversely, optional transitions can be arbitrarily disabled, and in
MTS the non-determinism in optional branches can be reduced or fully resolved.
However, the standard semantics of MTS do not provide the means to specify
actions that are susceptible to both enablement and disablement, yet
inevitably yield non-deterministic outcomes. This issue arises since any
action capable of being deactivated (i.e., an optional action) also opens the
possibility of diminishing its associated non-determinism. We term the
property stating that all optional actions in an MTS can be enabled or
disabled, while retaining their irreducible non-determinism, as _non-reducible
non-determinism_.

In formal specifications expressed as MTS, non-determinism is commonly used to
express under-specifications. This variant of non-determinism does not
necessitate preservation across all implementations of an MTS. Consequently,
modal refinement can reduce the non-determinism to fully determine a
specification, i.e., modal refinement does not satisfy the non-reducible non-
determinism property (see, e.g., Figure 5). There exists a distinction between
non-determinism present in all implementations (as showed in the next example)
and the non-determinism that characterizes under-specifications. However, both
these forms of non-determinism are expressed in an identical way within MTS.
This inherent ambiguity contributes to the incompleteness of modal refinement.
To address this, we assume that non-deterministic behaviour of MTS is always
preserved across all implementations, thereby eliminating non-determinism as a
source of under-specification. Consequently, NMTS refinement satisfies the
property of non-reducible non-determinism, whilst this is not the case for
modal refinement.

$\overline{go}$$head$$tail$$toss$$toss$$win$$lose$$\overline{go}$$head$$tail$$toss$$toss$$win$$lose$$\overline{go}$$head$$tail$gameover$toss$$toss$$win$$lose$
Figure 6:  From left to right, the NMTS modelling a coin toss game, an NMTS
implementation allowing infinite plays, an NMTS implementation allowing one
play.

In the following, we discuss an example showcasing the need to establish the
non-reducible non-determism property. Consider the NMTS in Figure 6 (left).
This NMTS serves as a model for a coin toss game. We visualize the actions of
this NMTS as buttons that light up and can only be pressed when the respective
action becomes enabled. Upon pressing an enabled button, the associated action
is carried out.

Initially, only one action, namely $toss$, is enabled. Upon executing the
$toss$ action, the outcome can result in either head or tail. If the outcome
is head, the $win$ action becomes enabled, while in the case of tail, the
$lose$ action is enabled. Upon the execution of either $win$ or $lose$, the
NMTS reverts back to its initial state. The NMTS does not specify whether the
coin is biased.

The $toss$ action exemplifies the property of non-reducible non-determinism.
In essence, any implementation that enables the $toss$ action must
consistently manifest the same non-deterministic behavior. Notably, the $toss$
action can be deactivated. An implementation that restricts the coin’s
outcomes solely to either heads or tails is considered invalid. However, under
the standard modal refinement $\preceq_{m}$, such invalid implementations are
deemed acceptable. Figure 6 (center and right) depicts two valid
implementations of the NMTS. In one, an indefinite number of plays are
feasible, while in the other, only a single play is permitted. Both these
implementations are preserving the non-determinisc nature of the $toss$
action.

The introduced NMTS refinement (see Definition 4) exclusively permits
implementations like the one showcased in Figure 6 whilst forbidding invalid
implementations as those forcing the coin to only return either head or tail.
Clearly, by relaxing the constraints in either Definition 3 or Definition 4,
it is possible to define systems whose implementations may violate the non-
reducible non-determinism property (see Section 3).

##  5 Related Work

MTS and their dialects are widely studied in the literature. Given two MTS $S$
and $T$, $S$ is a thorough refinement of $T$ whenever the set of
implementations of $S$ is included in the set of implementations of $T$. In
[12], four different refinement relations are studied extensively, including
thorough refinement, and an MTS is said to be _consistent_ if it admits at
least one non-empty implementation. MTS that allow inconsistent
specifications, where transitions can be necessary but not permitted, are
called Mixed Transition Systems [8, 1].

In [7, Corollary 4.6], it is proved that, similarly to modal refinement,
thorough refinement is decidable in polynomial time for deterministic MTS,
whilst thorough refinement is decidable in EXPTIME for non-deterministic MTS.
The authors describe a tableau-style algorithm [7, Section 6] for deciding
thorough refinement, which runs in exponential time in the worst case. While
thorough refinement does not always imply modal refinement of MTS, in [6,
Lemma 3.6] it is proved that thorough refinement implies modal refinement of a
deterministic overapproximation of (non-deterministic) MTS.

In [12, Theorem 3], it is proved that any alternative notion $\preceq_{alt}$
of modal refinement that is both sound and complete cannot be decided in
polynomial time unless $\textit{P}\\!=\\!\textit{NP}$. This is obtained by
reducing the problem of deciding thorough refinement to the problem of
deciding whether a 3-DNF formula is a tautology. However, in this case,
thorough refinement considers all implementations obtained through modal
refinement $\preceq_{m}$, and not only those obtained using the alternative
notion $\preceq_{alt}$. The problem of proposing an alternative notion of
modal refinement that is both sound and complete with respect to its set of
implementations is left open [12]. The main challenge is to argue that the
considered set of implementations is also interesting from a practical point
of view. In this paper, we addressed this challenge and discussed how all
implementations retained by $\preceq_{m}$ and discarded by $\preceq_{n}$ are
violating the non-reducible non-determinsm property (see Section 4).

Parametric MTS (PMTS) [5, 11, 4] were introduced to enhance the expressiveness
of MTS. PMTS are LTS equipped with an obligation function $\Phi$, which is a
parametric Boolean proposition over the outgoing transitions from each state.
The satisfying assignments of $\Phi$ yield the allowed combinations of
outgoing transitions. When $\Phi$ is not parametric, PMTS are called Boolean
MTS (BMTS). PMTS are capable of expressing, among others, _persistent_ choices
(i.e., once some outgoing transition is enabled, it must be enabled also
everywhere else). It is shown that MTS are a special case of BMTS, and that
BMTS are a special case of PMTS. Rather than extending MTS, in this paper we
presented a subset of MTS for which a sound and complete refinement relation
is proposed. Thorough refinement is computable in NEXPTIME for both BMTS and
PMTS, while we show in this paper that thorough refinement is polynomial for
NMTS. Modal refinement of MTS, BMTS, and PMTS is not complete, whereas we show
in this paper that NMTS refinement is complete (Lemma 3.3). The deterministic
variants of PMTS and BMTS are called, respectively, DPMTS and DBMTS. When
restricting to only deterministic systems, similarly to NMTS, also DBMTS modal
refinement is complete, whereas DPMTS modal refinement is still not complete.

In [2, 3], Coherent MTS (CMTS) are introduced as a model for software product
lines (SPL). In CMTS, the features of an SPL are identified with the actions
of an MTS. Therefore, in CMTS an action cannot be the label of both a
necessary and an optional transition, since a feature is either mandatory or
optional. The notion of ‘consistent’ product derivation requires that whenever
an optional transition is discarded in an implementation, all transitions
sharing the same label must also be discarded. This consistency requirement
mimicks the aforementioned persistency of PMTS [5, 11, 4] and it is not to be
confused with the above mentioned notion of consistency as studied in [12]. In
[2] the refinement of CMTS is presented, which is demonstrated to be both
sound and complete in relation to its set of implementations.

CMTS and their refinement [2] are an important milestone in addressing the
long-standing problem proposed at CONCUR 2007 [12]. NMTS and CMTS are
currently the only available subsets of MTS that possess the capacity to
preserve both non-deterministic specifications and completeness of the
refinement relation. In contrast, all the other MTS extensions mentioned above
do not possess completeness of refinement in the case of non-deterministic
specifications. In CMTS, by interpreting SPL features as MTS actions,
‘consistency’ and ‘coherence’ are enforced globally across all system states.
NMTS are a generalization of CMTS. In NMTS, the SPL-derived limitations are
discarded (i.e., actions are not interpreted as features of an SPL). The
constraints that in CMTS are applied globally, in NMTS are instead applied
exclusively to the set of states reachable through the same sequence of
actions. Consequently, NMTS strictly include CMTS while introducing a
refinement concept that remains sound and complete. Differently from the
restrictions imposed by CMTS and their refinement, in Section 3, we identified
the restrictions imposed by NMTS and their refinement as necessary to achieve
completeness in the refinement relation. Furthermore, in Section 4 we
presented a property that is violated by all implementations discarded by the
NMTS refinement relation but accepted through modal refinement.

##  6 Conclusion

We have introduced a subset of Modal Transition Systems (MTS) called Non-
reducible MTS (NMTS) and their refinement relation ($\preceq_{n}$).

In NMTS, states reached through the execution of identical action sequences
are related. Outgoing transitions from related states that are labeled by the
same action also exhibit the same modality. Disabling an optional transition
within a refinement results in the deactivation of all transitions that share
both the same action label and are outgoing from related states. We showed
that these two conditions are necessary to achieve completeness. If either of
these conditions is relaxed, it becomes possible to construct two systems that
are not in refinement relation, yet their respective sets of implementations
still maintain a relation of set inclusion. We proved that $\preceq_{n}$ is
both sound and complete with respect to its set of implementations. By
interpreting the optional non-determinism present in MTS as non-reducible
(i.e., non-deterministic behaviour within MTS is consistently maintained in
all implementations), we have showed that all implementations permitted by
$\preceq_{m}$ (modal refinement) but rejected by $\preceq_{n}$ are considered
invalid.

### Future work

In Section 4, we investigated optional non-determinism of MTS, which can be
interpreted in two distinct ways: as either under-specifications or optional
actions with irreducible non-determinism across all implementations. To
resolve this ambiguity and the challenge posed by [12], we opted to associate
the latter interpretation with non-deterministic optional actions. However,
this decision brings forth a new challenge: introducing the means to express
under-specifications while preserving the completeness of the refinement
relation requires further investigations.

## References

  * [1] Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wąsowski, A.: 20 Years of Modal and Mixed Specifications. B. EATCS 95, 94–129 (2008), https://vbn.aau.dk/files/16474238/BEATCS2008.pdf
  * [2] Basile, D., ter Beek, M.H., Fantechi, A., Gnesi, S.: Coherent modal transition systems refinement, submitted for publication
  * [3] ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: Modelling and analysing variability in product families: Model checking of modal transition systems with variability constraints. J. Log. Algebr. Meth. Program. 85(2), 287–315 (2016). https://doi.org/10.1016/j.jlamp.2015.11.006
  * [4] Beneš, N., Křetínský, J., Larsen, K.G., Møller, M.H., Sickert, S., Srba, J.: Refinement checking on parametric modal transition systems. Acta Inform. 52(2-3), 269–297 (2015). https://doi.org/10.1007/s00236-015-0215-4
  * [5] Beneš, N., Křetínský, J., Larsen, K.G., Møller, M.H., Srba, J.: Parametric Modal Transition Systems. In: Bultan, T., Hsiung, P. (eds.) Proceedings 9th International Symposium on Automated Technology for Verification and Analysis (ATVA’11). LNCS, vol. 6996, pp. 275–289. Springer (2011). https://doi.org/10.1007/978-3-642-24372-1_20
  * [6] Beneš, N., Křetínský, J., Larsen, K.G., Srba, J.: On determinism in modal transition systems. Theor. Comput. Sci. 410(41), 4026–4043 (2009). https://doi.org/10.1016/j.tcs.2009.06.009
  * [7] Beneš, N., Křetínský, J., Larsen, K.G., Srba, J.: EXPTIME-completeness of thorough refinement on modal transition systems. Inf. Comput. 218, 54–68 (2012). https://doi.org/10.1016/j.ic.2012.08.001
  * [8] Dams, D., Gerth, R., Grumberg, O.: Abstract Interpretation of Reactive Systems. ACM Trans. Program. Lang. Syst. 19(2), 253–291 (1997). https://doi.org/10.1145/244795.244800
  * [9] Keller, R.M.: Formal Verification of Parallel Programs. Commun. ACM 19(7), 371–384 (1976). https://doi.org/10.1145/360248.360251
  * [10] Křetínský, J.: 30 Years of Modal Transition Systems: Survey of Extensions and Analysis. In: Aceto, L., Bacci, G., Bacci, G., Ingólfsdóttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools, LNCS, vol. 10460, pp. 36–74. Springer (2017). https://doi.org/10.1007/978-3-319-63121-9_3
  * [11] Kretínský, J., Sickert, S.: On Refinements of Boolean and Parametric Modal Transition Systems. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Proceedings 10th International Colloquium on Theoretical Aspects of Computing (ICTAC’13). LNCS, vol. 8049, pp. 213–230. Springer (2013). https://doi.org/10.1007/978-3-642-39718-9_13
  * [12] Larsen, K.G., Nyman, U., Wąsowski, A.: On Modal Refinement and Consistency. In: Caires, L., Vasconcelos, V.T. (eds.) Proceedings 18th International Conference on Concurrency Theory (CONCUR’07). LNCS, vol. 4703, pp. 105–119. Springer (2007). https://doi.org/10.1007/978-3-540-74407-8_8
  * [13] Larsen, K.G., Thomsen, B.: A Modal Process Logic. In: Proceedings 3rd Symposium on Logic in Computer Science (LICS’88). pp. 203–210. IEEE (1988). https://doi.org/10.1109/LICS.1988.5119


# Complexity Results for Implication Bases of Convex Geometries

Todd Bichoupan  Department of Computer Science, Hofstra University, Hempstead,
NY 11549<EMAIL_ADDRESS>
(Date: November 15, 2022)

###### Abstract.

A convex geometry is finite zero-closed closure system that satisfies the
anti-exchange property. Complexity results are given for two open problems
related to representations of convex geometries using implication bases. In
particular, the problem of optimizing an implication basis for a convex
geometry is shown to be NP-hard by establishing a reduction from the minimum
cardinality generator problem for general closure systems. Furthermore, even
the problem of deciding whether an implication basis defines a convex geometry
is shown to be co-NP-complete by a reduction from the Boolean tautology
problem.

##  1\. Introduction

Convex geometries are finite zero-closed closure systems satisfying the anti-
exchange property. P. Edelman and R. Jamison introduced convex geometries in
[6] as a common formulation for various equivalent structures appearing in
several areas of research, including lattice theory and relational databases.
More recently, K. Adaricheva and J.B. Nation published a survey of work
related to convex geometries [2]. H. Yoshikawa et al. found a notable
application for convex geometries in computer-driven education systems, where
convex geometries are used in their dual form as _antimatroids_ to model the
space of possible knowledge states of learners [13].

This paper continues an effort to study convex geometries through the lens of
implication bases.

A set of implications $\Sigma=\\{A_{i}\rightarrow B_{i}:1\leq i\leq n\\}$
defining a finite closure system is an _optimum basis_ if its size is minimal
among all implication bases for the same closure system; the size of an
implication basis is the sum of all cardinalities of the sets on the left and
right sides of its implications. D. Maier showed that the general problem of
finding an optimum basis for a closure system given by an arbitrary
implication basis is NP-hard [9].

On the other hand, several special classes of closure systems are known to
have tractable optimum bases. M. Wild showed tractability of optimum bases for
modular closure systems in [12], and E. Boros et al. showed tractability of
optimum bases for component-quadratic closure systems in [4]. In particular,
many subclasses of the convex geometries are known to have tractable optimum
bases. K. Kashiwabara and M. Nakamura proved tractability of optimum bases for
affine geometries [8], and K. Adaricheva showed tractability of optimum bases
for convex geometries that satisfy the Carousel property, convex geometries
that do not have $D$-cycles, and convex geometries of order convex subsets in
a poset [1]. But the problem of determining whether there is a tractable
algorithm to find optimum bases of convex geometries in general has remained
open.

We show that, given an arbitrary implication basis for a convex geometry, the
problem of finding an optimum basis is NP-hard. The proof relies on a
reduction from the _minimum cardinality generator_ problem for general closure
systems, described in Section 3. In [10], C.L. Lucchesi and S.L. Osborn
describe a problem equivalent to the minimum cardinality generator problem and
prove NP-completeness by a reduction from the graph vertex cover problem.
Section 3 gives a proof of the intractability of the minimum cardinality
generator problem by a reduction from the Boolean CNF satisfiability problem.
Section 4 completes the proof of intractability of optimum bases of convex
geometries.

In Section 5, we show that even the problem of deciding whether an implication
basis defines a convex geometry is co-NP-complete. The proof is a direct
reduction from the Boolean DNF tautology problem.

##  2\. Definitions and Background Theorems

We use definitions and notational conventions from [3, 5]. A closure system
$\langle X,\phi\rangle$ is a set, $X$, equipped with a function,
$\phi:\mathcal{P}(X)\mapsto\mathcal{P}(X)$, satisfying the properties
$A\subseteq\phi(A)$, $A\subseteq B\implies\phi(A)\subseteq\phi(B)$, and
$\phi(\phi(A))=\phi(A)$ for all $A,B\subseteq X$; such a function $\phi$ is
called a _closure operator_ on $X$, and the sets in the image of $\phi$ are
called _closed sets_. Closure systems can be equivalently defined in terms of
their closed sets: if $\mathcal{F}$ is a family of subsets of $X$ such that
$\mathcal{F}$ is closed under set intersection and $\mathcal{F}$ contains $X$,
the function $\phi$ defined by $\phi(A)=\cap\\{S\in\mathcal{F}:A\subseteq
S\\}$ for all $A\subseteq X$ is a closure operator on $X$, and the image of
$\phi$ is precisely $\mathcal{F}$. Conversely, if $\langle X,\phi\rangle$ is a
closure system and $\mathcal{F}$ is the image of $\phi$, then $\mathcal{F}$ is
closed under set intersection, $\mathcal{F}$ contains $X$, and
$\phi(A)=\cap\\{S\in\mathcal{F}:A\subseteq S\\}$ for all $A\subseteq X$. A
closure system $\langle X,\phi\rangle$ is finite if its ground set, $X$, is
finite. A closure system $\langle X,\phi\rangle$ is _zero-closed_ if the empty
set is closed in the system, i.e. if $\phi(\emptyset)=\emptyset$.

A _convex geometry_ is a finite zero-closed closure system satisfying the
anti-exchange property. For a finite closure system $\langle X,\phi\rangle$,
the _anti-exchange_ property is the condition that
$y\not\in\phi(A\cup\\{x\\})$ or $x\not\in\phi(A\cup\\{y\\})$ for every closed
set $A\subsetneq X$ and all $x,y\in X\setminus A$ with $x\neq y$. A condition
equivalent to the anti-exchange property for finite closure systems $\langle
X,\phi\rangle$ is that for every closed set $A\subsetneq X$, there is an
element $x\in X\setminus A$ such that $A\cup\\{x\\}$ is closed.

An _implication_ on a nonempty set $X$ is an ordered pair of sets
$A,B\subseteq X$ where $B\neq\emptyset$, denoted $A\rightarrow B$. An
implication $A\rightarrow B$ on $X$ holds in the closure system $\langle
X,\phi\rangle$ if, for every closed set $S$ of $\langle X,\phi\rangle$,
$A\subseteq S\implies B\subseteq S$, or equivalently if $B\subseteq\phi(A)$.
For any set $\Sigma$ of implications on a set $X$, the family of sets
$\mathcal{F}=\\{S\subseteq X:\forall(A\rightarrow B)\in\Sigma$: $A\subseteq
S\implies B\subseteq S\\}$ is closed under set intersection and contains $X$,
and $\Sigma$ is called an _implication basis_ for the closure system on $X$
associated with $\mathcal{F}$. Given an implication basis $\Sigma$ of a finite
closure system $\langle X,\phi\rangle$ and a set $S\subseteq X$, there are
straightforward algorithms to compute $\phi(S)$.

A _quasi-closed_ set $Q$ of a closure system $\langle X,\phi\rangle$ is a
subset of $X$ such that $Q$ is not closed and for every closed set $S$ of
$\langle X,\phi\rangle$, $Q\subseteq S$ or $S\cap Q$ is closed; an equivalent
definition is that $Q\subseteq X$ is quasi-closed if $Q$ is not closed and for
all $S\subseteq Q$, $\phi(S)=\phi(Q)$ or $\phi(S)\subsetneq Q$. A _critical
set_ $C$ of a closure system $\langle X,\phi\rangle$ is a quasi-closed set
that is minimal among all quasi-closed sets of $\langle X,\phi\rangle$ that
have the same closure as $C$; that is, a quasi-closed set $C$ is critical if
for every quasi-closed set $Q\subsetneq C$, $\phi(Q)\subsetneq\phi(C)$. If
$\langle X,\phi\rangle$ is a closure system, $\mathcal{F}$ is the family of
all closed sets of $\langle X,\phi\rangle$, and $\mathcal{Q}$ is the family of
all quasi-closed sets of $\langle X,\phi\rangle$, then the family of sets
$\mathcal{F}\cup\mathcal{Q}$ is closed under set intersection and has an
associated closure system, $\langle X,\sigma\rangle$, where $\sigma$ is called
the _saturation operator_ of $\langle X,\phi\rangle$.

######  Theorem 1.

If $\langle X,\phi\rangle$ is a finite closure system, $\sigma$ is the
associated saturation operator, and $\Sigma$ is an associated implication
basis, then for every critical set $C$ of $\langle X,\phi\rangle$, there is an
implication $(A\rightarrow B)\in\Sigma$ such that $\sigma(A)=C$. Furthermore,
for every finite closure system $\langle X,\phi\rangle$, the set
$\Sigma_{C}=\\{C\rightarrow\phi(C):C\text{ is a critical set of }\langle
X,\phi\rangle\\}$, called the _canonical basis_ of $\langle X,\phi\rangle$, is
a valid implication basis of $\langle X,\phi\rangle$ and has minimal
cardinality among all implication bases of $\langle X,\phi\rangle$.

J.L. Guigues and V. Duquenne proved the statements of Theorem 1 in [7], and D.
Maier gave a similar result in the context of relational databases [9]. M.
Wild later connected Guigues and Duquenne’s work to Maier’s and made their
results significantly more accessible in [11].

An implication basis $\Sigma_{O}$ of a finite closure system $\langle
X,\phi\rangle$ is called an _optimum basis_ of $\langle X,\phi\rangle$ if the
sum of all cardinalities of all left and right sides of the implications in
$\Sigma_{O}$ is minimal among all implication bases for $\langle
X,\phi\rangle$. It is possible to conclude from Theorem 1 that optimum bases
are shortenings of the canonical basis; that is, if $\Sigma_{C}$ is the
canonical basis of a finite closure system and $\Sigma_{O}$ is an optimum
basis of the same closure system, then there is bijection
$f:\Sigma_{C}\mapsto\Sigma_{O}$ such that for all $(A\rightarrow
B)\in\Sigma_{C}$, $f(A\rightarrow B)=C\rightarrow D$ where $C\subseteq A$ and
$D\subseteq B$.

The _Boolean satisfiability problem_ gives a Boolean proposition, $P$, on $n$
variables and asks if there exists a truth assignment, $\psi$, of the
variables such that $P$ evaluates to _true_ according to $\psi$. The _Boolean
CNF satisfiability problem_ is a special case of the Boolean satisfiability
problem that only considers propositions written in _conjunctive normal form_.
A Boolean proposition is in _conjunctive normal form_ if it is expressed as a
conjunction of clauses, and each clause is a disjunction of literals; a
literal is either a single variable or the complement of a single variable.
The Boolean CNF satisfiability problem is equivalent to the Boolean
satisfiability problem in the sense that both are NP-complete.

The _Boolean tautology problem_ is a dual problem to the Boolean
satisfiability problem: the Boolean tautology problem gives a proposition,
$P$, on $n$ variables and asks if there is a truth assignment, $\psi$, of the
variables such that $P$ evaluates to _false_ according to $\psi$. The _Boolean
DNF tautology problem_ is a special case of the Boolean tautology problem that
only considers propositions written in _disjunctive normal form_ ; a Boolean
proposition is in _disjunctive normal form_ if it is expressed as a
disjunction of clauses, and each clause is a conjunction of literals. The
Boolean DNF tautology problem is dual to the Boolean CNF satisfyability
problem, and both the Boolean DNF tautology problem and the general Boolean
tautology problem are co-NP-complete.

##  3\. The Minimum Cardinality Generator Problem

A _generator_ of a closure system $\langle X,\phi\rangle$ is a set $S$ such
that $\phi(S)=X$. Given a set of implications $\Sigma$, the _minimum
cardinality generator_ problem asks to find a generator of minimal cardinality
for the closure system associated with $\Sigma$. In [10], C.L. Lucchesi and
S.L. Osborn studied an equivalent problem phrased in the language of
functional dependencies for relational databases, and proved a result
equivalent to Lemma 2 below.

######  Lemma 2.

The minimum cardinality generator problem is NP-hard.

###### Proof.

The proof proceeds by reduction from the Boolean CNF satisfiability problem.
Let $P$ be a Boolean expression on $n$ variables, $a_{1},...,a_{n}$, and
suppose that $P$ is written in conjunctive normal form with clauses
$c_{1},...,c_{m}$; that is, $P=c_{1}\land...\land c_{m}$, where each $c_{j}$
is a disjunction of literals.

Let $X=\\{x_{1},...,x_{n},y_{1},...,y_{n},z_{1},...z_{m},s\\}$, and define the
set of implications $\Sigma$ as follows:

  * •

For each clause $c_{j}$ of $P$ and each literal $a_{i}$ in $c_{j}$,
$(x_{i}\rightarrow z_{j})\in\Sigma$.

  * •

For each clause $c_{j}$ $P$ and each literal $\neg a_{i}$ in $c_{j}$,
$(y_{i}\rightarrow z_{j})\in\Sigma$.

  * •

$(z_{1}...z_{m}\rightarrow s)\in\Sigma$.

  * •

For each $i$, $(sx_{i}\rightarrow y_{i})\in\Sigma$ and $(sy_{i}\rightarrow
x_{i})\in\Sigma$.

Any generator of the closure system associated with $\Sigma$ must contain
$x_{i}$ or $y_{i}$ for each $i$, and therefore must have cardinality at least
$n$. On the other hand, the closure system associated with $\Sigma$ has a
generator of cardinality $n$ if and only $P$ is satisfiable.

Given a truth assignment $\psi$ of $(a_{1},...,a_{n})$, let
$S\subseteq\\{x_{1},...,x_{n},y_{1},...,y_{n}\\}$ be the set of cardinality
$n$ such that $x_{i}\in S$ if (and only if) $a_{i}$ is true according to
$\psi$ and $y_{i}\in S$ if (and only if) $a_{i}$ is false according to $\psi$.
Then $z_{j}\in\phi(S)$ if and only if $c_{j}$ evaluates to true under $\psi$,
and $s\in\phi(S)$ if and only if $P$ evaluates to true under $\psi$. It
follows that $\phi(S)=X$ if and only if $P$ evaluates to true under $\psi$. ∎

##  4\. Optimum Bases of Convex Geometries

######  Theorem 3.

The problem of finding an optimum basis for a convex geometry given an
arbitrary implication basis is NP-hard.

###### Proof.

Let $n$ and $m$ be positive integers and let $X=\\{x_{1},...,x_{m}\\}$. For
each positive integer $i\leq n$, let $A_{i}$ and $B_{i}$ be nonempty subsets
of $X$ such that $A_{i}\cap B_{i}=\emptyset$. Let $\Sigma=\\{A_{i}\rightarrow
B_{i}:1\leq i\leq n\\}$ be an implication basis. Let $\phi$ be the closure
operator associated with $\Sigma$. By Lemma 2, it suffices to reduce the
problem of finding a minimum cardinality generator for the closure system
associated with $\Sigma$ to the problem of optimizing an implication basis for
a convex geometry.

For each $(A_{i}\rightarrow B_{i})\in\Sigma$, let $\Sigma_{i}$ be the basis
consisting solely of the implication $A_{i}\rightarrow B_{i}$. Let
$Y=\\{y_{1},...,y_{n}\\}$. For each $i$, let
$\Sigma_{i}^{{}^{\prime}}=\\{(A_{i}\cup Y\setminus\\{y_{i}\\})\rightarrow
B_{i}\\}$ be a singleton implication basis on the set $X\cup Y$. Let
$\Sigma^{{}^{\prime}}=(\cup_{i=1}^{n}\Sigma_{i}^{{}^{\prime}})\cup\\{Y\rightarrow
X\\}$.

######  Claim 1.

The closure system associated with $\Sigma^{{}^{\prime}}$ is a convex
geometry.

######  Claim 2.

Every optimum basis for the closure system associated with
$\Sigma^{{}^{\prime}}$ is of the form
$(\cup_{i=1}^{n}\Sigma_{i}^{{}^{\prime}})\cup\\{Y\rightarrow S\\}$, where $S$
is a minimum cardinality generator for the closure system associated with
$\Sigma$.

###### Proof of Claim 1.

Let $C$ be a closed set in the closure system associated with
$\Sigma^{{}^{\prime}}$. If $|C\cap Y|\leq n-2$, then $C\cup\\{x\\}$ is closed
for every $x\in X\setminus C$; if $|C\cap Y|\leq n-2$ and $X\setminus
C=\emptyset$, then $C\cup\\{y\\}$ is closed for every $y\in Y\setminus C$.
Furthermore, if $|C\cap Y|=n=|Y|$, then $C$ must equal the top element, $X\cup
Y$. So the only case left to consider is $|C\cap Y|=n-1$. Let $y_{i}$ be the
sole element of $Y\setminus C$ and let $A_{i},B_{i}$ be the subsets of $X$
with $((A_{i}\cup Y\setminus\\{y_{i}\\})\rightarrow
B_{i})\in\Sigma^{{}^{\prime}}$. Then for each $x\in X\setminus A_{i}$,
$C\cup\\{x\\}$ is closed. If $X\setminus A_{i}\subseteq C$, then
$B_{i}\subseteq C$, which implies that $C\cup\\{x\\}$ is closed for every
$x\in X$. Lastly, if $X\subseteq C$, then $C\cup\\{y_{i}\\}$ is the top
element (which is closed). ∎

###### Proof of Claim 2.

Let $\phi^{{}^{\prime}}$ be the closure operator associated with
$\Sigma^{{}^{\prime}}$. For each positive integer $i$ less than or equal to
$n$, let $L_{i}=A_{i}\cup Y\setminus\\{y_{i}\\}$ and let $R_{i}=B_{i}$. Let
$L_{0}=Y$ and let $R_{0}=X$. For each $i$, $\phi(L_{i})=L_{i}\cup R_{i}$: when
$i=0$, $L_{i}\cup R_{i}$ is closed because it equals the top element, and when
$i\neq 0$, $L_{i}\cup R_{i}$ is closed because $y_{i}\not\in L_{i}\cup R_{i}$
(since $L_{i}\cup R_{i}=(Y\setminus\\{y_{i}\\})\cup(A_{i}\cup B_{i})$ where
$A_{i}\cup B_{i}\subseteq X$) and $y_{i}\in L_{j}$ for each $j\neq i$.

Since all of the $A_{i}$ are nonempty, every proper subset of every $L_{i}$ is
closed; but since $R_{i}\not\subseteq L_{i}$ for any $i$, none of the $L_{i}$
are closed. Also, the closures of the $L_{i}$ are distinct, since they have
distinct intersections with $Y$. So for each $i$, $L_{i}$ is a critical set
and is not the saturation of any set below it. Therefore, by Theorem 1, an
optimum basis for the closure system associated with $\Sigma^{{}^{\prime}}$
must consist of implications of the form $L_{i}\rightarrow S_{i}$ where
$S_{i}\subseteq R_{i}$ for each $i$; furthermore, when $i$ is positive,
$L_{j}\not\subseteq L_{i}\cup R_{i}$ for any $j\neq i$, so $S_{i}$ must equal
$R_{i}$.

Let $S$ be a subset of $X$ and let
$\Sigma^{{}^{\prime}}_{O}=\\{L_{i}\rightarrow R_{i}:1\leq i\leq
n\\}\cup\\{Y\rightarrow
S\\}=(\cup_{i=1}^{n}\Sigma_{i}^{{}^{\prime}})\cup\\{Y\rightarrow S\\}$. Let
$\phi^{{}^{\prime}}_{O}$ be the closure operator for the closure system
associated with $\Sigma^{{}^{\prime}}_{O}$. $\Sigma^{{}^{\prime}}_{O}$ is a
valid basis for the closure system associated with $\Sigma^{{}^{\prime}}$ if
and only if the implication $Y\rightarrow X$ can be derived in
$\Sigma^{{}^{\prime}}_{O}$, or equivalently, if and only if
$X\subseteq\phi^{{}^{\prime}}_{O}(Y)$. Since $L_{i}\setminus Y=A_{i}$ and
$R_{i}=B_{i}$ for each positive $i$,
$\phi^{{}^{\prime}}_{O}(Y)=\phi^{{}^{\prime}}_{O}(Y\cup S)=Y\cup\phi(S)$. So
$\Sigma^{{}^{\prime}}_{O}$ is a valid basis for the closure system associated
with $\Sigma^{{}^{\prime}}$ if and only if $S$ is a generator of the closure
system associated with $\Sigma$. It follows that $\Sigma^{{}^{\prime}}_{O}$ is
an optimum basis for the closure system associated with $\Sigma^{{}^{\prime}}$
if and only if $S$ is a minimum cardinality generator of the closure system
associated with $\Sigma$. ∎

##  5\. Deciding if a Closure System is a Convex Geometry

######  Theorem 4.

Given an arbitrary implication basis, the problem of determining whether the
closure system associated with that basis is a convex geometry is co-NP-
complete.

###### Proof.

Inclusion in co-NP is clear, because it is easy to validate a counterexample
to the anti-exchange property when an implication basis is given (and it is
easy to determine if the associated closure system is zero-closed).

The proof of co-NP-hardness proceeds by reduction from the Boolean DNF
tautology problem. Let $P$ be a Boolean expression on $n\geq 2$ variables,
$a_{1},...,a_{n}$, and suppose that $P$ is written in disjunctive normal form.
Let $c_{1},...,c_{m}$ be the clauses of $P$; so $P=c_{1}\lor...\lor c_{m}$,
where each $c_{j}$ is a conjunction of literals.

Let $X=\\{x_{1},...,x_{n},t_{1},...,t_{n},f_{1},...,f_{n}\\}$. Let
$x_{n+1}=x_{1}$. Define an implication basis $\Sigma$ on $X$ as follows:

  * •

For each positive integer $i\leq n$, $(x_{i}t_{i}\rightarrow
x_{i+1})\in\Sigma$ and $(x_{i}f_{i}\rightarrow x_{i+1})\in\Sigma$.

  * •

For each $c_{j}$, define the set
$S_{j}\subseteq\\{t_{1},...,t_{n},f_{1},...,f_{n}\\}$ as follows: $t_{i}\in
S_{j}$ if (and only if) $c_{j}$ contains the literal $a_{i}$, and $f_{i}\in
S_{j}$ if (and only if) $c_{j}$ contains the literal $\neg a_{i}$. For all
$S_{j}$, $(S_{j}\rightarrow x_{1})\in\Sigma$.

The closure system associated with $\Sigma$ is a convex geometry if and only
if $P$ is a tautology.

If $P$ is not a tautology, then there is truth assignment, $\psi$, of the
$a_{i}$ such that $P$ is false under $\psi$. Define
$A\subseteq\\{t_{1},...,t_{n},f_{1},...,f_{n}\\}$ such that $t_{i}\in A$ if
(and only if) $a_{i}$ is true according to $\psi$ and $f_{i}\in A$ if (and
only if) $a_{i}$ is false according to $\psi$. Since $P$ is false under
$\psi$, all of its clauses are false under $\psi$ as well. It follows that no
implication in $\Sigma$ has a left hand side that is a subset of $A$, so $A$
is closed. But then the closure system associated with $\Sigma$ fails the
anti-exchange property, since, for any $i$, the closure of $A\cup\\{x_{i}\\}$
contains all of $\\{x_{1},...,x_{n}\\}$.

Now suppose that $P$ is a tautology. It remains to show that for every closed
set $C$ other than the top element, there is an $e\in X\setminus C$ such that
$C\cup\\{e\\}$ is closed. Let $A$ be a closed set such that for every $i$,
$t_{i}\in A$ or $f_{i}\in A$. Then there is some implication $(S\rightarrow
x_{1})\in\Sigma$ with $S\subseteq A$, so in fact
$\\{x_{1},...,x_{n}\\}\subseteq A$. Then $A\cup\\{e\\}$ is closed for all
$e\in X\setminus A$. Let $B$ be a closed set such that for some $i$,
$t_{i}\not\in B$ and $f_{i}\not\in B$. Then there are three cases:

  * •

If $x_{i}\not\in B$, then $B\cup\\{x_{i}\\}$ is closed.

  * •

If there is $j\leq n$ with $x_{j+1}\in B$ and $x_{j}\not\in B$, then
$B\cup\\{x_{j}\\}$ is closed.

  * •

If $\\{x_{1},...,x_{n}\\}\subseteq B$, then, as before, $B\cup\\{e\\}$ is
closed for all $e\in X\setminus B$.

∎

## Acknowledgement

I am grateful to Kira Adaricheva for her valuable support and professional
guidance.

## References

  * [1] K. Adaricheva, _Optimum basis of finite convex geometry_ , Discrete Applied Mathematics 230 (2017) 11-20.
  * [2] K. Adaricheva, J.B. Nation, _Convex geometries_ , in Lattice Theory: Special Topics and Applications, v.2, G. Grätzer and F. Wehrung, eds. Springer, Basel, 2016.
  * [3] K. Adaricheva, J.B. Nation, _Bases in closure systems_ , in Lattice Theory: Special Topics and Applications, v.2, G. Grätzer and F. Wehrung, eds. Springer, Basel, 2016.
  * [4] E. Boros, O. Čepek, A. Kogan, P. Kučera, _A subclass of Horn CNFs optimally compressible in poynomial time_ , Ann. Math. Artif. Intell. 57 (3–4) (2009) 249–291.
  * [5] N. Caspard, B. Monjardet, _The lattices of closure systems, closure operators, and implicational systems on a finite set: a survey_ , Discrete Applied Mathematics 127 (2003) 241–269.
  * [6] P. Edelman, R. Jamison, _The theory of convex geometries_ , Geom. Dedicata 19 (1985) 247–274.
  * [7] J.L. Guigues, V. Duquenne, _Familles minimales d’implications informatives résultant d’un tableau de données binaires_ , Math. Sci. Hum. 95 (1986) 5–18.
  * [8] K. Kashiwabara, M. Nakamura, _The prime stems of rooted circuits of closure spaces_ , Electron. J. Combin. 20 (2013) paper 22, 13 pages.
  * [9] D. Maier, _Minimum covers in the relational database model_ , J. Assoc. Comput. Mach. 27 (1980) 664–674.
  * [10] C.L. Lucchesi, S.L. Osborn, _Candidate Keys for Relations_ , Journal of Computer and System Sciences 17 (1978) 270-279.
  * [11] M. Wild, _A Theory of Finite Closure Spaces Based on Implications_ , Adv. Math. 108 (1994) 118–139.
  * [12] M. Wild, _Optimal implicational bases for finite modular lattices_ , Quaestiones Math. 23 (2000) 153–161.
  * [13] H. Yoshikawa, H. Hirai, K. Makino, _A representation of antimatroids by Horn rules and its application to educational systems_ , J. Math. Psych. 77 (2017) 82–93.