# Model Repair via Symmetry

Paul Attie111School of Computer and Cyber Sciences, Augusta University,
Augusta GA and William Cocke222Correspoding author, School of Computer and
Cyber Sciences, Augusta University, Augusta GA<EMAIL_ADDRESS>
###### Abstract

The symmetry of a Kripke structure $\mathcal{M}$ has been exploited to replace
a model check of $\mathcal{M}$ by a model check of the potentially smaller
structure $\mathcal{N}$ obtained as the quotient of $\mathcal{M}$ by its
symmetry group $G$. We extend previous work to model repair: identify a
substructure that satisfies a given temporal logic formula. We show that the
substructures of $\mathcal{M}$ that are preserved by $G$ form a lattice that
maps to the substructure lattice of $\mathcal{N}$. We also show the existence
of a monotone Galois connection between the lattice of substructures of
$\mathcal{N}$ and the lattice of substructures of $\mathcal{M}$ that are
”maximal” w.r.t. an appropriately defined group action of $G$ on
$\mathcal{M}$. These results enable us to repair $\mathcal{N}$ and then to
lift the repair to $\mathcal{M}$. We can thus repair symmetric finite-state
concurrent programs by repairing the corresponding $\mathcal{N}$, thereby
effecting program repair while avoiding state-explosion.

##  1 Introduction

The model checking [9] problem for (finite-state) concurrent programs
$P=P_{1}\cdots\\!\parallel\\!P_{n}$ w.r.t. a temporal logic formula $f$ is to
verify that the Kripke structure $\mathcal{M}$ that is generated by the
execution of $P$ satisfies $f$. A major obstacle has been _state explosion_ :
in general, the size of $\mathcal{M}$ is exponential in the number of
processes $n$. When $\mathcal{M}$ and $f$ both have a high degree of symmetry
in the process index set $\\{1,\ldots,n\\}$, the use of _symmetry reduction_
to ameliorate state-explosion can yield significant reduction in the
complexity of model checking $\mathcal{M}\models f$.

An approach that has been thoroughly investigated is the computation of the
quotient structure $\overline{\mathcal{M}}=\mathcal{M}/G$ of $\mathcal{M}$ by
the symmetry group $G$ of symmetries of both $\mathcal{M}$ and $f$.
$\overline{\mathcal{M}}$ can be computed directly from $P$, thereby avoiding
the expensive computation of the large structure $\mathcal{M}$. Since model
checking $\overline{\mathcal{M}}\models f$ is linear in the size of
$\overline{\mathcal{M}}$ [9], this provides significant savings if
$\overline{\mathcal{M}}$ is small. A related approach is the use of structural
methods to express symmetric designs, e.g., parameterized systems, where
processes are all instances of a common template (possibly with a
distinguished controller process), and rings of processes, where all
communication is between a process and its neighbors in the ring.

###  1.1 Our contributions

We present a theory of substructures of Kripke structures which provides a
correspondence theorem between certain substructures of the Kripke structure
$\mathcal{M}$ and the substructures of the quotient structure
$\overline{\mathcal{M}}$. Substructures of $\mathcal{M}$ correspond to
possible repairs of $\mathcal{M}$, while substructures of
$\overline{\mathcal{M}}$ correspond to repairs of $\overline{\mathcal{M}}$.
Because the correspondence between the two lattices of substructures preserves
semantic valuation of certain formulae, we can associate certain repairs of
$\overline{\mathcal{M}}$ with repairs of $\mathcal{M}$. Syntactically the
correspondence of Kripke substructures lattices is of independent mathematical
interest as an example of a monotone Galois connection.

We then build on this theory to extend symmetry-based model checking to
_concurrent program repair_ : given a concurrent program $P$ that may not
satisfy $f$, modify $P$ to produce a program that does satisfy $f$. Given $P$,
$f$, and a group $G$ of symmetries of both $P$ and $f$, our method directly
computes the quotient $\mathcal{M}/G$ (following [26]), then repairs
$\mathcal{M}/G$, using the algorithm of [2], and finally, extracts a correct
program from the repaired structure.

##  2 Related Work

As discussed above, group theoretic approaches to symmetry-reduction [22, 26,
27, 8, 28, 29, 16, 30, 11] compute the quotient $\mathcal{M}/G$ and model
check that, instead of the original (much larger) structure $\mathcal{M}$. A
key consideration is to devise a symmetry group $G$ that is as large as
possible, so as to achieve the greatest possible reductions. Parametrized
systems [23, 24, 17, 18, 25, 21, 19, 10, 33, 13] are those which consist of an
arbitrary number of isomorphic instances of a single process template. The
usual approach is to establish a _cutoff_ : a small value $n$ such that
correctness of a system with $n$ instances implies correctness of arbitrarily
large systems. Special subclasses of parametrized systems include token-
passing systems [1, 12], which circulate one or more tokens amongst isomorphic
processes, and systems based on rendezvous/broadcast/multicast [32, 31, 20].
Bloem et. al. [3] surveys the decidability of verification problems for
parametrized systems.

Buccafurri et. al. [5] posed the repair problem for CTL and solved it using
abductive reasoning to generate repair suggestions that are verified by model
checking. Jobstmann et. al. [34] and Staber et. al. [35] present game-based
repair methods for programs and circuits. Their method is complete for
invariants only. Carrillo and Rosenblueth [6] presents a syntax-directed
repair method that uses “protections” to deal with conjunction, and a
representation of Kripke structures as “tables”. Chatzieleftheriou et. al. [7]
repair abstract structures, using Kripke modal transition systems and 3-valued
CTL semantics. von Essen and Jobstmann [36] present a game-based repair method
which attempts to keep the repaired program close to the original faulty
program, by also specifying a set of traces that the repair must leave intact.

##  3 Preliminary Definitions

In this section we include the formal definitions necessary for structure
repair via symmetry. The section is broken into two parts: the first part
covers the basic definitions of Kripke structures and CTL as can be found in
[15]; the second part covers the basic connections with group theory.

###  3.1 Kripke Structures and CTL

Given a set $AP$ of atomic propositions we define the propositional branching-
time temporal logic CTL[14, 15] by the following grammar:

$\varphi::=\mathsf{true}\mid\mathsf{false}\mid
p\mid\neg\varphi\mid\varphi\land\varphi\mid\varphi\lor\varphi\mid\textup{{AX}}\varphi\mid\textup{{EX}}\varphi\mid\textup{{A}}[\varphi\textup{{\,R\,}}\varphi]\mid\textup{{E}}[\varphi\textup{{\,R\,}}\varphi]$

where $p\in AP$, and $\mathsf{true},\mathsf{false}$ are constant propositions
whose interpretation is the semantic truth values $\mathit{tt},\mathit{ff}$
respectively. A propositional formula is a CTLformula not containing the AX,
EX, AR, ER modalities. The semantics of ${\rm CTL}$ are defined with respect
to a Kripke structure:

######  Definition 3.1 (Kripke structure).

A Kripke structure $\mathcal{M}$ is a tuple $\left(S,S_{0},T,L,AP\right)$
where $S$ is a finite nonempty set of states, $S_{0}\subseteq S$ is a nonempty
set of initial states, $T\subseteq(S\times S)$ is a transition relation, $AP$
is a set of atomic propositions, and $L:S\rightarrow 2^{AP}$ is a labeling
function that associates each state $s\in S$ with a subset of atomic
propositions, namely those that hold in state $s$. We require that
$\mathcal{M}$ be total, i.e., $\forall s\in S,\exists t\in S:(s,t)\in T$.

When referring to the constituents of
$\mathcal{M}=\left(S,S_{0},T,L,AP\right)$, we write
$\mathcal{M}_{S},\mathcal{M}_{S_{0}},\mathcal{M}_{T},\mathcal{M}_{L},$ and
$\mathcal{M}_{AP}$ respectively. State $t$ is a _successor_ of state $s$ in
$M$ iff $(s,t)\in T$. A path $\pi$ in $\mathcal{M}$ is a (finite or infinite)
sequence of states, $\pi=s_{0},s_{1},\ldots$, such that $\forall i\geq
0:(s_{i},s_{i+1})\in T$. A fullpath is an infinite path. State $t$ is
reachable from state $s$ iff there is a path from $s$ to $t$. State $t$ is
reachable iff there is a path from an initial state to $t$. Without loss of
generality, we assume that a Kripke structure does not contain unreachable
states, i.e., every $s\in S$ is reachable.

Throughout the rest of the paper we will refer to two running examples of
Kripke structures. We will refer to these as Example 2-mutex and Example Box.

######  Example 3.2 ($2$-mutex).

This is the classic $2$-mutex example. Our Kripke structure corresponds to two
processes acting concurrently. Each process can be in one of 3 states, either
Neutral, Trying, or Critical and can transiting from Neutral to Trying, from
Trying to Critical, and from Critical to Neutral.

We represent this Kripke structure diagrammatically in the left hand side of
Figure 5. We see all of the transitions represented by arrows, the initial
states are shaded green, and the labels can be seen in each state.

######  Example 3.3 (Box).

The so-called Box Kripke structure in Figure 1 is an example of a highly
symmetric structure, as we will discuss in section 5. This structure has 4
states and is represented in Figure 1. Of note, we assign all states with the
same label, making Box a boring structure with respect to semantic evaluation.
However, the simplicity of Box will be useful when considering the syntactic
concept of a group of state mappings and the various substructures of Box.

Figure 1: The Box Kripke structure. Useful for visualizing concepts.

A CTL formula $\varphi$ is evaluated (i.e., is true or false) in a state $s$
of a Kripke structure $\mathcal{M}$ [15]. Its value in $s$ depends on the
value of its subformulae in states that are reachable from $s$. Write
$\mathcal{M},s\models\varphi$ when $s$ is true in state $s$ of structure
$\mathcal{M}$, and write $\mathcal{M}\models\varphi$ to abbreviate $\forall
s_{0}\in S_{0}:\mathcal{M},s_{0}\models\varphi$, i.e., $\varphi$ holds in all
initial states of $\mathcal{M}$. Appendix A gives the formal definition of
$\models$, which proceeds by induction on the structure of CTL formulae.

