Model and Program Repair via Group Actions

Abstract

Given a textual representation of a finite-state concurrent program $P$, one can construct the corresponding Kripke structure $\mathcal {M}$. However, the size of $\mathcal {M}$ can be exponentially larger than the textual size of $P$. This state explosion can make model checking properties of $P$ via $\mathcal {M}$ expensive or even infeasible. The action of a symmetry group $G$ on $\mathcal {M}$ can be used to produce a smaller Kripke structure $\overline{\mathcal {M}}$. Various authors have exploited the direct correspondence between $\mathcal {M}$ and $\overline{\mathcal {M}}$ to perform model checking. When the structure $\mathcal {M}$ does not satisfy a formula, one can look for a substructure that will satisfy the formula. We call this substructure-repair: identifying a substructure $\mathcal {N}$ of $\mathcal {M}$ that satisfies a given temporal logic formula.

In this paper we extend previous work by showing that repairs of $\overline{\mathcal {M}}$ lift to repairs of $\mathcal {M}$. In other words, we can repair a computer program $P$, which exhibits a high degree of symmetry, by repairing the smaller Kripke structure $\overline{\mathcal {M}}$ and then symmetrizing the corresponding program. To do this we arrange the substructures of $\mathcal {M}$ and $\overline{\mathcal {M}}$ into substructure lattices that are ordered by substructure inclusion. We show that the substructures of $\mathcal {M}$ preserved by $G$ form a (sub)lattice that maps to the substructure lattice of $\overline{\mathcal {M}}$. When restricted to the lattice of substructures of $\mathcal {M}$ that are “maximal” with the action of $G$ on $\mathcal {M}$, the above map is a lattice isomorphism.

These results enable us to repair $\overline{\mathcal {M}}$ and then to lift the repair to $\mathcal {M}$. In cases where a program has a high degree of symmetry, such as in many concurrent programs, we can repair the program by repairing the small Kripke structure $\overline{\mathcal {M}}$.

1 Introduction

To model check a program $P,$ one first constructs a Kripke structure $\mathcal {M}$. In general, the Kripke structure $\mathcal {M}$ is generated by all potential executions of $P$. The model checking problem for a program $P$ w.r.t. a temporal logic formula $\varphi$ is to verify that the Kripke structure $\mathcal {M}$ generated by the execution of $P$ satisfies $\varphi$ [8]. A major obstacle to model checking a concurrent program via its Kripke structure is state explosion: in general, the size of $\mathcal {M}$ is exponential in the number of processes n. As studied by Emerson and Sistla [18] and extended by others [10, 14, 21], the use of symmetry reduction to ameliorate state-explosion can yield a significant reduction in the complexity of model checking $\mathcal {M}\,\models \,\varphi$ when both $\mathcal {M}$ and $\varphi$ have a high degree of symmetry in the process index set $\{1,\ldots ,n\}$.

For a Kripke structure $\mathcal {M}$, we capture the symmetry of $\mathcal {M}$ using the group $G$ of automorphisms of both $\mathcal {M}$ and $\varphi$. The quotient structure $\overline{\mathcal {M}}= \mathcal {M}/G$ of $\mathcal {M}$ by $G$ often has significantly fewer states than $\mathcal {M}$. Since $\overline{\mathcal {M}}$ can be computed directly from the original $P$, we avoid the expensive computation of the large structure $\mathcal {M}$. Model checking $\overline{\mathcal {M}}\,\models \,\varphi$ is linear in the size of $\overline{\mathcal {M}}$ [8], so this provides significant savings if $\overline{\mathcal {M}}$ is small, i.e., if $G$ is large.

If , then we can search for a model $\mathcal {N}$ related to $\mathcal {M}$ such that $\mathcal {N}\models f$. In this paper we focus on substructure-repair: we require $\mathcal {N}$ to be a substructure of $\mathcal {M}$. The key idea behind substructure-repair is to remove execution paths which violate required properties, e.g., paths that lead to a violation of mutual exclusion. We give examples in Section 6 of different properties and substructure repairs with respect to these properties. Substructure-repairs can always repair $\mathcal {M}$ w.r.t. all universal properties (those expressible using universal path quantification [26]).¹

1.1 Our Contributions

We present a theory of substructures of Kripke structures. Using this theory we establish an evaluation preserving correspondence between certain substructures of the original Kripke structure $\mathcal {M}$ and the substructures of the quotient structure $\overline{\mathcal {M}}$ (this is Theorem 2). This correspondence is a functorial form of bisimilarity between a certain lattice of substructures of $\mathcal {M}$ and the lattice of substructures of $\overline{\mathcal {M}}$. Hence for a given formula $\varphi$, substructure-repairs of $\overline{\mathcal {M}}$ with respect to $\varphi$ can be lifted to substructure-repairs of $\mathcal {M}$ with respect to $\varphi$ (this is Theorem 3). This correspondence of Kripke substructures lattices is of independent mathematical interest as an example of a monotone Galois connection.

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

The rest of the paper proceeds as follows: Section 3 contains the formal definition of Kripke structures and substructures. In Section 4, after briefly recalling group actions, we show how one can use a group to obtain a quotient $\overline{\mathcal {M}}$ of $\mathcal {M}$ and the repair correspondence between $\mathcal {M}$ and $\overline{\mathcal {M}}$. We extend our results to the repair of concurrent programs in Section 5. Section 6 presents some examples. In particular, we show that a structure $\mathcal {M}$ might have a nonempty repair even if the quotient $\overline{\mathcal {M}}$ does not. In Section 7 we examine what classes of Kripke structures and what types of formulae guarantee the existence of quotient based repairs.

2 Related Work

Our work combines model/program repair [5, 25, 29, 32] and symmetry reductions via group actions[7, 10, 16, 18,19,20,21,22]. Le Goues et al.  [25] provides a modern introduction to program repair; although their results generally relate to program repair based on the textual representation of the program. Our approach repairs a Kripke structure w.r.t. a computation tree logic (CTL) formula and uses that to repair the corresponding program.

2.1 Computation Tree Logic Repair

Buccafuri 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. [29] and Staber et. al. [32] used game-based repair methods for programs and circuits, although their method is complete for invariants only.

Chatzieleftheriou et. al. [6] repair abstract structures, using Kripke modal transition systems and 3-valued CTL semantics. Von Essen and Jobstmann [23] 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.

The work of Attie et al.  [2] establishes that repair by abstraction can avoid state explosion. However, repairs of abstracted structures do not always lift to repairs of the original structure. Within networks, Namjoshi and Trefler [30] have shown that a combination of abstraction and group actions can be used to produce smaller structures.