$[\varphi\textup{{\,R\,}}\psi]$ ($\varphi$ “releases” $\psi$) means that
$\psi$ must hold up to and including the first state where $\varphi$ holds,
and forever if $\varphi$ never holds. We introduce the abbreviations
$\textup{{A}}[\phi\textup{{\,U\,}}\psi]$ for
$\neg\textup{{E}}[\neg\varphi\textup{{\,R\,}}\neg\psi]$,
$\textup{{E}}[\phi\textup{{\,U\,}}\psi]$ for
$\neg\textup{{A}}[\neg\varphi\textup{{\,R\,}}\neg\psi]$,
$\textup{{AF}}\varphi$ for
$\textup{{A}}[\mathsf{true}\textup{{\,U\,}}\varphi]$, $\textup{{EF}}\varphi$
for $\textup{{E}}[\mathsf{true}\textup{{\,U\,}}\varphi]$,
$\textup{{AG}}\varphi$ for
$\textup{{A}}[\mathsf{false}\textup{{\,R\,}}\varphi]$, $\textup{{EG}}\varphi$
for $\textup{{E}}[\mathsf{false}\textup{{\,R\,}}\varphi]$. We use
$\mathit{tt}$, $\mathit{ff}$ for the (semantic) truth values of
$\mathsf{true}$, $\mathsf{false}$, respectively. Whereas $\mathsf{true}$,
$\mathsf{false}$ are atomic propositions whose interpretation is always
$\mathit{tt}$, $\mathit{ff}$, respectively.

##  4 Substructures of Kripke structures

Symmetry-based repairs are motivated by the correspondence between certain
substructures of two related Kripke structures which we introduce as Theorem
5.16. A substructure of a Kripke structure is defined as follows:

######  Definition 4.1 (Substructure).

Given Kripke structures $\mathcal{M}$ and $\mathcal{M^{\prime}}$, we say that
$\mathcal{M^{\prime}}$ is a substructure of $\mathcal{M}$, denoted
$\mathcal{M^{\prime}}\leq\mathcal{M}$, iff the following all hold:

  1. 1.

$\mathcal{M}^{\prime}_{S}\subseteq\mathcal{M}_{S}$.

  2. 2.

$\mathcal{M}^{\prime}_{S_{0}}=\mathcal{M}_{S_{0}}\cap\mathcal{M}^{\prime}_{S}$.

  3. 3.

$\mathcal{M}^{\prime}_{T}\subseteq\mathcal{M}_{T}$.

  4. 4.

$\mathcal{M}^{\prime}_{AP}=\mathcal{M}_{AP}$.

  5. 5.

$\mathcal{M}^{\prime}_{L}=\mathcal{M}_{L}\\!\upharpoonright\\!S^{\prime}$
(where $\\!\upharpoonright\\!$ denotes domain restriction).

We require substructures to be total. To reiterate, a substructure
$\mathcal{N}$ of a Kripke structure $\mathcal{M}$ is total. For mathematical
necessity in what follows, we allow for the ‘empty’ substructure. Since
substructures must be total, some Kripke structures contain only two
substructures, i.e., the empty substructure and the whole structure.

We return briefly to our examples.

######  Example 4.2 (Example 2-mutex).

Let $\mathcal{M}$ be the Kripke structure correspond to our running example
2-mutex (see Figure 5).

We can form a number of substructures of $\mathcal{M}$. For example, there is
a substructure of $\mathcal{M}$ consisting only of states
$s_{0},s_{1},s_{2},s_{3}$ and $s_{5}$ along with all edges from $\mathcal{M}$.
This substructure corresponds to computations wherein each process must return
to neutral before the other process can enter the trying state. The states
$s_{0},s_{1},s_{3}$ also form a substructure.

######  Example 4.3 (Example Box).

Like our 2-mutex example, Example Box has many substructures. We present some
of these substructures in Figure 2.

Figure 2: Some substructures of Example Box. There are many substructures not
shown.

As seen in the above examples, even a simple Kripke structure can have many
different substructures, even on the same set of states.

We can define a partially ordered set of substructures of a Kripke structure.
This partially ordered set is a lattice i.e., it has a join and a meet
operation. Before we define this lattice, we investigate a few more basic
properties regarding substructures of Kripke structures.

Given a Kripke structure $\mathcal{M}$, a substructure $\mathcal{M^{\prime}}$
of $\mathcal{M}$, and a substructure $\mathcal{M^{\prime\prime}}$ of
$\mathcal{M^{\prime}}$ it is immediate that $\mathcal{M^{\prime\prime}}$ is a
substructure of $\mathcal{M}$.

######  Lemma 4.4.

Let $\mathcal{M}$ be a Kripke structure and suppose that $\mathcal{N}$ and
$\mathcal{N}^{\prime}$ are substructures of $\mathcal{M}$. Then

$\mathcal{N}\vee\mathcal{N}^{\prime}=(\mathcal{N}_{S}\cup\mathcal{N}^{\prime}_{S},\,\mathcal{N}_{S_{0}}\cup\mathcal{N}^{\prime}_{S_{0}},\,\mathcal{N}^{\prime}_{R}\cup\mathcal{N}^{\prime}_{R},\,\mathcal{M}_{L}\\!\upharpoonright\\!(\mathcal{N}_{S}\cup\mathcal{N}^{\prime}_{S}),\,\mathcal{M}_{X})$

is the smallest substructure of $\mathcal{M}$ containing both $\mathcal{N}$
and $\mathcal{N}^{\prime}$.

###### Proof.

We will write $\mathcal{N}_{\vee}$ for $\mathcal{N}\vee\mathcal{N}^{\prime}$.
By construction $\mathcal{N}_{\vee}$ contains both $\mathcal{N}$ and
$\mathcal{N}^{\prime}$. Let $\mathcal{T}$ be any substructure of $\mathcal{M}$
containing both $\mathcal{N}$ and $\mathcal{N}^{\prime}$. Clearly
$\left(\mathcal{N}_{\vee}\right)_{S}\subseteq\mathcal{T}_{S}$,
$\left(\mathcal{N}_{\vee}\right)_{S_{0}}\subseteq\mathcal{T}_{S_{0}}$,
$\mathcal{T}_{R}\subseteq\mathcal{T}_{R}$, and $\mathcal{T}_{L}$ extends
$\left(\mathcal{N}_{\vee}\right)_{L}$.

It remains to show that $\mathcal{N}_{\vee}$ is a substructure, i.e., that
$\mathcal{N}_{\vee}$ is total. Given a state $s_{1}$ in
$\left(\mathcal{N}_{v}ee\right)_{S}$, we know that either
$s\in\mathcal{N}_{S}$ or $s\in\mathcal{N}_{S}^{\prime}$. If
$s\in\mathcal{N}_{S}$, then there is an $t\in\mathcal{N}_{S}$ such that
$(s,t)\in\mathcal{N}_{T}\subseteq\left(\mathcal{N}_{\vee}\right)_{T}$. By
symmetry if $s\in\mathcal{N}_{S}^{\prime}$ then there is an
$t\in\mathcal{N}_{S}^{\prime}$ with
$(s,t)\in\left(\mathcal{N}_{\vee}\right)_{T}$. ∎

Given a finite set $X=\\{X_{0},X_{1},\dots,X_{n}\\}$ of substructures of
$\mathcal{M}$, we can define the structure $\bigvee X=X_{0}\vee
X_{1}\vee\dots\vee X_{n}$.

######  Lemma 4.5.

Let $\mathcal{M}$ be a Kripke structure and suppose that $\mathcal{N}$ and
$\mathcal{N}^{\prime}$ are substructures of $\mathcal{M}$. Then there is a
largest substructure of $\mathcal{M}$ contained in both $\mathcal{N}$ and
$\mathcal{N}^{\prime}$.

###### Proof.

The empty structure is contained in both $\mathcal{N}$ and
$\mathcal{N}^{\prime}$. Let $X$ be the collection of structures contained in
both $\mathcal{N}$ and $\mathcal{N}^{\prime}$. Then $\bigvee X$ is contained
in both $\mathcal{N}$ and $\mathcal{N}^{\prime}$ and is the largest
substructure of $\mathcal{M}$ contained in both $\mathcal{N}$ and
$\mathcal{N}^{\prime}$. ∎

######  Definition 4.6 (Join, Meet of substructures).

Let $\mathcal{N}^{\prime}$ and $\mathcal{N}^{\prime}$ be two substructures of
$\mathcal{M}$. The join of $\mathcal{N}$ and $\mathcal{N}^{\prime}$, written
$\mathcal{N}\vee\mathcal{N}^{\prime}$, is the smallest substructure of
$\mathcal{M}$ containing both $\mathcal{N}$ and $\mathcal{N}^{\prime}$. The
meet of $\mathcal{N}$ and $\mathcal{N}^{\prime}$, written
$\mathcal{N}\wedge\mathcal{N}^{\prime}$, is the largest substructure of
$\mathcal{M}$ contained in both $\mathcal{N}$ and $\mathcal{N}^{\prime}$.

We note that for two substructures $\mathcal{N}$ and $\mathcal{N^{\prime}}$ of
$\mathcal{M}$, the join $\mathcal{N}\lor\mathcal{N^{\prime}}$ has the simple
description as given in Lemma 4.4. However, the meet
$\mathcal{N}\land\mathcal{N^{\prime}}$, while well-defined, does not have such
a simple description. It is possible that for two substructure $\mathcal{N}$
and $\mathcal{N^{\prime}}$ of a Kripke structure $\mathcal{M}$, there are no
substructures contain in both $\mathcal{N}$ and $\mathcal{N^{\prime}}$. Hence
the largest substructure contained in both $\mathcal{N}$ and
$\mathcal{N^{\prime}}$ could be empty.

We can now define a lattice of substructures $\Lambda_{\mathcal{M}}$ for a
given structure $\mathcal{M}$.

######  Definition 4.7 (Lattice of Substructures).

Given a Kripke structure $\mathcal{M}$ the lattice of substructures of
$\mathcal{M}$ is

$\Lambda_{\mathcal{M}}=\left(\left\\{\mathcal{N}:\mathcal{N}\text{ is a
substructure of }\mathcal{M}\right\\},\leq\right),$

where the meet and join in $\Lambda_{\mathcal{M}}$ are the meet and join
defined for substructures earlier.

There is another lattice of substructures related to $\mathcal{M}$. Given a
subset $S^{\prime}\subseteq\mathcal{M}_{S}$ we can define the substructure
$\mathcal{N}=\langle S^{\prime}\rangle$ of $\mathcal{M}$ generated by
$S^{\prime}$ as the largest substructure $\mathcal{N^{\prime}}$ of
$\mathcal{M}$ such that $\mathcal{N^{\prime}}_{S}\subseteq S^{\prime}$,
equivalently

$\mathcal{N}=\bigvee_{\begin{subarray}{c}\mathcal{N^{\prime}}\leq\mathcal{M}\\\
\mathcal{N^{\prime}}_{S}\subseteq
S^{\prime}\end{subarray}}\mathcal{N^{\prime}}.$

##  5 Quotient structures.

Broadly speaking, a symmetry of an object captures the concept of what we mean
for two objects to be equal. For Kripke structures, we are in general not
interested in full symmetry. Instead, we are interested in a concept of
partial symmetry that allows for certain computations to take place. The
reason for this is because true symmetry of a Kripke structure would have to
act on not only the underlying state-space, but the set of atomic propositions
as well. We introduce a related concept, which we call a state-mapping. Some
authors call a ‘state-mapping’ a ‘symmetry’ of $\mathcal{M}$. Due to the
mathematical meaning of the word symmetry, we do not follow this tradition.

###  5.1 Groups Acting on Kripke Structures

######  Definition 5.1.

A state-mapping of $\mathcal{M}$ is a graph isomorphism of the state-space of
$\mathcal{M}$ such that its restriction to the initial states is also an
isomorphism, e.g., takes initial states to initial states. Formally, for a
Kripke structure $\mathcal{M}$, a state-mapping of $\mathcal{M}$ is a
bijection $f:\mathcal{M}_{S}\rightarrow\mathcal{M}_{S}$ such that:

  * •

$f(\mathcal{M}_{S_{0}})=\mathcal{M}_{S_{0}};$

  * •

For states $s,t\in\mathcal{M}_{S}$ we have that
$(s,t)\in\mathcal{M}_{T}\iff(f(s),f(t))\in\mathcal{M}_{T}$.

The set of all state-mappings of $\mathcal{M}$ forms a group.

######  Definition 5.2 ($G$-closed).

For a group $G$ of state-mappings of a Kripke structure $\mathcal{M}$, a
substructure $\mathcal{N}$ of $\mathcal{M}$ is called $G$-closed, if $G$ is a
group of state-mappings of $\mathcal{N}$, i.e., for every $g\in G$ and
$s\in\mathcal{N}_{S}$ we have $g(s)\in\mathcal{N}_{S}$.

######  Lemma 5.3.

Let $\mathcal{M}$ be a Kripke structure and let $G$ be a group of state
mappings of $\mathcal{M}$. Let $\mathcal{N},\mathcal{N^{\prime}}$ be two
$G$-closed substructures of $\mathcal{M}$. Then
$\mathcal{N}\lor\mathcal{N^{\prime}}$ and
$\mathcal{N}\land\mathcal{N^{\prime}}$ are both $G$-closed.

###### Proof.

We first show that $\mathcal{N}\vee\mathcal{N}^{\prime}$ is $G$-closed. Since
$(\mathcal{N}\vee\mathcal{N^{\prime}})_{S}=\mathcal{N}_{S}\cup\mathcal{N^{\prime}}_{S}$,
the group $G$ acts on the states of $\mathcal{N}\vee\mathcal{N^{\prime}}.$ We
will show that every element of $G$ is a state-mapping on
$\mathcal{N}\vee\mathcal{N^{\prime}}.$

Let $s,t\in(\mathcal{N}\vee\mathcal{N^{\prime}})_{S}$. If $g(s)=g(t)$ then
$s=t$ since $g$ is bijection on $\mathcal{M}_{S}$. Similarly, for any
$s\in(\mathcal{N}\vee\mathcal{N^{\prime}})_{S}$, since
$g^{-1}(s)\in(\mathcal{N}\vee\mathcal{N^{\prime}})_{S}$.

If $(s,t)\in(\mathcal{N}\vee\mathcal{N^{\prime}})_{T}$, then $(s,t)$ is in one
of $\mathcal{N}_{T}$ or $\mathcal{N^{\prime}}_{T}$. In either case,
$(g(s),g(t))$ is contained in the same set of transitions, and thus contained
in $(\mathcal{N}\vee\mathcal{N^{\prime}})_{T}$.

We now consider $\mathcal{N}\land\mathcal{N^{\prime}}$. Recall that
$\mathcal{N}\wedge\mathcal{N^{\prime}}$, is the largest substructure contained
in both $\mathcal{N}$ and $\mathcal{N^{\prime}}$. If
$s\in(\mathcal{N}\wedge\mathcal{N^{\prime}})_{S}$, and $g\in G$, then there is
a substructure of $\mathcal{N}$ and $\mathcal{N^{\prime}}$ containing $g(s)$.
Moreover as the largest substructure of $\mathcal{N}$ and
$\mathcal{N^{\prime}}$, $\mathcal{N}\wedge\mathcal{N^{\prime}}$ must contain
this substructure, hence $g(s)\in\mathcal{N}\wedge\mathcal{N^{\prime}}$.

Consider $(s,t)\in(\mathcal{N}\land\mathcal{N^{\prime}})_{T}$. Since $G$ is a
group of state mappings of $\mathcal{N}\land\mathcal{N^{\prime}}$ there is a
substructure of $\mathcal{N}$ and $\mathcal{N^{\prime}}$ containing
$(g(s),g(t))$. Since $\mathcal{N}\land\mathcal{N^{\prime}}$ is the join of all
substructures contained in $\mathcal{N}$ and $\mathcal{N^{\prime}}$, we
conclude that it must contain $(g(s),g(t))$ as well. ∎

By Lemma 5.3, we see that the $G$-closed substructures of $\mathcal{M}$ forms
a sublattice of $\Lambda_{\mathcal{M}}$.

######  Definition 5.4 (Lattice of $G$-closed substructures).

Given a Kripke structure $\mathcal{M}$ and a group $G$ of state mappings of
$\mathcal{M}$, the poset of $G$-closed substructures of $\mathcal{M}$ forms a
lattice. We call this lattice the lattice of $G$-closed substructures of
$\mathcal{M}$ and write it as $\Lambda_{\mathcal{M},G}$.

######  Example 5.5 (Example Box).

Let $\mathcal{M}$ be Example Box, i.e., the Kripke structure described in
Example 3.3. Let $g$ be the map that simultaneously switches $s_{1}$ and
$s_{2}$, and switches $t_{1}$ and $t_{2}$, i.e.
$g(s_{1})=s_{2},g(s_{2})=s_{1},g(t_{1})=t_{2},g(t_{2})=t_{1}$. Let $G$ be the
group consisting of $g$ and the identity map on $\mathcal{M}_{S}$. We note
that $G$ is not the entire group of state-mappings of $\mathcal{M}$. The
structure $\mathcal{M}$ has 10 $G$-closed substructures, including the empty
structure. We present these structures in Figure 3.

Figure 3: The nonempty $G$-closed substructure of Example Box. Where $G$ is
the group generated by the simultaneous swapping of indexes of both the
$s_{i}$ and the $t_{i}$.

As evidenced by Figure 3 in Example 5.5, a single Kripke structure can have
many $G$-closed substructures.

###  5.2 Constructing the Quotient Model

Give a group $G$ of state-mappings of a model $\mathcal{M}$, we want to
construct a quotient model $\mathcal{M}_{G}$. However, as noted, state-
mappings do not contain any information about $\mathcal{M}_{L}$. To remedy
this situation, we need a function that assigns a representative to each orbit
of $G$.

######  Definition 5.6 (Representative map).

Let $\mathcal{M}$ be a Kripke structure and suppose that $G$ is a group of
state-mappings of $\mathcal{G}$. A representative map of $\mathcal{M}$ with
respect to $G$ is a function
$\vartheta_{G}:\mathcal{M}_{S}\rightarrow\mathcal{M}_{S}$ satisfying the
following:

  * •

For all $s,s^{\prime}\in\mathcal{M}_{S}$, if there is a $g\in G$ such that
$g(s)=s^{\prime}$ then $\vartheta_{G}(s)=\vartheta_{G}(s^{\prime})$. (respects
orbits)

  * •

For all $s,s^{\prime}\in\mathcal{M}_{S}$, if there is no $g\in G$ such that
$g(s)=s^{\prime}$ then $\vartheta_{G}(s)\neq\vartheta_{G}(s^{\prime})$.
(separates orbits)

  * •

For all $s\in\mathcal{M}_{S}$, we have that
$\vartheta_{G}(\vartheta_{G}(s))=\vartheta_{G}(s)$, i.e., each orbit has a
stable representative. (idempotent)

We are now ready to define the quotient structure.

######  Definition 5.7 (Quotient structure).