2.2 Group theoretic model checking

Group theoretic approaches to symmetry-reduction in model checking began in 1995 with work by Emerson and a collection of coauthors [7, 10, 14, 16, 18,19,20,21,22] compute the quotient $\mathcal {M}/G$ and model check $\mathcal {M}/G$, instead of the original (much larger) structure $\mathcal {M}$. The group theoretic approach to model checking works because $\mathcal {M}$ and $\mathcal {M}/G$ are bisimilar with respect to certain formulae.

A requirement for group theoretic model checking or repair is calculating the group of symmetries in question. We will see that larger groups of symmetries result in smaller quotient models. Clarke et al. [7] showed that calculating the orbit of a group action, a part of model checking via symmetry, is at least as difficult as graph isomorphism. However, in many practical cases concurrent programs have a natural symmetry by swapping certain processes. Hence many concurrent programs have a small known symmetry group in advance. Donaldson and Miller [11] showed that there is a process to build a larger symmetry group for a program from a smaller symmetry group.

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) [1, 9, 24], and rings of processes, where all communication is between a process and its neighbors in the ring [9, 15, 17].

3 Temporal Logic and Kripke Structures

Computation tree logic (CTL) is a propositional branching-time temporal logic used to model the possible computational branches taken by a system [12, 13]. The semantics of $\textrm{CTL}$ are defined with respect to a Kripke structure.

Definition 1 (Kripke structure)

A Kripke structure $\mathcal {M}$ is a tuple $\left( S, S_0, T, L, AP\right)$ where $S$ is a finite set of states, $S_0\subseteq S$ is a set of initial states, $T\subseteq (S\times S)$ is a transition relation, $AP$ is a finite 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: $\forall s \in S, \exists t \in S: (s,t) \in T$, and that $S\ne \emptyset$ implies $S_0\ne \emptyset$. Also, different states have different labels: $s \ne t \Rightarrow L(s) \ne L(t)$. We admit the empty Kripke structure, i.e., $S= \emptyset$, due to mathematical necessity.

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$. We will write $s\rightarrow t$ in this case. A path $\pi$ in $\mathcal {M}$ is a (finite or infinite) sequence of states, $\pi =s_{0}, s_{1}, \ldots$, such that $\forall i \ge 0: (s_i,s_{i+1}) \in T$.

To model the behavior of a concurrent program $P= P_1,\ldots ,P_n$, we define a special type of Kripke structure: a multiprocess Kripke structure is one in which the set of atomic propositions $AP$ is partitioned into disjoint subsets $AP_1,\ldots ,AP_n$, states have the form $(s_1,\ldots ,s_n)$ and transitions T are partitioned into disjoint subsets $T_1,\ldots ,T_n$. The set of atomic propositions “owned” by $P_i$ is denoted by $AP_i$: they can only be changed by $P_i$, but can be read by other processes. The local state of $P_i$ is written as $s_i$, and is labelled by the subset of $AP_i$ whose propositions are true in $s_i$. Then, the truth value of $p \in AP_i$ in global state $(s_1,\ldots ,s_n)$ is given by its value in local state $s_i$. $T_i$ gives the transitions of process $P_i$, which are denoted as $s \, {\mathop {\rightarrow }\limits ^{i}} \, t$. For state $s = (s_1,\ldots ,s_n)$, define $s \upharpoonright i = s_i$, and $s \downarrow i = (s_1,\ldots ,s_{i-1},s_{i+1},\ldots ,s_n)$. We then require $s \downarrow i = t \downarrow i$ for every transition $s \, {\mathop {\rightarrow }\limits ^{i}} \, t$, i.e., transitions by $P_i$ do not change atomic propositions of other processes.

A CTL formula $\varphi$ is evaluated (i.e., is true or false) in a state s of a Kripke structure $\mathcal {M}$ [13]. We 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}$. The formal definition of $\,\models \,$, proceeds by induction on the structure of CTL formulae [12, 13] and is omitted for space reasons.

Fig. 1.

The Box Kripke structure.

Example 1 (Example Box) The “Box” Kripke structure in Figure 1 has 4 states and transitions as shown. Its set of atomic propositions is empty, and so all states have empty labels, as indicated by “()”. There is a natural group acting on this Kripke structure, i.e., the group generated by the action which exchanges the state $\textbf{s1}$ with $\textbf{s2}$, and the state $\textbf{t1}$ with $\textbf{t2}$.

The theory of substructures presented below is motivated by the concept of a substructure-repair of a structure $\mathcal {M}$ with respect to a formula f, i.e., a substructure $\mathcal {N}$ of $\mathcal {M}$ such that $\mathcal {N}\models f$.

Definition 2

(Substructure, $\le$). Given Kripke structures $\mathcal {M}$ and $\mathcal {N}$, we say that $\mathcal {N}$ is a substructure of $\mathcal {M}$, denoted $\mathcal {N}\le \mathcal {M}$, iff the following all hold:

• 1. $\mathcal {N}_{S}\subseteq \mathcal {M}_{S}$.

• 2. $\mathcal {N}_{S_0}= \mathcal {M}_{S_0}\cap \mathcal {M}'_{S}$.

• 3. $\mathcal {N}_T\subseteq \mathcal {M}_T$.

• 4. $\mathcal {N}_{AP}= \mathcal {M}_{AP}$.

• 5. $\mathcal {N}_{L}= \mathcal {M}_{L}\upharpoonright S'$ (where $\upharpoonright$ denotes domain restriction).

• 6. For all $s \in \mathcal {N}_{S}$ there is a $t \in \mathcal {N}_{S}$ such that $(s,t) \in \mathcal {N}_T$, i.e., $\mathcal {N}$ is total.

For mathematical necessity in what follows, we allow for the ‘empty’ substructure. We do not, however, accept an empty substructure as a valid repair. It is immediate that $\le$ is a reflexive partial order. Lemmas 1 and 2 below imply that the substructures of $\mathcal {M}$ can be regarded as a lattice, with join and meet operations as follows.

Lemma 1

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