Given a Kripke structure $\mathcal{M}$, a group $G$ of state-mappings of
$\mathcal{M}$, and a representative map $\vartheta_{G}$ of $\mathcal{M}$ with
respect to $G$, we define the quotient structure $\mathcal{M}/\vartheta_{G}$
of $\mathcal{M}$ with respect to $G$ and $\vartheta_{G}$ as follows:

The set of states of $\mathcal{M}/(G,\vartheta_{G})$ consists of the image of
$\vartheta_{G}$. We borrow the quotient notation from group theory and write
$\overline{\mathcal{M}}$ for $\mathcal{M}/(G,\vartheta_{G})$ and
$\overline{s}$ for $\vartheta_{G}(s)$.

We have $(\overline{s},\overline{t})\in\overline{\mathcal{M}}_{T}$ if and only
if there is some $s^{\prime}\in\mathcal{M}_{S}$ with
$\vartheta_{G}(s^{\prime})=\overline{s}$ and some
$t^{\prime}\in\mathcal{M}_{S}$ with $\vartheta_{G}(t^{\prime})=\overline{t}$
such that $(s^{\prime},t^{\prime})\in\mathcal{M}_{T}$.

An initial state of $\overline{\mathcal{M}}$ is the image under
$\vartheta_{G}$ of an initial state of $\mathcal{M}$.

We define $\overline{\mathcal{M}}_{L}:\overline{\mathcal{M}}_{S}\rightarrow
2^{AP}$ by
$\overline{\mathcal{M}}_{L}(\overline{s})=\mathcal{M}_{L}(\vartheta_{G}(s))$.

$\overline{\mathcal{M}}_{AP}=\mathcal{M}_{AP}.$

We note that the states of a quotient structure correspond exactly to the
orbits of states of the original structure. For transitions, we have a
slightly more subtle correspondence. Consider the following example:

######  Example 5.8 (Example Box).

Let $\mathcal{M}$ and $G$ be as in Example 5.5. Let $\vartheta_{G}$ be defined
by $\vartheta(x_{i})=x_{1}$ for $x\in\\{s,t\\}$. Then the quotient structure
$\mathcal{M}/(G,\vartheta_{G})$ has exactly 2 states,
$s_{1}=\vartheta_{G}(s_{1})=\vartheta_{G}(s_{2})$ and
$t_{1}=\vartheta_{G}(t_{1})=\vartheta_{G}(t_{2})$ with transitions
$(s_{1},t_{1}),(t_{1},s_{1})$. Every $G$-closed substructure $\mathcal{N}$ of
$\mathcal{M}$ in Figure 3, will map to this structure via

$\mathcal{N}\rightarrow\mathcal{N}/(G,\vartheta_{G}).$

Many of these substructures do no have $(s_{1},t_{1})$ as a transition at all.

As shown in Example 5.8, the existence of a transition in the quotient
structure, does not imply the existence of “the same” transition in the
original structure. However, it does imply the existence of a corresponding
transition in the original structure. Hence it is true that for every path
through a quotient structure there is a corresponding path through the
original Kripke structure. This property is what allows for model checking of
the original structure via model checking of the quotient. This path
correspondence is formalized in the below theorem which has appeared in many
texts. See for example the work by Emerson and Sistla [26, 3.1].

######  Theorem 5.9 (Path Correspondence Theorem).

Let $\mathcal{M}$ be a Kripke structure and let $G$ be a group of state-
mappings of $\mathcal{M}$. Let $\vartheta_{G}$ be any representative map of
$\mathcal{M}$ with respect of $G$. Write $\overline{\mathcal{M}}$ for
$\mathcal{M}/(G,\vartheta_{G})$. There is a bidirectional correspondence
between paths of $\mathcal{M}$ and paths of $\overline{\mathcal{M}}$. Formally
we have the following:

  1. 1.

If $x=s_{0},s_{1},s_{2},\dots$ is a path in $\mathcal{M}$, then
$\overline{x}=\overline{s_{0}},\overline{s_{1}},\overline{s_{2}},\dots$ is a
path in $\overline{\mathcal{M}}$ where
$\overline{s_{i}}=\vartheta_{G}(s_{i})$.

  2. 2.

If $\overline{x}=\overline{s_{0}},\overline{s_{1}},\overline{s_{2}},\dots$ is
a path in $\overline{\mathcal{M}}$, then for every state
$s^{\prime}_{0}\in\mathcal{M}_{S}$ such that
$\vartheta_{G}(s^{\prime}_{0})=\overline{s_{0}}$ there is a path
$s^{\prime}_{0},s^{\prime}_{1},s^{\prime}_{2},\dots$ such that
$\vartheta_{G}(s^{\prime}_{i})=\overline{s_{i}}$.

###### Proof.

1\. Given $(s_{i},s_{i+1})\in\mathcal{M}_{R}$, then
$(\overline{s_{i}},\overline{s_{i+1}})\in\overline{\mathcal{M}}_{R}.$

2\. Suppose that
$(\overline{s_{i}},\overline{s_{i+1}})\in\overline{\mathcal{M}}_{R}$. Then
there is some $(t,t^{\prime})\in\mathcal{M}_{R}$ with $t\in\overline{s_{i}}$
and $t^{\prime}\in\overline{s_{i+1}}.$ Suppose that we have a path
$s_{0}^{\prime},\dots,s_{i}^{\prime}$ such that
$s_{0}^{\prime}\in\overline{s_{0}}$,
$s_{1}^{\prime}\in\overline{s_{1}},\dots,s_{i}^{\prime}\in\overline{s_{i}}$
and
$(s_{0}^{\prime},s_{1}^{\prime}),(s_{1}^{\prime},s_{2}^{\prime}),\dots,(s_{i-1}^{\prime},s_{i}^{\prime})\in\mathcal{M}_{R}.$
Since both $t,s_{i}^{\prime}\in\overline{s_{i}}$, there is a group element
$g\in G$ such that $g(t)=s_{i}^{\prime}$. Then
$g(s_{0}^{\prime}),g(s_{1}^{\prime}),\dots,g(s_{i}^{\prime})=t,s_{i+1}$ is a
partial path in $\mathcal{M}$ Continuing in this manner we see the existence
of the desired path in $\mathcal{M}$. ∎

We would like to extend the path correspondence between $\mathcal{M}$ and
$\mathcal{M}/\left(G,\vartheta_{G}\right)$, for a group $G$ of state-mappings
of $\mathcal{M}$ and a representative map $\vartheta_{G}$ to one of
substructures of Kripke structures. To do this, we need to identify a
correspondence between $G$-closed substructures of $\mathcal{M}$ and
substructures of $\mathcal{M}/(G,\vartheta_{G})$. For $\mathcal{N}$ a
$G$-closed substructure of $\mathcal{M}$, there is a natural map
$\mathcal{N}\rightarrow\mathcal{N}/(G,\vartheta_{G})$, which we call the
quotient map. The quotient map establishes a lattice homomorphism between
$\Lambda_{\mathcal{M},G}$ and $\Lambda_{\mathcal{M}/(G,\vartheta_{G})}.$

We prove this property in a series of lemmas.

######  Lemma 5.10.

Let $\mathcal{M}$ be a Kripke structure and $G$ a group of state mappings of
$\mathcal{M}$ with representative map $\vartheta_{G}$. Then for every
substructure $\mathcal{N}$ of $\mathcal{M}/(G,\vartheta_{G})$, there is a
$G$-closed substructure $\mathcal{N^{\prime}}$ of $\mathcal{M}$ such that
$\mathcal{N^{\prime}}/(G,\vartheta_{G})=\mathcal{N}$.

###### Proof.

We will construct a $G$-closed substructure $\mathcal{N^{\prime}}$ of
$\mathcal{M}$ such that $\mathcal{N^{\prime}}/(G,\vartheta_{G})=\mathcal{N}$.
For the states of $\mathcal{N^{\prime}}$, we select exactly the $G$-orbits of
the representative states of $\mathcal{N}$, i.e.,
$\mathcal{N^{\prime}}_{S}=\\{g(s):\forall g\in G,s\in\mathcal{N}_{S}\\}$. For
transitions, we note that for every transition $(s,t)\in\mathcal{N}_{T}$ there
is at least one transition $(s^{\prime},t^{\prime})\in\mathcal{M}_{T}$ such
that $\vartheta(s^{\prime})=s$ and $\vartheta(t^{\prime})=t$. We add this
transition and its orbit under $G$ to $\mathcal{N^{\prime}}$. Hence for any
state $s^{\prime}\in\mathcal{N^{\prime}}_{S}$ there is a transition
$(s^{\prime},t^{\prime})$ for some $t^{\prime}\in\mathcal{N^{\prime}}_{S}$. We
conclude that $\mathcal{N^{\prime}}$ is total. Since $\mathcal{N^{\prime}}$ is
determined by its states and transitions as a substructure, the lemma is
proved. ∎

Lemma 5.10 establishes that the quotient map is surjective. The next lemma
demonstrates that it is a homomorphism of the join-semilattices
$\Lambda_{M,G}$ and $\Lambda_{M/(G,\vartheta_{G})}$. We note that it is not a
homomorphism of the lattices themselves, because the meet of two $G$-closed
structures mapping might be empty due to the requirement that Kripke
structures are total.

######  Lemma 5.11 (Quotient map respects join).

Let $\mathcal{M}$ be a Kripke structure and $G$ a group of state mappings of
$\mathcal{M}$ with representative map $\vartheta_{G}$. Let
$\mathcal{N},\mathcal{N^{\prime}}\in\Lambda_{\mathcal{M},G}$. Then

$(\mathcal{N}\lor\mathcal{N^{\prime}})/(G,\vartheta_{G})=\mathcal{N}/(G,\vartheta_{G})\lor\mathcal{N^{\prime}}/(G,\vartheta_{G}).$

###### Proof.

Clearly, by definition a state
$\vartheta_{G}(s)\in\left(\mathcal{N}/(G,\vartheta_{G})\lor\mathcal{N^{\prime}}/(G,\vartheta_{G})\right)_{S}$
if and only if it is in at least one of
$\left(\mathcal{N}/(G,\vartheta_{G})\right)_{S}$ or
$\left(\mathcal{N^{\prime}}/(G,\vartheta_{G})\right)_{S}$ which occurs if and
only if $\vartheta_{G}(s)$ is in one of the $G$-closed substructures
$\mathcal{N}$ or $\mathcal{N^{\prime}}$.

For transitions, we note that a transition in
$\left(\mathcal{N}/(G,\vartheta_{G})\lor\mathcal{N^{\prime}}/(G,\vartheta_{G})\right)_{T}$
is entirely contained in one of
$\left(\mathcal{N}/(G,\vartheta_{G})\right)_{T}$ or
$\left(\mathcal{N^{\prime}}/(G,\vartheta_{G})\right).$ Hence the transition
must come from either $\mathcal{N}$ or $\mathcal{N^{\prime}}$. ∎

As seen in Example 5.8, for a Kripke structure $\mathcal{M}$ with a group of
state-mappings $G$ of $\mathcal{M}$ and representative map $\vartheta_{G}$, it
is possible for multiple $G$-closed substructures of $\mathcal{M}$ to map to
the same substructure of the quotient structure
$\mathcal{M}/(G,\vartheta_{G})$.

Recall that the join of $G$-closed substructures of $M$ is $G$-closed.

######  Definition 5.12 ($G$-maximal).

Let $\mathcal{M}$ be a Kripke structure with group $G$ of state-mappings and
representative map $\vartheta_{G}$. A $G$-closed substructure $\mathcal{N}$ of
$\mathcal{M}$ is $G$-maximal if

$\mathcal{N}=\bigvee_{\begin{subarray}{c}\mathcal{N^{\prime}}\in\Lambda_{\mathcal{M},G}\\\
\mathcal{N^{\prime}}/(G,\vartheta_{G})\leq\mathcal{N}/(G,\vartheta_{G})\end{subarray}}\mathcal{N^{\prime}}.$

######  Lemma 5.13.

Let $\mathcal{M}$ be a Kripke structure and let $G$ be a group of state-
mappings of $\mathcal{M}$ with representative map $\vartheta_{G}$. Let
$\mathcal{M^{\prime}},\mathcal{M^{\prime\prime}}$ be two $G$-maximal
substructures of $\mathcal{M}$. Then
$\mathcal{M^{\prime}}\lor\mathcal{M^{\prime\prime}}$ is $G$-maximal.

###### Proof.

Consider a $G$-closed substructure $\mathcal{N^{\prime}}$ such that
$\mathcal{N^{\prime}}/(G,\vartheta_{G})\leq(\mathcal{M^{\prime}}\lor\mathcal{M^{\prime\prime}})/(G,\vartheta_{G})$.
Let $(s,t)\in\mathcal{N^{\prime}}_{T}$. Since
$(\vartheta_{G}(s),\vartheta_{G}(t))\in(\mathcal{M^{\prime}}\lor\mathcal{M^{\prime\prime}})/(G,\vartheta_{G})_{T}$
we conclude that $(\vartheta_{G}(s),\vartheta_{G}(t))$ is in either
$\mathcal{M^{\prime}}/(G,\vartheta_{G})$ or
$\mathcal{M^{\prime\prime}}/(G,\vartheta_{G})$. In either case, since
$\mathcal{M^{\prime}}$ and $\mathcal{M^{\prime\prime}}$ are both $G$-maximal
the transitions $(g(s),g(t))$ are already contained in $\mathcal{M^{\prime}}$
or $\mathcal{M^{\prime\prime}}$. ∎

######  Lemma 5.14.

Let $\mathcal{M}$ be a Kripke structure and let $G$ be a group of state-
mappings of $\mathcal{M}$ with representative map $\vartheta_{G}$. Let
$\mathcal{M^{\prime}},\mathcal{M^{\prime\prime}}$ be two $G$-maximal
substructures of $\mathcal{M}$. Then
$\mathcal{M^{\prime}}\land\mathcal{M^{\prime\prime}}$ is $G$-maximal.

###### Proof.

Suppose that $\mathcal{N}$ is the $G$-maximal substructure of $\mathcal{M}$
corresponding to
$(\mathcal{M^{\prime}}\land\mathcal{M^{\prime\prime}})/(G,\vartheta_{G})$. We
note that
$\mathcal{N}/(G,\vartheta_{G})\leq\mathcal{M^{\prime}}/(G,\vartheta_{G}).$
Hence $\mathcal{N}\leq\mathcal{M^{\prime}}$. By symmetry
$\mathcal{N}\leq\mathcal{M^{\prime\prime}}$ and thus
$\mathcal{N}\leq\mathcal{M^{\prime}}\land\mathcal{M^{\prime\prime}}.$ ∎

Combing Lemma 5.13 and 5.14 allows us to make the following definition.

######  Definition 5.15 ($G$-maximal lattice of substructures).

Let $\mathcal{M}$ be a Kripke structure and let $G$ be a group of state-
mappings of $\mathcal{M}$ with representative map $\vartheta_{G}$. Then the
set of $G$-maximal substructures of $\mathcal{M}$ forms a sublattice
$\Lambda_{\mathcal{M},G-\text{max}}$ of $\Lambda_{\mathcal{M}}$.

While in general the quotient map from $\Lambda_{\mathcal{M},G}$ to
$\Lambda_{\mathcal{M}/(G,\vartheta_{G})}$ is always surjective, when
restricted to $\Lambda_{\mathcal{M},G-\text{max}}$ the map is injective and a
lattice isomorphism.

######  Theorem 5.16 ($G$-Maximal Lattice Correspondence).

Let $\mathcal{M}$ be a Kripke structure and suppose that $G$ is a group of
state-mappings of $\mathcal{M}$ with a representative map $\vartheta_{G}$.
Then the map $f(\mathcal{N})=\mathcal{N}/\left(G,\vartheta_{G}\right)$ is an
isomorphism between the lattice of $G$-maximal substructures of $\mathcal{M}$
and the lattice of structures of $\mathcal{M}/\left(G,\vartheta_{G}\right)$.
That is $f$ is an isomorphism from $\Lambda_{M,G-\text{max}}$ to
$\Lambda_{M/(G,\vartheta_{G})}.$

###### Proof.

As noted the $G$-maximal lattice of substructures is in bijection with the
lattice of substructures of $\mathcal{M}/(G,\vartheta_{G})$. Since the meet
and join of two $G$-maximal structures are determined entirely by the meet and
join of their image in $M/(G,\vartheta_{G})$, the correspondence is a lattice
isomorphism. ∎

So far, our correspondence between models $\mathcal{M}$ and
$\mathcal{M}/\left(G,\vartheta_{G})\right)$ has been entirely syntactical. In
the next section we explore the semantic connections between $\mathcal{M}$ and
$\mathcal{M}/\left(G,\vartheta_{G}\right)$.

###  5.3 Semantic relationships between structures and quotient structures.

Let $G$ be a symmetry group of $\mathcal{M}$.

######  Definition 5.17.

A CTL formula $f$ is $G$-invariant over $\mathcal{M}$, if for every state $s$,
every $g\in G$, for all maximal propositional subformulae $P$ of $f$, we have

$\mathcal{M},s\models P\iff\mathcal{M},g(s)\models P.$

######  Lemma 5.18.

Let $G$ be a group of state-mappings for a Kripke structure $\mathcal{M}$. If
$f$ is $G$-invariant, then the valuation of $f$ in
$\overline{\mathcal{M}}=\mathcal{M}/\left(G,\vartheta_{G}\right)$ does not
depend on the choice of representative map $\vartheta_{G}$.

###### Proof.

Let $\vartheta_{G},\varphi_{G}$ be two representative maps with respect to
$G$. The quotients $\mathcal{M}/\left(G,\vartheta_{G}\right)$ and
$\mathcal{M}/\left(G,\varphi_{G}\right)$ have corresponding transition maps.
Moreover, for any maximal propositional subformula, $P$ of $f$ we have that

$\mathcal{M}/(G,\vartheta_{G}),\vartheta_{G}(s)\models
P\iff\mathcal{M}/\left(G,\varphi_{G}\right),\varphi_{G}(s)\models P.$

The valuation of $f$ depends only on the valuation of its maximal
propositional subformulae at all other states of the model. Since $\vartheta$
and $\varphi$ have the same evaluation of the maximal propositional
subformulae at all states, the evaluation of $f$ at all states is the same. ∎

This allows us to connect semantic statements about $\mathcal{M}$ with
semantic statements about $\mathcal{M}/(G,\vartheta_{G})$ for formulae that
are $G$-invariant.

If $G$ is a group of state-mappings of a structure $\mathcal{M}$ and
$\vartheta_{G}$ is a representative map of $G$, then the path correspondence
theorem establishes what we call a $G$-bisimulation between $\mathcal{M}$ and
the structure $\mathcal{M}/(G,\vartheta_{G})$.

######  Definition 5.19 ($G$-bisimulation).

Let $\mathcal{M}$ be a Kripke structure, $G$ be a group of state-mappings of
$\mathcal{M}$ with representative map $\vartheta_{G}$, and
$\overline{\mathcal{M}}$ be $\mathcal{M}/(G,\vartheta_{G})$. Let
$R\subseteq\mathcal{M}_{S}\times\overline{\mathcal{M}}_{S}$. Then $R$ is a
$G$-bisimulation between $\mathcal{M}$ and $\overline{\mathcal{M}}$ iff:

  1. 1.

If $(s,t)\in R$ then there exists $g\in G$ such that $t=g(s)$, i.e.,
$t=\vartheta_{G}(s)$;

  2. 2.