$$\begin{aligned} \mathcal {N}\vee \mathcal {N}'= (\mathcal {N}_{S}\cup \mathcal {N}'_{S},\, \mathcal {N}_{S_0}\cup \mathcal {N}'_{S_0},\, \mathcal {N}_T\cup \mathcal {N}'_T,\, \mathcal {M}_{L}\upharpoonright (\mathcal {N}_{S}\cup \mathcal {N}'_{S}),\, \mathcal {M}_{AP}) \end{aligned}$$

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

Given a nonempty finite set $X=\{X_0,X_1,\dots ,X_n\}$ of substructures of $\mathcal {M}$, we define the structure $\bigvee X = X_0 \vee X_1 \vee \cdots \vee X_n$.

Lemma 2

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

Definition 3 (Join, Meet of Substructures)

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

The join $\mathcal {N}\vee \mathcal {N}'$ has a simple description as given in Lemma 1. However, the meet $\mathcal {N}\wedge \mathcal {N}'$, while well-defined, does not have such a simple description. It is possible that for two substructures $\mathcal {N}$ and $\mathcal {N}'$ of a Kripke structure $\mathcal {M}$, there are no non-empty substructures contained in both $\mathcal {N}$ and $\mathcal {N}'$. Hence the largest substructure contained in both $\mathcal {N}$ and $\mathcal {N}'$ could be empty.

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

Definition 4 (Lattice of Substructures)

Given a Kripke structure $\mathcal {M}$ the lattice of substructures of $\mathcal {M}$ is $\mathrm {\Lambda }_\mathcal {M}= \left( \left\{ \mathcal {N}: \mathcal {N}\text { is a substructure of } \mathcal {M}\right\} , \le \right)$ where the meet and join in $\mathrm {\Lambda }_\mathcal {M}$ are as given in Definition 3.

4 Quotient Structures

We capture the symmetry in a Kripke structure $\mathcal {M}$ with the notion of state-mapping: a graph isomorphism on $\mathcal {M}$ which preserves initial states. State-mappings also preserve paths since they are isomorphisms. We ignore for now the labelling function $\mathcal {M}_{L}$, i.e., which atomic propositions hold in which states, and concern ourselves only with the graph structure of $\mathcal {M}$. Since the atomic proposition labelling obviously affects the truth of CTL formulae in states of $\mathcal {M}$, it must be accounted for. We do this below using the notion of $G$-invariant CTL formula. Thus, we decompose the symmetry characterization of $\mathcal {M}$ into two separate concerns: the graph structure of $\mathcal {M}$, handled using state-mapping, and the atomic proposition labelling of states of $\mathcal {M}$, handled using $G$-invariant CTL formulae.

A type of symmetry of particular interest is the symmetry of a multiprocess Kripke structure w.r.t. the process indices $1,\ldots ,n$ of the corresponding concurrent program $P_1 \!\parallel \!\cdots \!\parallel \!P_n$, as we illustrate below. Our theory, however, applies to Kripke structures in general.

4.1 Groups Acting on Kripke Structures

Definition 5

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, i.e., 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. This means that the composition of any two state-mappings is another state-mapping and for any state-mapping f on $\mathcal {M}$ there is another state-mapping g on $\mathcal {M}$ such that $f(g(s)) = s$ and $g(f(s)) = s$. We refer to the manuscripts by Issacs [27, 28], and Serre [31] for a more in-depth introduction to group theory.

Definition 6

($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 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}'$ be two $G$-closed substructures of $\mathcal {M}$. Then $\mathcal {N}\vee \mathcal {N}'$ and $\mathcal {N}\wedge \mathcal {N}'$ are both $G$-closed.

By Lemma 3, we see that the $G$-closed substructures of $\mathcal {M}$ form a sublattice of $\mathrm {\Lambda }_\mathcal {M}$. This is a proper sublattice in that the meet and join operations are the same as those of $\mathrm {\Lambda }_\mathcal {M}$.

Definition 7

(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 the lattice of $G$-closed substructures of $\mathcal {M}$ and write it as $\mathrm {\Lambda }_{\mathcal {M},G}$.

Example 1 (Example Box)

Let $\mathcal {M}$ be Example Box, i.e., the Kripke structure presented in Figure 1. Let g be the map that simultaneously switches $\mathbf {s_1}$ and $\mathbf {s_2}$, and switches $\mathbf {t_1}$ and $\mathbf {t_2}$, i.e., $g(\mathbf {s_1}) = \mathbf {s_2}$, $g(\mathbf {s_2}) = \mathbf {s_1}$, $g(\mathbf {t_1}) = \mathbf {t_2}$, $g(\mathbf {t_2}) = \mathbf {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 some of these structures in Figure 2.

Fig. 2.

Four $G$-closed substructures of Example Box. Where $G$ is the group generated by the simultaneous swapping of indexes of both the $\mathbf {s_i}$ and the $\mathbf {t_i}$. Note that each of the structures is a substructure of the substructure to the right. Looking ahead to Definition 10, only the entire structure (d) is $G$-maximal.

4.2 Constructing the Quotient structure

Given a group $G$ of state-mappings of a structure $\mathcal {M}$, we want to construct a quotient structure $\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, where for $s \in \mathcal {M}_{S}$ the orbit of s is $\{g(s): g \in G\}$.

Definition 8 (Representative map)

Let $\mathcal {M}$ be a Kripke structure and suppose that $G$ is a group of state-mappings of $\mathcal {M}$. 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' \in \mathcal {M}_{S}$, if there is some $g \in G$ such that $g(s) = s'$ then $\vartheta _{G}(s) = \vartheta _{G}(s')$. (respects orbits)

• For all $s, s' \in \mathcal {M}_{S}$, if there is no $g \in G$ such that $g(s) = s'$ then $\vartheta _{G}(s) \ne \vartheta _{G}(s')$. (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 define $\vartheta _{G}(S) = \{ \vartheta _{G}(s) ~|~s \in S \}$.

Definition 9 (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 $\overline{\mathcal {M}}= \mathcal {M}/(G,\vartheta _{G})$ of $\mathcal {M}$ with respect to $G$ and $\vartheta _{G}$ as follows, where we write $\overline{s}$, $\overline{t}$ for $\vartheta _{G}(s)$, $\vartheta _{G}(t)$, respectively:

• $\overline{\mathcal {M}}_{S}= \vartheta _{G}(\mathcal {M}_{S})$, i.e., the states of $\overline{\mathcal {M}}$ are the image under $\vartheta _{G}$ of the states of $\mathcal {M}$.

• $\overline{\mathcal {M}}_{T}$ consists of all $(\overline{s},\overline{t})$ such that there exist $s \in \mathcal {M}_{S}$ with $\vartheta _{G}(s) = \overline{s}$ and $t \in \mathcal {M}_{S}$ with $\vartheta _{G}(t) = \overline{t}$ such that $(s,t)\in \mathcal {M}_T$.

• $\overline{\mathcal {M}}_{S_0}= \vartheta _{G}(\mathcal {M}_{S_0})$, i.e., the initial states of $\overline{\mathcal {M}}$ are the image under $\vartheta _{G}$ of the initial states of $\mathcal {M}$.

• $\overline{\mathcal {M}}_{L}(\overline{s}) = \mathcal {M}_{L}(\overline{s})$, i.e., the label of a state in $\overline{\mathcal {M}}$ is the same as its label in $\mathcal {M}$.

• $\overline{\mathcal {M}}_{AP}= \mathcal {M}_{AP}$, i.e., $\overline{\mathcal {M}}$ has the same atomic propositions as $\mathcal {M}$.

Thus the states of a quotient structure correspond exactly to the orbits of states of the original structure under the group of state mappings. For transitions, we have a slightly more subtle correspondence. Consider the following examples:

Example 2

In Figure 3 we demonstrate the correspondence between Kripke structures, $G$-closed substructures, and their quotients. In the figure, we present a multiprocess Kripke structure $\mathcal {M}$ corresponding to two concurrent processes $P_1$ (atomic propositions and transitions in blue) and $P_2$ (atomic propositions and transitions in red). The group $G$ of state mappings swaps the indexes of the processes. This structure has a $G$-closed substructure $\mathcal {N}$ constructed by removing the ‘center’ state $\mathbf {u_0}$. Define $\vartheta _{G}$ to take the ‘left-most’ state in the orbit, i.e., $\vartheta _{G}(\mathbf {t_1}) = \mathbf {t_0}$, $\vartheta _{G}(\mathbf {t_5}) = \mathbf {t_2}$, $\vartheta _{G}(\mathbf {u_0})= \mathbf {u_0}$, $\vartheta _{G}(\mathbf {t_6}) = \mathbf {t_3}$, $\vartheta _{G}(\mathbf {t_4}) = \mathbf {t_4}$. The quotient structure $\mathcal {M}/(G,\vartheta _{G})$ appears in the top right. While the quotient structure is isomorphic to a substructure of $\mathcal {M}$, this is not always the case. (See Figure 6 in Example 5 for an example where the quotient gains a new transition.) The quotient structure $\mathcal {N}/(G,\vartheta _G|\mathcal {N}_S)$ appears in the bottom right.

Example 3 (Example Box)

Let $\mathcal {M}$ and $G$ be as in Example 1. Let $\vartheta _{G}$ be defined by $\vartheta _{G}(\mathbf {s_1}) = \vartheta _{G}(\mathbf {s_2}) = \mathbf {s_1}$ and $\vartheta _{G}(\mathbf {t_1})=\vartheta _{G}(\mathbf {t_2}) = \mathbf {t_1}$. Then the quotient structure $\mathcal {M}/(G,\vartheta _{G})$ has exactly 2 states, $\mathbf {s_1}$ and $\mathbf {t_1}$ with transitions $(\mathbf {s_1},\mathbf {t_1}),(\mathbf {t_1},\mathbf {s_1})$. Also, the $G$-closed substructure substructures of $\mathcal {M}$ given in Figure 2 (a), (b), and (c) also map to this quotient structure via $\mathcal {N}\rightarrow \mathcal {N}/(G,\vartheta _{G})$. Note that the transition $(\mathbf {t_1},\mathbf {s_1})$ is present in the quotient, but is not present, for example, in the structure of Figure 2 (b). However, the “corresponding” transition $(\mathbf {t_2},\mathbf {s_1})$ is present in Figure 2 (b).

Fig. 3.

As discussed in Example 2, we have a Kripke structure in the top left and a G-closed substructure in the bottom left. On the right, we have the quotients of the whole structure (top) and the G-closed substructure (bottom).

In the sequel, we fix 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$.

Example 3 shows that many $G$-closed substructures can have the same quotient structure, and also that, in general, a transition in the quotient may not itself be present in the original structure. We show, however, in Theorem 1 below that a “corresponding” transition is guaranteed to be present in the original structure. These corresponding transitions can be joined into a path which corresponds state-by-state to the path in the quotient. This “path correspondence” is what allows for model checking of $\mathcal {M}$ via model checking of $\overline{\mathcal {M}}$ and is formalized in the following theorem from Emerson and Sistla [18, 3.1].

Theorem 1

(Path Correspondence Theorem). There is a bidirectional correspondence between paths of $\mathcal {M}$ and paths of $\overline{\mathcal {M}}$. Formally we have the following:

• 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. 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'_0 \in \mathcal {M}_{S}$ such that $\vartheta _{G}(s'_0) = \overline{s_0}$ there is a path $s'_0, s'_1, s'_2,\dots$ in $\mathcal {M}$ such that $\vartheta _{G}(s'_i) = \overline{s_i}$.

We now extend the path correspondence between $\mathcal {M}$ and $\overline{\mathcal {M}}$ to a correspondence between $G$-closed substructures of $\mathcal {M}$ and substructures of $\overline{\mathcal {M}}$. Define $\mathrm {\Psi }: \mathrm {\Lambda }_{\mathcal {M},G} \rightarrow \mathrm {\Lambda }_{\overline{\mathcal {M}}}$, by $\mathrm {\Psi }(\mathcal {N}) = \mathcal {N}/(G,\vartheta _{G})$, so that $\mathrm {\Psi }$ maps a $G$-closed substructure $\mathcal {N}$ of $\mathcal {M}$ to a corresponding substructure of $\overline{\mathcal {M}}$. We call $\mathrm {\Psi }$ the quotient map. $\mathrm {\Psi }$ establishes a join-semilattice homomorphism between $\mathrm {\Lambda }_{\mathcal {M},G}$ and $\mathrm {\Lambda }_{\overline{\mathcal {M}}}$ as we now show in the following series of lemmas.

Lemma 4

For every substructure $\overline{\mathcal {N}}$ of $\overline{\mathcal {M}}$, there is a $G$-closed substructure $\mathcal {N}$ of $\mathcal {M}$ such that $\mathcal {N}/(G,\vartheta _{G})= \overline{\mathcal {N}}$.

Lemma 4 establishes that $\mathrm {\Psi }$ is surjective. We note that every substructure $\overline{\mathcal {N}}$ of $\overline{\mathcal {M}}$ defines a set of states of $\overline{\mathcal {M}}$, i.e., the orbits of the states in $\overline{\mathcal {N}}$. However, in general, the transitions of $\overline{\mathcal {N}}$ do not uniquely define transitions in $\overline{\mathcal {M}}$.

The next lemma demonstrates that $\mathrm {\Psi }$ is a homomorphism of the join-semilattices $\mathrm {\Lambda }_{M,G}$ and $\mathrm {\Lambda }_{\overline{\mathcal {M}}}$. We note that it is not a homomorphism of the lattices themselves because the meet of two $G$-closed structures mapping might be empty.

Lemma 5 (Quotient map respects join)

Let $\mathcal {N},\mathcal {N}'\in \mathrm {\Lambda }_{\mathcal {M},G}$. Then

$$\begin{aligned} \mathrm {\Psi }(\mathcal {N}\vee \mathcal {N}') = \mathrm {\Psi }(\mathcal {N}) \vee \mathrm {\Psi }(\mathcal {N}'). \end{aligned}$$

As seen in Example 3, it is possible for multiple $G$-closed substructures of $\mathcal {M}$ to map to the same substructure of the quotient structure $\overline{\mathcal {M}}$. To obtain a single well-defined preimage for each substructure of the quotient structure, we introduce the concept of $G$-maximal. Recall that the join of $G$-closed substructures of $\mathcal {M}$ is $G$-closed.

Definition 10

($G$-maximal). A $G$-closed substructure $\mathcal {N}$ of $\mathcal {M}$ is $G$-maximal if

$$ \mathcal {N}= \bigvee _{\begin{array}{c} \mathcal {N}'\in \mathrm {\Lambda }_{\mathcal {M}, G}\\ \mathcal {N}'/(G,\vartheta _{G})\le \mathcal {N}/(G,\vartheta _{G}) \end{array}} \mathcal {N}'. $$

That is, $\mathcal {N}$ is the join of all $G$-closed substructures of $\mathcal {M}$ whose quotient is a substructure of the quotient of $\mathcal {N}$ itself, namely of $\mathcal {N}/(G,\vartheta _{G})$. A $G$-closed substructure $\mathcal {N}$ fails to be $G$-maximal exactly when there are states $s,t \in \mathcal {N}$, such that $(s,t)\in \mathcal {N}/(G,\vartheta _{G})$, but (s, t) is not in $\mathcal {N}$.

Among all of the $G$-closed substructures in Figure 2 only the entire structure itself is $G$-maximal

Lemma 6

Let $\mathcal {M'},\mathcal {M''}$ be two $G$-maximal substructures of $\mathcal {M}$. Then $\mathcal {M'}\vee \mathcal {M''}$ is $G$-maximal and $\mathcal {M'}\wedge \mathcal {M''}$ is $G$-maximal.

Lemma 6 allows us to make the following definition.

Definition 11

($G$-maximal lattice of substructures). The set of $G$-maximal substructures of $\mathcal {M}$ forms a sublattice $\mathrm {\Lambda }_{\mathcal {M},G-\text {max}}$ of $\mathrm {\Lambda }_\mathcal {M}$.

While in general the quotient map from $\mathrm {\Lambda }_{\mathcal {M},G}$ to $\mathrm {\Lambda }_{\overline{\mathcal {M}}}$ is always surjective, when restricted to $\mathrm {\Lambda }_{\mathcal {M},G-\text {max}}$, the map is injective and is a lattice isomorphism.

Theorem 2

($G$-Maximal Lattice Correspondence). The restriction of the quotient map $\mathrm {\Psi }$ to $\mathrm {\Lambda }_{\mathcal {M},G-\text {max}}$ is an isomorphism from $\mathrm {\Lambda }_{\mathcal {M},G-\text {max}}$ to $\mathrm {\Lambda }_{\overline{\mathcal {M}}}$, i.e., between the lattice of $G$-maximal substructures of $\mathcal {M}$ and the lattice of structures of $\overline{\mathcal {M}}$.

At this point, we would like to remind the reader of the various lattices that we have defined and how they relate to each other:

$$ \underbrace{G\text {-maximal substructures}}_{\mathrm {\Lambda }_{\mathcal {M},G-\text {max}}} \subseteq \underbrace{G\text {-closed substructures}}_{\mathrm {\Lambda }_{\mathcal {M},G}} \subseteq \underbrace{\text {All substructures}}_{\mathrm {\Lambda }_\mathcal {M}}. $$

4.3 Semantic Relationships Between Structures and Quotient Structures

Definition 12

Let $G$ be a group of state mappings of $\mathcal {M}$. A CTL formula $\varphi$ is $G$-invariant over $\mathcal {M}$, if for every state s, every $g \in G$, for all maximal propositional subformulae $\varphi '$ of $\varphi$, we have

$$\begin{aligned} \mathcal {M}, s \,\models \,\varphi ' \iff \mathcal {M}, g(s) \,\models \,\varphi '. \end{aligned}$$

Lemma 7

If $\varphi$ is $G$-invariant, then the valuation of $\varphi$ in $\overline{\mathcal {M}}$ does not depend on the choice of representative map $\vartheta _G$.

This allows us to connect semantic statements about $\mathcal {M}$ with semantic statements about $\overline{\mathcal {M}}$ for formulae that are $G$-invariant. The path correspondence theorem establishes a bisimulation between $\mathcal {M}$ and $\overline{\mathcal {M}}$, in which state s of $\mathcal {M}$ and state $\overline{s}$ of $\overline{\mathcal {M}}$ are bisimilar iff s is in the orbit of $\overline{s}$, i.e., $s = g(\overline{s})$ for some $g \in G$. We call such a bisimulation a $G$-bisimulation. Hence, $G$-bisimilar states satisfy the same propositional subformulae of any $G$-invariant CTL formula $\varphi$. A straightforward induction over path length then shows that s and $\overline{s}$ satisfy the same $G$-invariant CTL formulae:

Corollary 1

$\mathcal {M}\,\models \,\varphi$ iff $\overline{\mathcal {M}}\,\models \,\varphi$ for all $G$ invariant CTL formulae $\varphi$.

Lemma 8

Let $s \in \mathcal {M}_{S}$, $t \in \overline{\mathcal {M}}_S$. Let $\varphi$ be a $G$-invariant CTL formula. If $t=\vartheta _G(s)$, then $\mathcal {M}, s \,\models \,\varphi \iff \overline{\mathcal {M}}, t \,\models \,\varphi$.

Section 3 developed the theory of substructures of a Kripke structure. This development was motivated by the following definition and theorem.

Definition 13 (Substructure-Repair)

Given a structure $\mathcal {M}$ and a CTL formula $\varphi$, we call a nonempty substructure $\mathcal {N}$ of $\mathcal {M}$ a substructure-repair of $\mathcal {M}$ with respect to $\varphi$ if $\mathcal {N}\,\models \,\varphi .$

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

Theorem 3

(Repair Correspondence). Let $\varphi$ be a $G$-invariant CTL formula. Let $\mathcal {N}$ be a non-empty $G$-closed substructure of $\mathcal {M}$, $s \in \mathcal {N}_{S}$, and $\overline{\mathcal {N}}= \mathcal {N}/(G,\vartheta _{G})$. Then $\mathcal {N}, s \,\models \,\varphi \iff \overline{\mathcal {N}}, \vartheta _{G}(s) \,\models \,\varphi$.

5 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 $(s_i, B, t_i)$, where $s_i, t_i$ are local states of $P_i$ and B is a guard (a predicate on the global state). We say action when we ignore the process id. We assume a given set $S_0$ of initial states. The program $P_1 \!\parallel \!\cdots \!\parallel \!P_n$ generates a transition $s \, {\mathop {\rightarrow }\limits ^{i}} \, t$ iff $P_i$ contains an action $(s_i,B,t_i)$ such that $s \upharpoonright i = s_i$, $t \upharpoonright i = t_i$, and $s(B) = true$, where s(B) is the value of guard B in global state s. The transition updates only atomic propositions in $AP_i$, and so $s \downarrow i = t \downarrow i$. The state-transition graph of $P$ is the closure of this “transition generation” operation, starting in the initial state set $S_0$.

Given a concurrent program $P$ and a CTL formula $\varphi$, we wish to modify $P$ to produce a repaired program $P^{r}$ such that $\mathcal {M'}\,\models \,\varphi$, where $\mathcal {M'}$ is the state-transition graph of $P^{r}$. The modification is “subtractive”, that is, it only removes behaviors and does not add them. We assume henceforth that when $\mathcal {M}$ is a multiprocess Kripke structure over process indices $1,\ldots ,n$, that the symmetry group $G$ is a subgroup of $\textsf{S}_n$, the group of permutations on $\{1,\ldots ,n\}$.

5.1 Repair of Symmetry-reduced Structures

We first generate the symmetry-reduced state transition graph $\overline{\mathcal {M}}$ of $P$. We use the algorithm of Emerson and Sistla [18, Figure 1]. We then apply the model repair algorithm of Attie et. al. [2] to $\overline{\mathcal {M}}$, and the specification $\varphi$ of $P$. This algorithm is sound and complete, so that if $\overline{\mathcal {M}}$ has some substructure that satisfies $\varphi$, then the algorithm will return such a substructure $\overline{\mathcal {N}}$. If not, the algorithm will report that no repair exists. As noted, applying this algorithm to the symmetry-reduced state transition graph is only complete with respect to the symmetric repairs, see Example 6.3.

5.2 Extraction of Concurrent Programs from Symmetry-reduced Structures

We want to extract a repaired concurrent program from $\overline{\mathcal {N}}$ using the projection method of [4, 13]: each transition $s \, {\mathop {\rightarrow }\limits ^{i}} \, t$ is turned into an i-action $action{(s \, {\mathop {\rightarrow }\limits ^{i}} \, t)} \triangleq (s \upharpoonright i, B, t \upharpoonright i)$, with guard where ” and Q ranges over $AP$. When process i is in local state $s_i$, guard B checks that the current global state is actually s.

A key problem is that the definition of the quotient $\overline{\mathcal {M}}$ allows transitions in which the atomic propositions of more than one process are changed, since any representative of an orbit can be chosen. Hence the repaired $\overline{\mathcal {N}}\le \overline{\mathcal {M}}$ can also contain such transitions, e.g., the transition from S6 to S1 in Figure 6 below, which we write as $[C_1\, T_2] \rightarrow [T_1\, N_2]$. Note that the propositions of both processes 1 and 2 are changed. To generate i-actions, such transitions must be converted so that only the atomic propositions of a single process are modified.

Define a transition from s to t to be regular iff it modifies atomic propositions in at most one $AP_i$, so that $s \downarrow i = t \downarrow i$ for some process index i, and write the transition as $s \, {\mathop {\rightarrow }\limits ^{i}} \, t$. Also define a transition from s to t to be irregular iff it is not regular, i.e., it modifies atomic propositions in more than one $AP_i$, and write the transition as $s \rightarrow t$, with no process index labelling the arrow.

For each irregular transition $s \rightarrow t \in \overline{\mathcal {N}}_{T}$, there is $g' \in G$ such that $s \rightarrow g'(t)$ is regular. Such an element $g'$ always exists. Let $\overline{s} \rightarrow \overline{t} \in \overline{\mathcal {M}}_{T}$ for arbitrary $\overline{\mathcal {M}}_{T}$. By Definition 9, there exists $s \rightarrow t \in \mathcal {M}_T$ such that $\overline{s} = \vartheta _{G}(s)$ and $\overline{t} = \vartheta _{G}(t)$. Hence there is some $g \in G$ such that $g(s) = \overline{s}$ since s and $\overline{s}$ are in the same orbit. Since g is a symmetry of $\mathcal {M}$, we have $g(s) \rightarrow g(t) \in \mathcal {M}_T$. Hence $\overline{s} \rightarrow g(t) \in \mathcal {M}_T$. Now $t = h(\overline{t})$ for some $h \in G$ since t and $\overline{t}$ are in the same orbit. Hence $\overline{s} \rightarrow g(h(\overline{t})) \in \mathcal {M}_T$, and so the needed $g'$ is the product of g and h. For example, by applying the permutation of process indices 1, 2 to $[T_1\, N_2]$, from the irregular transition $[C_1\, T_2] \rightarrow [T_1\, N_2]$ we extract the regular transition $[C_1\, T_2] \, {\mathop {\rightarrow }\limits ^{1}} \, [N_1\, T_2]$.

Define $Reg _{i}(\overline{\mathcal {N}}_{T})$ to be the set of regular transitions $s \, {\mathop {\rightarrow }\limits ^{i}} \, g(t)$ such that $g \in G$ and $s \rightarrow t \in \overline{\mathcal {N}}_{T}$. Since g can be the identity element of $G$, it follows that this account for both regular and irregular transitions in $\overline{\mathcal {N}}_{T}$. Define $Act _{i}(\overline{\mathcal {N}}_{T}) = \{ action{(s \, {\mathop {\rightarrow }\limits ^{i}} \, t)} ~|~s \, {\mathop {\rightarrow }\limits ^{i}} \, t \in Reg _{i}(\overline{\mathcal {N}}_{T}) \}$, be the set of actions obtained from $Reg _{i}(\overline{\mathcal {N}}_{T})$.

Define the action of $g \in G$ on syntactic elements of $P_i$ as follows. For local state $s_i$: $g(s_i) = s_{g(i)}$. For atomic proposition $Q_i$: $g(Q_i) = Q_{g(i)}$. For guard B, by induction: $g(\lnot B) = \lnot g(B)$ and $g(B1 \wedge B2) = g(B1) \wedge g(B2)$, with the base case given by $g(Q_i)$ above. For i-action $(s_i, B, t_i)$: $g(s_i, B, t_i) = (g(s_i), g(B), g(t_i))$. That is, we apply g to all process indices in the syntactic element. Now define $Act ^{G}_{i}(\overline{\mathcal {N}}_{T})$, the symmetrization of $Act _{i}(\overline{\mathcal {N}}_{T})$, by $Act ^{G}_{i}(\overline{\mathcal {N}}_{T}) = \{ g(a) ~|~g \in G, a\in Act _{j}(\overline{\mathcal {N}}_{T}), g(j) = i \}$. The repaired concurrent program arises from process-wise repair $\overline{P}^{G}= \overline{P}_{1}^{G} \!\parallel \!\cdots \!\parallel \!\overline{P}_{n}^{G}$, where $\overline{P}_{i}^{G}$ consists of the i-actions in $Act ^{G}_{i}(\overline{\mathcal {N}}_{T})$.

Theorem 4

Let $\overline{P}^{G}$ be the concurrent program extracted from $\overline{\mathcal {N}}$ as above, let $\mathcal {N}^p$ be the state transition graph generated by the execution of $\overline{P}^{G}$, and let $\overline{\mathcal {N}^p} = \mathcal {N}^p/(G,\vartheta _{G})$. Then $\mathcal {N}^p$ is G-closed and $\overline{\mathcal {N}^p} = \overline{\mathcal {N}}$.

Corollary 2

Let $\overline{P}^{G}$ be the repaired program and $\varphi$ the CTL specification that was used to repair $\overline{\mathcal {M}}$, resulting in $\overline{\mathcal {N}}$. Then $\overline{P}^{G}\,\models \,\varphi$.

6 Examples

6.1 Two process Mutual Exclusion

We consider mutual exclusion for two processes $P_1$, $P_2$. Each $P_i$ has three local states: $N_i$ (neutral, computing locally), $T_i$ (trying, has requested critical section entry), and $C_i$ (in the critical region). We start with the “trivial” program $P$ shown in Figure 4 in which all action guards are “true” and apply the program repair algorithm of Section 5 to repair this program w.r.t. the specification $\varphi = \textsf {AG} \lnot (C_1 \wedge C_2) \wedge \textsf {AG} ( (T_1 \vee T_2) \Rightarrow \textsf {AF} (C_1 \vee C_2) )$. The first conjunct specifies mutual exclusion of the critical sections (safety) and the second specifies progress: if some process requests the critical section then some process will obtain it (liveness). Figure 5 (left side) shows the Kripke structure $\mathcal {M}$ generated by execution of $P$. Transitions of $P_1$, $P_2$ are shown in blue, red, respectively. Clearly, . Actually both conjuncts are violated: $\textsf {AG} \lnot (C_1 \wedge C_2)$ due to the reachability of state S8 from the initial state, and $\textsf {AG} ( (T_1 \vee T_2) \Rightarrow \textsf {AF} (C_1 \vee C_2) )$ due to the self loop on state S4.

$\mathcal {M}$ has exactly two symmetries: the identity map, and the map that swaps process indices 1 and 2. Our program repair algorithm does not generate $\mathcal {M}$ since $\mathcal {M}$ may be large, and we show $\mathcal {M}$ only for exposition. We generate $\overline{\mathcal {M}}= \mathcal {M}/(G,\vartheta _{G})$ directly from $P$, and we show $\overline{\mathcal {M}}$ in Figure 5 (right side). $\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}(\textbf{S6}) = \textbf{S6}$ and $\vartheta _{G}(\textbf{S2}) = \textbf{S1}$ so the edge $(\vartheta _{G}(\textbf{S6}), \vartheta _{G}(\textbf{S2}))$ occurs in $\overline{\mathcal {M}}$.

Figure 6 shows the repair $\overline{\mathcal {N}}$ 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 7 shows the repaired concurrent program $\overline{P}^{G}$ that is extracted from $\overline{\mathcal {N}}$. Note that $\oplus$ means disjunction [3]. By Corollary 2, $\overline{P}^{G}\,\models \,\varphi$.

Fig. 4.

Initial incorrect mutual exclusion program from Section 6.1.

6.2 n-Process Mutual Exclusion

We now consider mutual exclusion for n-processes. To reduce clutter, we remove the trying $\textbf{Ti}$ state, and we give a concrete example for 3 processes — the generalization to n processes is straightforward. Each process can move directly from N to C with the appropriate indexes, i.e., the guards on all actions are initially “true”, just like in Figure 4.

Fig. 5.

The original model $\mathcal {M}$ and quotient $\overline{\mathcal {M}}= \mathcal {M}/(G,\vartheta _{G})$ for the Kripke structures in Section 6.1.

Fig. 6.

The repair of $\overline{\mathcal {M}}$ and the lifting of the repair to $\mathcal {M}$ from Section 6.1.

Fig. 7.

The mutual exclusion concurrent program extracted from $\mathcal {M}$ in Figure 6.

We consider the mutual exclusion specification $\bigwedge _{i \ne j} \textsf {AG} \lnot (C_i \wedge C_j)$. The group of state mappings $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 8 shows the repair of the quotient $\overline{\mathcal {M}}$ and then the lifting of the repair to the original structure $\mathcal {M}$. Figure 9 shows the correct (repaired) program $\overline{P}^{G}$ that is extracted from the repaired quotient in Figure 8. For N processes, the guard on actions of $\overline{P}_{i}^{G}$ is $\bigwedge _{j \ne i} N_j$.

6.3 No $G$-closed Repairs

Consider the structure in Figure 10 and the formula $f=\textsf {AX} \textsf {AX} \textsf {AX} P$. The structure $\mathcal {M}$ has a single initial state. Let G be the group consisting of the identity and the map swapping S1 and S2. In Figure 10 we see that the quotient structure $\mathcal {M}/(G,\vartheta _{G})$ does not have any nonempty repairs with respect to f. But, $\mathcal {M}$ does contain a substructure $\mathcal {N}$ that satisfies f.

7 Relative Completeness of Group Theoretic Repair

By the Repair Correspondence (Theorem 3), the existence of a repair $\overline{\mathcal {N}}$ of $\overline{\mathcal {M}}$ implies the existence of a repair $\mathcal {N}$ of $\mathcal {M}$. In Example 6.3, we gave an example in which a repair $\mathcal {N}$ of $\mathcal {M}$ exists but no $G$-closed repair does, i.e., $\overline{\mathcal {M}}$ has no repairs. This leads us to ask: is there a fragment of CTL, and/or a class of Kripke structures, for which group theoretic repair is complete? That is, the existence of a repair (substructure $\mathcal {N}$ of $\mathcal {M}$ that satisfies $\varphi$) implies the existence of a $G$-closed repair (substructure $\overline{\mathcal {N}}$ of $\overline{\mathcal {M}}$ that satisfies $\varphi$).

One attempt to answer this question is to examine formulae and structures where substructures are equivalent to the smallest G-closed substructure containing them. Assume there exists $\mathcal {N}\le \mathcal {M}$ such that $\mathcal {N}\,\models \,\varphi$. Write $\mathcal {N}^{G}$ for the smallest $G$-closed structure that contains $\mathcal {N}$. We call $\mathcal {N}^{G}$ the $G$-closure of $\mathcal {N}$ in $\mathcal {M}$. If $\mathcal {N}^{G}$ is bisimilar to $\mathcal {N}$, then $\mathcal {N}^{G}\models \varphi$ and $\overline{\mathcal {N}^G} \models \varphi$ which is a substructure of $\overline{\mathcal {M}}$.

In [14], Emerson et al., give a criteria for a structure $\mathcal {M}$ to be bisimilar to the symmetrized structure $\mathcal {M}^{G}$, their criteria is: for any transition $(s,t) \in \left( \mathcal {M}^{G}\right) _{T}$, there must be a $g \in G$ such that $(s,gt) \in \mathcal {M}_T$. When asking about substructures, it is not clear what criteria on $\mathcal {M}$ is needed to ensure that each substructure $\mathcal {N}$ of $\mathcal {M}$ is bisimilar to $\mathcal {N}^{G}$.

Definition 14

($G$-Repair Complete). Let $\mathcal {M}$ be a Kripke structure with a group of state mappings $G$ and $\varphi$ a $G$-invariant CTL  formula. Let $\mathcal {N}\le \mathcal {M}$ be any repair of $\mathcal {M}$ with respect to $\varphi$, and let s be any state in $\mathcal {N}_{S}$. Then the pair $(\mathcal {M},\varphi )$ is $G$-repair complete if: $\mathcal {N},s \,\models \,\varphi$ implies for all $g\in G$, we have $\mathcal {N}^{G},g(s) \,\models \,\varphi$.

It is clear that propositional formulae are always $G$-repair complete. In addition we note the following:

Theorem 5

If $\varphi$ and $\psi$ are purely propositional formulae then for any Kripke structure $\mathcal {M}$, the pair $(\mathcal {M}, \textsf {A} [\varphi \textsf {\,R\,} \psi ])$ is $G$-repair complete.

There exists structures $\mathcal {M}$ and $\varphi , \psi$ formulae such that $(\mathcal {M},\varphi )$ $G$-repair complete, and $(\mathcal {M}, \psi )$ $G$-repair complete, but $(\mathcal {M}, \varphi \wedge \psi )$ not $G$-repair complete.

Fig. 8.

The Kripke structure defined in Section 6.2. On the left is the repair of $\overline{\mathcal {M}}$ and the lifting of the repair to $\mathcal {M}$ appears on the right.

Fig. 9.

The repaired program $\overline{P}^{G}$ for the program in Section 6.2.

Fig. 10.

The models from Section 6.3 from left to right: the model $\mathcal {M}$, the quotient of $\mathcal {M}$, a repair of $\mathcal {M}$ with respect to $f =\textsf {AX} \textsf {AX} \textsf {AX} P$ that is not G-closed.

Example 4

Let $\mathcal {M}$ be the Kripke structure described by Figure 11. Let $G$ be the group of state mappings generated by swapping s1 and s2. Let $\varphi =\textsf {A} [p\textsf {\,R\,} q]$ and $\psi =\textsf {AF} \ne q$. The structure $\mathcal {M}$ has a nonempty $G$-closed repair for $\varphi$. Similarly there is a single nonempty $G$-closed repair for $\psi$. But $\mathcal {M}$ has no $G$-closed repairs of $\varphi \wedge \psi$.

Fig. 11.

The Kripke Structure from Example 4 (note that $(b,s_0)$ is a transition, while (b, r) is not) (left), $G$-closed repairs of $\mathcal {M}$ with respect to the formulae $\textsf {A} [p\textsf {\,R\,} q]$ (center), and $\textsf {AF} \lnot q$ (right).

8 Conclusions

We present a theory of how group actions could be used to assist in the repair of a Kripke structure.

We presented a theory for the substructures of a given Kripke structure $\mathcal {M}$, their organization into lattices, and how these substructures interact with a group of state-mappings of $\mathcal {M}$. We show a lattice isomorphism between substructure-repairs of $\overline{\mathcal {M}}$ and G-maximal repairs of $\mathcal {M}$ (Theorem 3: Repair Correspondence). This monotone Galois correspondence guarantees that a repair of $\overline{\mathcal {M}}$ lifts to a repair of $\mathcal {M}$: that is to say that model repairs of $\overline{\mathcal {M}}$ with respect to a $G$-invariant CTL  formula $\varphi$ lift to model repairs of $\mathcal {M}$ with respect to $\varphi$. Using this theory we were able to devise a method for repairing concurrent programs which exploits this correspondence, thus avoiding state explosion. We construct the quotient structure $\overline{\mathcal {M}}$ directly from $P$ without the need to construct the structure $\mathcal {M}$. By our correspondence, repairing $\overline{\mathcal {M}}$ will lift to a repair of the structure $\mathcal {M}$, which in turn corresponds to a repair of $P$. We show how to construct a repair of $P$ using the repair of $\overline{\mathcal {M}}$ while circumventing the creation of the larger Kripke structure.

A Kripke structure $\mathcal {M}$ that can be repaired with respect to a formulae $\varphi$ can be repaired via abstraction. However, not every repair of an abstracted structure $\mathcal {N}$ corresponds to a repair of $\mathcal {M}$. In contrast, the structure might not be repairable using the quotient structure, but any repair of the quotient structure will lift to a repair of the original structure.