If $(s,t)\in R$ and $s\rightarrow s^{\prime}\in\mathcal{M}_{T}$, then there
exists $t^{\prime}$ such that $t\rightarrow
t^{\prime}\in\overline{\mathcal{M}}_{T}$ and $(s^{\prime},t^{\prime})\in R$

  3. 3.

If $(s,t)\in R$ and $t\rightarrow t^{\prime}\in\overline{\mathcal{M}}_{T}$,
then there exists $s^{\prime}$ such that $s\rightarrow
s^{\prime}\in\mathcal{M}_{T}$ and $(s^{\prime},t^{\prime})\in R$

######  Lemma 5.20.

Let $\mathcal{M}$ be a Kripke structure, $G$ be a group of state-mappings of
$\mathcal{M}$ with representative map $\vartheta_{G}$, and
$\overline{\mathcal{M}}$ be $\mathcal{M}/(G,\vartheta_{G})$. Let $\ \sim\
=(s,\overline{s})$ where $s\in\mathcal{M}_{S}$ and
$\overline{s}=\vartheta_{G}(s)$. Then $\ \sim\ $ is a $G$-bisimulation.

###### Proof.

We show that all clauses of Definition 5.19 hold. By definition of
$\vartheta_{G}$, $\overline{s}=g(s)$ for some $g\in G$, so Clause 1 holds.
Theorem 5.9 shows the existence of the corresponding transitions needed to
satisfy Clauses 2 and 3 of Definition 5.19. ∎

######  Lemma 5.21.

Let $\mathcal{M}$ be a Kripke structure, $G$ be a group of state-mappings of
$\mathcal{M}$ with representative map $\vartheta_{G}$, and
$\overline{\mathcal{M}}$ be $\mathcal{M}/(G,\vartheta_{G})$. Let
$s\in\mathcal{M}_{S}$, $t\in\overline{\mathcal{M}}S$, let $\ \sim\
=(s,\overline{s}$ where $s\in\mathcal{M}_{S}$ and
$\overline{s}=\vartheta_{G}(s)$. If $s\ \sim\ t$. Let $f$ be a $G$-invariant
CTL formula. Then $\mathcal{M},s\models f\iff\overline{\mathcal{M}},t\models
f$.

###### Proof.

Proof is by induction on the structure of CTL formulae, as given by the
grammar in Section 3.1.

Since $f$ is $G$-invariant over $\mathcal{M}$, then for all $t\in\mathcal{M}$
we have that $\mathcal{M},t\models P\mbox{ iff
}\overline{\mathcal{M}},\vartheta_{G}(t)\models P$, where $P$ is any maximal
propositional subformula of $f$.

This provides the base case for the induction, where $f$ is an atomic
proposition.

The induction step when $f$ has main operator one of $\neg,\land,\lor$ are
straightforward, and omitted. The induction steps when $f$ is one of
$\textup{{AX}}g$, $\textup{{EX}}g$ and $\textup{{A}}[g\textup{{\,R\,}}h]$ use
Definition 5.19 to establish the existence of the necessary transitions/paths.
The details are standard, see for example Theorem 3.2 in [4]. ∎

######  Lemma 5.22.

Let $\mathcal{M}$ be a Kripke structure, $G$ be a group of state-mappings of
$\mathcal{M}$ with representative map $\vartheta_{G}$, and
$\overline{\mathcal{M}}$ be $\mathcal{M}/(G,\vartheta_{G})$. Let $f$ be a
$G$-invariant CTL formula and $s\in\mathcal{M}_{S}$. Then
$\mathcal{M},s\models f\mbox{ iff
}\overline{\mathcal{M}},\vartheta_{G}(s)\models f$.

###### Proof.

By Lemma 5.20, $s\ \sim\ \vartheta_{G}(s)$. So, by Lemma 5.21,
$\mathcal{M},s\models f\mbox{ iff
}\overline{\mathcal{M}},\vartheta_{G}(s)\models f$. ∎

######  Definition 5.23 (Repair).

Given a structure $\mathcal{M}$ and a formula $f$, we call a nonempty
substructure $\mathcal{M^{\prime}}$ of $\mathcal{M}$ a repair of $\mathcal{M}$
with respect to $f$ if $\mathcal{M^{\prime}}\models f$.

If a CTL formula $f$ is $G$-invariant, then the lattice correspondence will
respect the valuation of $f$.

######  Theorem 5.24 (Repair Correspondence).

Let $\mathcal{M}$ be a Kripke structure, $G$ be a group of state-mappings of
$\mathcal{M}$ with a representative map $\vartheta_{G}$, and $f$ be a
$G$-invariant CTL formula.

Let $\mathcal{N}$ be a $G$-closed substructure of $\mathcal{M}$, and let
$\overline{\mathcal{N}}=\mathcal{N}/(G,\vartheta_{G})$. Then
$\mathcal{N},s\models f\iff\overline{\mathcal{N}},\vartheta_{G}(s)\models f$.

###### Proof.

We can show that $\mathcal{N}$ and $\overline{\mathcal{N}}$ are $G$-bisimilar
under the usual relation of each state $s$ in $\mathcal{N}_{S}$ with
$\vartheta_{G}(s)$ in $\overline{\mathcal{N}}_{S}$. ∎

It should be noted however that there are formulae $f$ and structures
$\mathcal{M}$, such that $f$ is $G$-invariant for some symmetry group $G$ of
$\mathcal{M}$ and there are no $G$-closed repairs of $f$, but there are
repairs that are not $G$-closed. That is, not every repairable structure has a
symmetric repair.

Theorem 5.24 gives us the commuting diagram in Figure 4.

Figure 4: Commutative diagram illustrating the connection between a structure
$\mathcal{M}$, a quotient structure $\overline{\mathcal{M}}$, and
substructures of $\overline{\mathcal{M}}$ satisfying a formula $f$ with
$G$-closed substructures of $\mathcal{M}$ satisfying $f$.

##  6 Repair of concurrent programs

We now apply the repair correspondence theorem to realize our goal: the repair
of concurrent programs. A concurrent program
$P=P_{1}\\!\parallel\\!\ldots\\!\parallel\\!P_{n}$ consists of $n$ sequential
processes executing in parallel. Each process $P_{i}$ is a set of _$i$
-actions_, i.e., tuples $(s_{i},B\rightarrow A,t_{i})$, where $s_{i},t_{i}$
are _local states_ of $P_{i}$, $B$ is a guard, and $A$ is an assignment to
shared variables. We say _action_ when we wish to ignore the identity of the
process that executes the action. Each $P_{i}$ has a local set of atomic
propositions $AP_{i}$ which it alone can modify, but other processes can read.
Each local state of $P_{i}$ determines as assignment of truth values to the
atomic propositions in $AP_{i}$. We set $AP=AP_{1}\cup\ldots\cup AP_{n}$. A
_global state_ $s=(s_{1},\ldots,s_{n},v_{1},\ldots,v_{m})$ of $P$ is a tuple
consisting of local states $s_{1},\ldots,s_{n}$ for processes
$P_{1},\ldots,P_{n}$ respectively, and values $v_{1},\ldots,v_{m}$ for shared
variables $x_{1},\ldots,x_{m}$. Define $s\\!\upharpoonright\\!i=s_{i}$ for
$i=1,\ldots,n$ and $s(x_{j})=v_{j}$ for $j=1,\ldots,m$. The truth values that
atomic propositions in $AP_{i}$ have in $s$ must be the same as those in
$s_{i}$. The states of Kripke structures that we have treated above are global
states as described here.

Given a concurrent program $P$ and a CTL formula $f$, we wish to modify $P$ to
produce a $P^{\prime}$ such that $\mathcal{M}\models f$, where $\mathcal{M}$
is the global state transition graph of $P^{\prime}$. The modification is
”subtractive”, that is, it only removes behaviors, it does not add behaviors
(which would be, in essence, a synthesis, and not a repair, algorithm). We
proceed as follows:

  1. 1.

Generate the symmetry-reduced state transition graph $\mathcal{N}$ of $P$. We
use the algorithm given by Figure 1 in [26], which is reproduced in Appendix
?.

  2. 2.

Repair $\mathcal{N}$ w.r.t. the given CTL specification $f$. Let
$\mathcal{N^{\prime}}$ be the repaired structure, so that
$\mathcal{N^{\prime}}\models f$.

  3. 3.

Extract a repaired concurrent program $P^{\prime}$ from $\mathcal{N^{\prime}}$

Steps 2 and 3 are given in the subsections below.

###  6.1 Repair of symmetry-reduced structures

We apply the model repair algorithm of [2] to the symmetry-reduced state
transition graph $\mathcal{N}$ of $P$, and the specification $f$ of $P$. This
algorithm is sound and complete, so that if $\mathcal{N}$ has some
substructure that satisfies $f$, then the algorithm will return such a
substructure $\mathcal{N^{\prime}}$. If not, the algorithm will report that no
repair exists, in which case there is no subtractive modification of $P$ which
satisfies $f$.

###  6.2 Extraction of concurrent programs from symmetry-reduced structures

We extract concurrent program $P^{\prime}$ from $\mathcal{N^{\prime}}$
following [15], by projecting each transition in
$s\mbox{$\,\stackrel{{\scriptstyle i}}{{\rightarrow}}\,$}t\in\mathcal{N}_{T}$
onto the process $P_{i}$ making the transition. For each
$s\mbox{$\,\stackrel{{\scriptstyle i}}{{\rightarrow}}\,$}t\in\mathcal{N}_{T}$
we define $action{(s\mbox{$\,\stackrel{{\scriptstyle
i}}{{\rightarrow}}\,$}t)}$ to be the $i$-action
$(s\\!\upharpoonright\\!i,B\rightarrow A,t\\!\upharpoonright\\!i)$ as follows.
The start, end states of this action are the projections of $s,t$ respectively
onto $P_{i}$. We define the guard
$B=``(\bigwedge_{Q\in\mathcal{N}_{L}(s)}Q)\land(\bigwedge_{Q\not\in\mathcal{N}_{L}(s)}\neg
Q)\land(\bigwedge_{x\in\mbox{$\cal SH$}}x=s(x))\mbox{\rm''}$ where $Q$ ranges
over $AP-AP_{i}$. When $P_{i}$ is in local state $s_{i}$, the guard $B$ checks
that the current global state is actually $s$. We define the assignment
$A=``/\\!/x:=t(x)\mbox{\rm''}$ where $x$ ranges over all shared variables such
that $t(x)\neq s(x)$. That is, $A$ makes the necessary updates to the shared
variables in moving from state $s$ to state $t$.

Let $AC=\\{action{(s\mbox{$\,\stackrel{{\scriptstyle
i}}{{\rightarrow}}\,$}t)}~{}|~{}s\mbox{$\,\stackrel{{\scriptstyle
i}}{{\rightarrow}}\,$}t\in\mathcal{N}_{T}\\}$, i.e., $AC$ is the set of
actions generated by all the transitions of $\mathcal{N}$. In principle, each
process $P^{\prime}_{i}$ of the repaired program $P^{\prime}$ can be set to be
the set of $i$-actions in $AC$. It is straightforward to show that
$P^{\prime}$ thus constituted generates exactly $\mathcal{N}$ as its global
state transition diagram. Since $\mathcal{N^{\prime}}\models f$, we also have
$P^{\prime}\models f$ as desired. However, even though $\mathcal{N^{\prime}}$
is total, it is possible for some processes in $P^{\prime}$ to have ”dead end”
local states from which they have no outgoing actions. We therefore repeatedly
apply some $g\in G$ to $AC$, until all such ”dead end” local states acquire at
least one outgoing action. One can continue this application of $g\in G$ to
$AC$ until no more actions are generated, which produces a ”$G$-closed”
program $P^{\prime}$. This is the ”largest” correct program that can be
produced as a repair of $P$. Using the largest program may increase the
available concurrency, but may produce a large number of actions, and so
increase the complexity of the repair procedure.

######  Theorem 6.1.

Let $\mathcal{N^{\prime}}$ be a repaired Kripke structure as above,
$P^{\prime}$ be a concurrent program extracted from $\mathcal{N^{\prime}}$ as
above, and $\mathcal{M^{\prime}}$ be the global state transition diagram of
$P^{\prime}$. Then every initial state of $\mathcal{M^{\prime}}$ is
$G$-bisimilar to some initial state of $\mathcal{N^{\prime}}$, and vice-versa.

###### Proof.

Let $\ \sim\ $ consist of the pairs $(s,t)$ such that
$s\in\mathcal{N^{\prime}}_{S}$, $t\in\mathcal{M}^{\prime}_{S}$, and $t=g(s)$
for some $g\in G$. The proof that $\ \sim\ $ is a $G$-bisimulation follows
from the definitions of program extraction and program execution semantics. By
the definitions of program extraction and program execution semantics,
$\mathcal{N^{\prime}}$ and $\mathcal{M^{\prime}}$ have isomorphic sets of
initial states, with corresponding states having the same labels. It follows
that these states are bisimilar. Hence $\ \sim\ $ is a $G$-bisimulation which
moreover relates each initial state of $\mathcal{N^{\prime}}$ to an initial
state of $\mathcal{M^{\prime}}$ and vice-versa. ∎

######  Lemma 6.2.

Let $\mathcal{N^{\prime}}$ be a Kripke structure as above that is repaired
w.r.t. a $G$-invariant CTL formula $f$. Let $P^{\prime}$ be a concurrent
program extracted from $\mathcal{N^{\prime}}$ as above, and
$\mathcal{M^{\prime}}$ be the global state transition diagram of $P^{\prime}$.
Then $\mathcal{M^{\prime}}\models f$.

###### Proof.

Since $\mathcal{N^{\prime}}$ is repaired w.r.t. $f$, we have
$\mathcal{N^{\prime}}\models f$ by Corollary 4.5 of [2]. Hence
$\mathcal{N^{\prime}},s_{0}\models f$ for every initial state $s_{0}$ of
$\mathcal{N^{\prime}}$. By Theorem 6.1, every initial state of
$\mathcal{M^{\prime}}$ is $G$-bisimilar to some initial state of
$\mathcal{N^{\prime}}$. Hence by Lemma 5.21,
$\mathcal{M^{\prime}},t_{0}\models f$ for every initial state $t_{0}$ of
$\mathcal{M^{\prime}}$. Hence $\mathcal{M^{\prime}}\models f$. ∎

##  7 Examples

###  7.1 Two process mutual exclusion

Figure 5 shows a Kripke structure $\mathcal{M}$ for mutual exclusion of two
processes $P_{1}$ and $P_{2}$. $P_{i}$ ($i=1,2$) can be in any of three local
states: $Ni$ (neutral, doing local computation), $Ti$ (trying, has requested
critical section entry), and $Ci$ (in the critical section). $\mathcal{M}$ has
exactly two symmetries: the identity map, and the map that swaps process
indices $1$ and $2$. We construct _the_ quotient model under this symmetry
group. The reduced structure
$\overline{\mathcal{M}}=\mathcal{M}/(G,\vartheta_{G})$ is also shown in Figure
5. Transitions of $P_{1}$, $P_{2}$ are shown in blue, red, respectively.
$\overline{\mathcal{M}}$ has a transition (shown in black) from state S6 to
S1, which is the quotient of the transition from S6 to S2 in $\mathcal{M}$,
i.e., $\vartheta_{G}(S6)=S6$ and $\vartheta_{G}(S2)=S1$ so the edge
$(\vartheta_{G}(S6),\vartheta_{G}(S1))$ occurs in $\overline{\mathcal{M}}$.

Consider the formula $\varphi=\textup{{AG}}\neg(C_{1}\land C_{2})$. Clearly,
$\mathcal{M}\not\models\varphi$. Since $\varphi$ is $G$-invariant, this is
equivalent to $\overline{\mathcal{M}}\not\models\varphi$ for any
representative map $\vartheta_{G}$. From the correspondence theorem, any
substructure of $\overline{\mathcal{M}}$ that satisfies $\varphi$ corresponds
to a $G$-maximal substructure of $\mathcal{M}$ that satisfies $\varphi$.

Figure 6 shows the repair of the reduced structure $\overline{\mathcal{M}}$,
and the resultant lifting of the repair to $\mathcal{M}$. The deleted
transitions and states are shown dashed.

Figure 5: The original model $\mathcal{M}$ and quotient
$\overline{\mathcal{M}}=\mathcal{M}/(G,\vartheta_{G})$.

Figure 6: The repair of $\overline{\mathcal{M}}$ and the lifting of the repair
to $\mathcal{M}$.

###  7.2 $N$-Process Mutual Exclusion

We now consider mutual exclusion for $N$-processes. To reduce clutter, we
remove the trying $(Ti)$ state, and we give a concrete example for 3 processes
— the generalization to $N$ processes is straightforward. We start with the
naïve concurrent program shown in Figure 7, where actions are labeled with the
trivial guard $\mathsf{true}$. The resulting Kripke structure is an
$N$-dimensional hypercube, and Figure 8 shows the structure $\mathcal{M}$ for
3-processes, along with the quotient
$\overline{\mathcal{M}}=\mathcal{M}/(G,\vartheta_{G})$. We consider the mutual
exclusion specification $\bigwedge_{i\neq j}\textup{{AG}}\neg(C_{i}\land
C_{j})$. The symmetry group $G$ for both structure and specification is the
full permutation group on the indices $\\{1,\ldots,N\\}$. For $N$-processes,
we have that the quotient model by the full group of symmetries has $N+1$
states, while the original model would have $2^{N}$ states. Figure 9 shows the
repair of the quotient $\overline{\mathcal{M}}$ and then the lifting of the
repair to the original structure $\mathcal{M}$. Figure 10 shows the correct
(repaired) program $P^{\prime}$ that is extracted from the repaired quotient
in Figure 9. For $N$ processes, the guard on actions of $P^{\prime}_{i}$ is
$\bigwedge_{j\neq i}N_{j}$.

Figure 7: The original program $P$

Figure 8: The original model $\mathcal{M}$ and quotient
$\overline{\mathcal{M}}=\mathcal{M}/(G,\vartheta_{G})$.

Figure 9: The repair of $\overline{\mathcal{M}}$ and the lifting of the repair
to $\mathcal{M}$. Figure 10: The repaired program $P^{\prime}$

##  8 Conclusions

We presented a theory for the substructures of a given Kripke structure
$\mathcal{M}$, their organization into lattices, and how these substructures
can interact with a group of state-mappings of $\mathcal{M}$. We showed the
existence of an isomorphism between the lattice $\Lambda_{M,G-\text{max}}$ of
$G$-maximal substructures of $\mathcal{M}$ and the lattice of substructures of
$\mathcal{M}(G,\vartheta_{G})$. Using this theory we were able to devise a
method for repairing concurrent programs which exploits symmetry.

## References

  * [1] Benjamin Aminof, Swen Jacobs, Ayrat Khalimov, and Sasha Rubin.  Parameterized model checking of token-passing systems.  In Kenneth L. McMillan and Xavier Rival, editors, Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings, volume 8318 of Lecture Notes in Computer Science, pages 262–281. Springer, 2014\.  doi:10.1007/978-3-642-54013-4\\_15.
  * [2] Paul C. Attie, Kinan Dak-Al-Bab, and Mouhammad Sakr.  Model and program repair via SAT solving.  ACM Trans. Embed. Comput. Syst., 17(2):32:1–32:25, 2018.  doi:10.1145/3147426.
  * [3] Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder.  Decidability of Parameterized Verification.  Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2015.  doi:10.2200/S00658ED1V01Y201508DCT013.
  * [4] Michael C. Browne, Edmund M. Clarke, and Orna Grümberg.  Characterizing finite kripke structures in propositional temporal logic.  Theoretical computer science, 59(1-2):115–131, 1988.
  * [5] F. Buccafurri, T. Eiter, G. Gottlob, and N. Leone.  Enhancing model checking in verification by AI techniques.  Artif. Intell., 112:57–104, 1999.
  * [6] M. Carrillo and D.A. Rosenblueth.  A method for ctl model update, representing kripke structures as table systems.  IJPAM, 52:401–431, 2009.
  * [7] G. Chatzieleftheriou, B. Bonakdarpour, S.A. Smolka, and P. Katsaros.  Abstract model repair.  In AlwynE. Goodloe and Suzette Person, editors, NASA Formal Methods, volume 7226 of Lecture Notes in Computer Science, pages 341–355. Springer Berlin Heidelberg, Norfolk, VA, USA, 2012.
  * [8] Edmund M. Clarke, E. Allen Emerson, Somesh Jha, and A. Prasad Sistla.  Symmetry reductions in model checking.  In CAV, volume 1427 of Lecture Notes in Computer Science, pages 147–158. Springer, 1998.
  * [9] Edmund M. Clarke, E. Allen Emerson, and A. Prasad Sistla.  Automatic verification of finite-state concurrent systems using temporal logic specifications.  ACM Trans. Program. Lang. Syst., 8(2):244–263, 1986.
  * [10] Edmund M. Clarke, Orna Grumberg, and Somesh Jha.  Verifying parameterized networks.  ACM Trans. Program. Lang. Syst., 19(5):726–750, 1997.  doi:10.1145/265943.265960.
  * [11] Edmund M. Clarke, Somesh Jha, Reinhard Enders, and Thomas Filkorn.  Exploiting symmetry in temporal logic model checking.  Formal Methods Syst. Des., 9(1/2):77–104, 1996.  doi:10.1007/BF00625969.
  * [12] Edmund M. Clarke, Muralidhar Talupur, Tayssir Touili, and Helmut Veith.  Verification by network decomposition.  In Philippa Gardner and Nobuko Yoshida, editors, CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings, volume 3170 of Lecture Notes in Computer Science, pages 276–291. Springer, 2004.  doi:10.1007/978-3-540-28644-8\\_18.
  * [13] Edmund M. Clarke, Muralidhar Talupur, and Helmut Veith.  Environment abstraction for parameterized verification.  In E. Allen Emerson and Kedar S. Namjoshi, editors, Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings, volume 3855 of Lecture Notes in Computer Science, pages 126–141. Springer, 2006.  doi:10.1007/11609773\\_9.
  * [14] E. Allen Emerson.  Temporal and modal logic.  In Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pages 995–1072. Elsevier and MIT Press, 1990.
  * [15] E. Allen Emerson and Edmund M. Clarke.  Using branching time temporal logic to synthesize synchronization skeletons.  Sci. Comput. Program., 2(3):241–266, 1982.
  * [16] E. Allen Emerson, John Havlicek, and Richard J. Trefler.  Virtual symmetry reduction.  In LICS, pages 121–131. IEEE Computer Society, 2000.
  * [17] E. Allen Emerson and Vineet Kahlon.  Reducing model checking of the many to the few.  In CADE, volume 1831 of Lecture Notes in Computer Science, pages 236–254. Springer, 2000.
  * [18] E. Allen Emerson and Vineet Kahlon.  Model checking large-scale and parameterized resource allocation systems.  In TACAS, volume 2280 of Lecture Notes in Computer Science, pages 251–265. Springer, 2002.
  * [19] E. Allen Emerson and Vineet Kahlon.  Exact and efficient verification of parameterized cache coherence protocols.  In CHARME, volume 2860 of Lecture Notes in Computer Science, pages 247–262. Springer, 2003.
  * [20] E. Allen Emerson and Vineet Kahlon.  Model checking guarded protocols.  In LICS, pages 361–370. IEEE Computer Society, 2003.
  * [21] E. Allen Emerson and Vineet Kahlon.  Rapid parameterized model checking of snoopy cache coherence protocols.  In TACAS, volume 2619 of Lecture Notes in Computer Science, pages 144–159. Springer, 2003.
  * [22] E. Allen Emerson and Kedar S. Namjoshi.  Reasoning about rings.  In POPL, pages 85–94. ACM Press, 1995.
  * [23] E. Allen Emerson and Kedar S. Namjoshi.  Automatic verification of parameterized synchronous systems (extended abstract).  In CAV, volume 1102 of Lecture Notes in Computer Science, pages 87–98. Springer, 1996.
  * [24] E. Allen Emerson and Kedar S. Namjoshi.  Verification of parameterized bus arbitration protocol.  In CAV, volume 1427 of Lecture Notes in Computer Science, pages 452–463. Springer, 1998.
  * [25] E. Allen Emerson and Kedar S. Namjoshi.  On reasoning about rings.  Int. J. Found. Comput. Sci., 14(4):527–550, 2003.
  * [26] E Allen Emerson and A Prasad Sistla.  Symmetry and model checking.  Formal methods in system design, 9(1):105–131, 1996.
  * [27] E. Allen Emerson and A. Prasad Sistla.  Utilizing symmetry when model-checking under fairness assumptions: An automata-theoretic approach.  ACM Trans. Program. Lang. Syst., 19(4):617–638, 1997.
  * [28] E. Allen Emerson and Richard J. Trefler.  Model checking real-time properties of symmetric systems.  In MFCS, volume 1450 of Lecture Notes in Computer Science, pages 427–436. Springer, 1998.
  * [29] E. Allen Emerson and Richard J. Trefler.  From asymmetry to full symmetry: New techniques for symmetry reduction in model checking.  In CHARME, volume 1703 of Lecture Notes in Computer Science, pages 142–156. Springer, 1999.
  * [30] E. Allen Emerson and Thomas Wahl.  Dynamic symmetry reduction.  In TACAS, volume 3440 of Lecture Notes in Computer Science, pages 382–396. Springer, 2005.
  * [31] Javier Esparza, Alain Finkel, and Richard Mayr.  On the verification of broadcast protocols.  In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pages 352–359. IEEE Computer Society, 1999\.  doi:10.1109/LICS.1999.782630.
  * [32] Steven M. German and A. Prasad Sistla.  Reasoning about systems with many processes.  J. ACM, 39(3):675–735, 1992.  doi:10.1145/146637.146681.
  * [33] Nouraldin Jaber, Swen Jacobs, Christopher Wagner, Milind Kulkarni, and Roopsha Samanta.  Parameterized verification of systems with global synchronization and guards.  In Shuvendu K. Lahiri and Chao Wang, editors, Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I, volume 12224 of Lecture Notes in Computer Science, pages 299–323. Springer, 2020.  doi:10.1007/978-3-030-53288-8\\_15.
  * [34] B. Jobstmann, A. Griesmayer, and R. Bloem.  Program repair as a game.  In CAV, pages 226–238, Berlin, Heidelberg, 2005. Springer-Verlag.
  * [35] S. Staber, B. Jobstmann, and R. Bloem.  Finding and fixing faults.  In CHARME ’05, pages 35–49, Berlin, Heidelberg, 2005. Springer-Verlag.  Springer LNCS no. 3725.
  * [36] Christian von Essen and Barbara Jobstmann.  Program repair without regret.  Formal Methods Syst. Des., 47(1):26–50, 2015.  doi:10.1007/s10703-015-0223-6.

##  Appendix A CTL Semantics

######  Definition A.1.

$\mathcal{M},s\models\varphi$ means that formula $\varphi$ is true in state
$s$ of structure $M$, and $\mathcal{M},s\not\models\varphi$ means that
$\varphi$ is false in $s$.

  1. 1.

$\mathcal{M},s\models\mathsf{true}$ and
$\mathcal{M},s\not\models\mathsf{false}$

  2. 2.

$\mathcal{M},s\models p\text{ iff }p\in L(s)$ where atomic proposition $p\in
AP$

  3. 3.

$\mathcal{M},s\models\neg\varphi$ iff  $\mathcal{M},s\not\models\varphi$

  4. 4.

$M,s\models\varphi\land\psi\text{ iff }\mathcal{M},s\models\varphi\text{ and
}M,s\models\psi$

  5. 5.

$M,s\models\varphi\lor\psi\text{ iff }\mathcal{M},s\models\varphi\text{ or
}M,s\models\psi$

  6. 6.

$\mathcal{M},s\models\textup{{AX}}\varphi\text{ iff }\text{ for all $t$ such
that }(s,t)\in T:(\mathcal{M},t)\models\varphi$

  7. 7.

$M,s\models\textup{{EX}}\varphi\text{ iff }\text{ there exists $t$ such that
}(s,t)\in T\text{ and }(\mathcal{M},t)\models\varphi$

  8. 8.

$\mathcal{M},s\models\textup{{A}}[\varphi\textup{{\,R\,}}\psi]\text{ iff
}\text{ for all fullpaths $\pi=s_{0},s_{1},\ldots$ starting from $s=s_{0}$: }$
$\forall k\geq 0:(\forall j<k:\mathcal{M},s_{j}\not\models\varphi)\text{
implies }\mathcal{M},s_{k}\models\psi$

  9. 9.

$\mathcal{M},s\models\textup{{E}}[\varphi\textup{{\,R\,}}\psi]\text{ iff
}\text{ for some fullpath $\pi=s_{0},s_{1},\ldots$ starting from $s=s_{0}$: }$
$\forall k\geq 0:(\forall j<k:\mathcal{M},s_{j}\not\models\varphi)\text{
implies }\mathcal{M},s_{k}\models\psi$