exploration. Nevertheless, for attributes defined as DL concepts, S. Rudolph
[87] as well as F. Baader and F. Distel [18] proved by different approaches
that the algorithm terminates, if a finite model exists (compare p. 9.2). It
may be given as a transition context.

It could be theoretically interesting to define a category of transition
contexts and to investigate if it is equivalent to a category of Kripke
structures. If the morphisms are chosen accordingly, this should be obvious.
However, there are some technical problems, since within a Kripke structure
the state context is given explicitly, whereas states may occur only in the
first or second component of the transition relation $R$, as indicated in the
proof of the theorem.

In order to show categorial equivalence, it is sufficient to prove that there
is a full, faithful and essentially surjective functor in one direction.
Regarding automata, surely only one or two of these properties are given.
Constructing the respective functors could permit to transfer mathematical
results from one category (or theory) to the other. Yet, for our purposes it
is adequate to state the above structural paralleles.

Figure 5.1: Transitive context of the automaton example 3.1.4 shown in Figure
3.1 (Concept Explorer screenshot).

Finally an example is given how attribute exploration might be used for the
analysis of an automaton. The stem base of the transitive context (Figure 5.1)
according to example 3.1.4 is rather simple:

    1 < 4 > final_in ==> final_out;
    2 < 2 > start_out ==> start_in 1_out;
    3 < 2 > 0_in 1_out ==> final_out;
    4 < 0 > start_in 1_out start_out final_out ==> 0_in 1_in final_in 0_out;
    5 < 0 > 0_in 1_in ==> start_in final_in 0_out 1_out start_out final_out;
    6 < 0 > 0_in start_in ==> 1_in final_in 0_out 1_out start_out final_out;
    7 < 0 > 0_out 1_out ==> 0_in 1_in start_in final_in start_out final_out;
    8 < 0 > start_in final_in final_out ==> 0_in 1_in 0_out 1_out start_out;

Implication 1 signifies that a string is recognised as soon as the first
01-substring is entered, 3 expresses the final condition, 2 that an input 1 is
necessary to remain in a start state. In implications 4-8 all attributes occur
and the support is 0. They express that states must not be start and final at
the same time, 0 and 1 are exclusive, and 0 is not possible in the start
state, but an empty input or 1. These implications could have been entered as
background knowledge, but an attribute exploration helps not to forget one of
the implications, e.g. 6. For this example they are rather obvious for a
human, but in a computer program for automatic reasoning every piece of
information has to be made explicit.

##  Chapter 6 Inference rules for the integration of background knowledge

This chapter presents a method to derive inference rules integrating already
acquired knowledge into the successive exploration of the four formal
contexts. This method uses attribute exploration again on a higher level by
means of a test context defined in Section 6.2.2.

A reasonable order is to first explore a state context $\mathbb{K}_{s}$, then
the related transitive, transition and temporal contexts $\mathbb{K}_{tt}$,
$\mathbb{K}_{t}$ and $\mathbb{K}_{tmp}$ (Section 6.1). We concentrate on
inference rules for implications of $\mathbb{K}_{tt}$, which defines the
semantics of three temporal attributes, or of all in the case of a
deterministic process. Nevertheless, the stem base of $\mathbb{K}_{tmp}$ is
not completely derivable from the stem base of $\mathbb{K}_{tt}$; a subsequent
exploration of $\mathbb{K}_{tmp}$ creates new information (Section 6.2.1).
Inference rules are proven for two important classes of implications:

  * •

Section 6.3: The premises are one or two “homogeneous” attribute sets, e.g.
$X^{in}\wedge\,Y^{out}$ (in $\mathbb{K}_{tt}$) or $\operatorname{ev}{Y}$ (in
$\mathbb{K}_{tmp}$), $X,Y\subseteq M$. Due to computational limits, the test
context had to be constructed with $|M|=3$, but most of the discovered
inference rules are general.

  * •

Section 6.4: The many-valued attributes $e\in E$ take Boolean values $f\in
F=\\{0,1\\}$ (compare Definition 4.2.2). The implications have one homogeneous
attribute set as premise and conclusion, respectively.

###  6.1 A hierarchy of formal contexts

The four defined formal contexts are closely related. $\mathbb{K}_{t}$ is a
subcontext of $\mathbb{K}_{tt}$, since transitions according to the transitive
closure of $R$ are added. Here subcontext means that the attribute set is
equal and the object set is a subset of the object set of the larger context
(of course equality is possible). The same holds for the sets of intents.
$\mathbb{K}_{t}^{in/out}$ and $\mathbb{K}_{tt}^{in/out}$, the input and output
parts of a transition and a transitive context, are equal after object
clarifying and identification of a transition $(s^{in},s^{out})$ with the
state $s^{in}$ and $s^{out}$, respectively. Modified that way and after
identification of an attribute $a^{in}/a^{out}$ with $a$,
$\mathbb{K}_{t}^{in/out}$ and $\mathbb{K}_{tt}^{in/out}$ are subcontexts of
the scale $\mathbb{K}_{s}$.

$\operatorname{Imp}\mathbb{K}$ denotes the set of attribute implications that
hold in a context $\mathbb{K}$. Since implications valid for a formal context
are less restricted by a smaller set of intents, the inverse subset relations
hold for the respective implication sets:

$\operatorname{Imp}\mathbb{K}_{s}\subseteq\operatorname{Imp}\mathbb{K}_{tt}^{in/out}=\operatorname{Imp}\mathbb{K}_{t}^{in/out}$
(6.1)
$\operatorname{Imp}\mathbb{K}_{tt}\subseteq\operatorname{Imp}\mathbb{K}_{t}$
(6.2)

However, implications between sets of input and output attributes of a
transition and a transitive context have different semantics. They relate to
single transitions and sequences of transitions, respectively.

The subset relations can be proven more formally before the background of
model theory.

####  6.1.1 Excursus: Model theory and Galois connections

The two derivation operators ′ of a formal context (Definiton 2.1.1) define
maps $\sigma\colon\mathfrak{P}(G)\rightarrow\mathfrak{P}(M)$ and
$\tau\colon\mathfrak{P}(M)\rightarrow\mathfrak{P}(G)$ between power sets
ordered by set inclusion. They constitute a Galois connection between $G$ and
$M$.

######  Definition 6.1.1.

[56, Definition 3.1.3] A Galois connection between the sets $G$ and $M$ is a
pair of maps

$\sigma\colon\mathfrak{P}(G)\rightarrow\mathfrak{P}(M)\qquad\text{and}\qquad\tau\colon\mathfrak{P}(M)\rightarrow\mathfrak{P}(G),$

so that for all $X,X_{1},X_{2}\subseteq G$ and all $Y,Y_{1},Y_{2}\subseteq M$
the subsequent conditions hold:

  1. 1.

$X_{1}\subseteq X_{2}\Rightarrow\sigma(X_{2})\subseteq\sigma(X_{1})$

  2. 2.

$Y_{1}\subseteq Y_{2}\Rightarrow\tau(Y_{2})\subseteq\tau(Y_{1})$

  3. 3.

$X\subseteq\tau\sigma(X)\text{ and }Y\subseteq\sigma\tau(Y)$.

Now this definition will be applied to the formal context

$(\mathfrak{P}(M),\mathfrak{P}(M)\times\mathfrak{P}(M),\models).$

The attributes in $\mathfrak{P}(M)\times\mathfrak{P}(M)$ are interpreted as
implications $\alpha\colon A\rightarrow B,\>A,B\subseteq M$. The incidence
means that $X\in\mathfrak{P}(M)$ respects the implication $\alpha$, i.e.
$X\models\alpha\Leftrightarrow A\not\subseteq X\text{ or }B\subseteq X$ [38,
p. 110-112]. $X$ is called a model of $\alpha$.

For subsets $\mathcal{F}\subseteq\mathfrak{P}(M)\times\mathfrak{P}(M)$ and
$\mathcal{S}\subseteq\mathfrak{P}(M)$ let

$\operatorname{Mod}\mathcal{F}:=\\{X\subseteq M\mid X\models\alpha\text{ for
all }\alpha\in\mathcal{F}\\}$

be the set of models of $\mathcal{F}$ and

$\operatorname{Imp}\mathcal{S}:=\\{\alpha\in\mathfrak{P}(M)\times\mathfrak{P}(M)\mid
X\models\alpha\text{ for all }X\in\mathcal{S}\\}.$

The operators $\operatorname{Imp}$ and $\operatorname{Mod}$ define a Galois
connection between subsets of $M$ and implications over $M$, i.e. between
$\mathfrak{P}(M)$ and $\mathfrak{P}(M)\times\mathfrak{P}(M)$ (compare [37]).

For every Galois connection the compositions $\tau\sigma$ and $\sigma\tau$
define a closure operator on $G$ and $M$, respectively (p. 2.1.7). Here,
$G:=\mathfrak{P}(M)$, $M:=\mathfrak{P}(M)\times\mathfrak{P}(M)$,
$\sigma:=\operatorname{Imp}$ and $\tau:=\operatorname{Mod}$. The extents and
intents of $(\mathfrak{P}(M),\mathfrak{P}(M)\times\mathfrak{P}(M),\models)$
are Galois closed sets. This closure means that the extents are precisely the
closure systems on $M$ (they are closed under arbitrary intersections), the
intents are the respective implicational theories [38, p. 110]. Thus,
$\operatorname{Mod}\operatorname{Imp}\,\mathcal{S}$ is a closure system on
$M$. It can be represented as the system of intents of a formal context
$\mathbb{K}=(G,M,I)$. Then, $\operatorname{Imp}\mathcal{S}$ is the set of
implications holding in $\mathbb{K}$, or the implicational theory generated by
the stem base of $\mathbb{K}$.

Returning to $\mathbb{K}_{s}$ and $\mathbb{K}_{t}^{in/out}$ identified with a
subcontext of $\mathbb{K}_{s}$, let $\mathcal{S}_{1}$ be the set of object
intents of $\mathbb{K}_{s}$ and $\mathcal{S}_{2}$ the set of object intents of
$\mathbb{K}_{t}^{in/out}$. Then $\operatorname{Imp}\mathcal{S}_{1}$ is the
implicational theory of $\mathbb{K}_{s}$, $\operatorname{Imp}\mathcal{S}_{2}$
that of $\mathbb{K}_{t}^{in/out}$.
$\operatorname{Mod}\operatorname{Imp}\mathcal{S}_{i}$ are the respective
systems of all intents. Since $\mathcal{S}_{2}\subseteq\mathcal{S}_{1}$, we
obtain by virtue of the Galois connection between $\mathfrak{P}(M)$ and
$\mathfrak{P}(M)\times\mathfrak{P}(M)$ (property 1.):

$\operatorname{Imp}\mathbb{K}_{s}=\operatorname{Imp}\mathcal{S}_{1}\subseteq\operatorname{Imp}\mathcal{S}_{2}=\operatorname{Imp}\mathbb{K}_{t}^{in/out}.$

The inclusion $\eqref{eq:impKttKt}$ is proven analogously.

####  6.1.2 Background knowledge for the successive exploration of
$\mathbb{K}_{s},\mathbb{K}_{tt},\mathbb{K}_{t}$ and $\mathbb{K}_{tmp}$

By entering background knowledge (not necessarily implications) prior to an
attribute exploration, the algorithm may be shortened considerably [38]. Thus,
a well structured analysis of a dynamic system should first explore the set of
possible states, then the long-term dynamics expressed by the transitive
context. If a more fine-grained investigation is desired, then also the
transiton context may be explored. Finally, the temporal context should be
computed out of $\mathbb{K}_{t}$, respectively $\mathbb{K}_{tt}$, if the
transitive context is sufficient to determine the semantics of the interesting
attributes (compare Remark 4.5.3). Then the stem base of $\mathbb{K}_{s}$
serves as background knowledge for the exploration of $\mathbb{K}_{tt}$ and
the resulting stem base can be used for the exploration of $\mathbb{K}_{t}$.

Given a state context $\mathbb{K}_{s}$ as scale for a transition as well as a
transitive context (p. 4.3), exploration means determining the attribute logic
with respect to a set of background sequents $\bigwedge A\rightarrow\bigvee
B,\>A,B\subseteq M,$ valid in $\mathbb{K}_{s}$ [38, 104f.]. A formal context
is determined by its stem base up to object reduction and by a set of sequents
up to object clarification. The stem base of $\mathbb{K}_{s}$ excludes only
object intents but does not determine which intents are object intents. It can
be used as background knowledge instead of computing the sequents (possibly
additionally to an already performed attribute exploration), if one is only
interested in the implicational logic of the transition context and does not
need to fix occurring states positively. However, if partially defined states
should be excluded, in general sequents of the structure $\emptyset\multimap
B,B\subseteq M$ are necessary. They can express that for each attribute a
scale value exists, for instance $\top\rightarrow m.0\vee m.1$ for a
dichotomic attribute $m\in M$.

As will be shown in Section 6.2.1, generally the stem base of
$\mathbb{K}_{tt}$ does not determine $\mathbb{K}_{tmp}$ uniquely. However, I
will prove semantic inference rules in order to integrate respective
background knowledge into the exploration of a temporal context. Since
$\mathbb{K}_{tmp}$ extends the attribute set of $\mathbb{K}_{s}$ and restricts
its object set to the set of input states, the implications of
$\mathbb{K}_{s}$ remain valid but are possibly “slightly” too restrictive.
Nevertheless, they can serve as background knowledge for the exploration of
$\mathbb{K}_{tmp}$.

Finally, $\operatorname{Imp}\mathbb{K}_{tt}$ is partly determined by
$\operatorname{Imp}\mathbb{K}_{t}$, e.g.

$A_{in}\rightarrow B_{out},\>B_{in}\rightarrow C_{out}\>(\text{in
}\mathbb{K}_{t})\models A_{in}\rightarrow C_{out}\>(\text{in
}\mathbb{K}_{tt}).$

Hence, it could also make sense to first explore $\mathbb{K}_{t}$ and to
integrate the information into the exploration of $\mathbb{K}_{tt}$ by
inference rules. I will not investigate this rare case further.

###  6.2 Transitive and temporal contexts: A calculus for implications between
temporal atomic propositions

I searched for first order logic background formula in order to use the
results of an attribute exploration of $\mathbb{K}_{tt}$ for the exploration
of $\mathbb{K}_{tmp}$. Then the implications of the latter context are
derivable from this background knowledge and a reduced set of new
implications. The developed method also generates rules between implications
of $\mathbb{K}_{tmp}$ alone. Therefore, during an exploration of
$\mathbb{K}_{tmp}$ implications can be decided automatically based on the stem
base of $\mathbb{K}_{tt}$ and on already accepted implications. The second
type of inferences exploits implications between temporal attributes following
from their definitions, like $\Box Gm\rightarrow\Diamond Fm$.

Prior to searching inference rules systematically by means of a test context,
the subsequent proposition summarises inference rules between implications of
$\mathbb{K}_{tt}$ and $\mathbb{K}_{tmp}$ that follow immediately from the
definition of the temporal attributes by $\mathbb{K}_{tt}$ (Remark 4.5.3):

######  Proposition 6.2.1.

Let $\mathbb{K}_{tmp}=(S^{in},M\cup T,I^{in}\cup I_{T})$ be a temporal
context, $m,m_{1}$ and $m_{2}\in M$ and $B\subseteq M$. Suppose the relation
$t(R)\subseteq S\times S$ is the object set of the related transitive context
$\mathbb{K}_{tt}=(t(R),M\times\\{in,out\\},\nabla)$. Then the following
entailments between implications of both contexts are valid:

$\displaystyle B^{in}\rightarrow m^{out}\>(\text{in }\mathbb{K}_{tt})$
$\displaystyle\equiv B\rightarrow\Box\,Gm\>(\text{in }\mathbb{K}_{tmp})$ (6.3)
$\displaystyle B^{in}\rightarrow m^{out}\>(\text{in }\mathbb{K}_{tt})$
$\displaystyle\models B\rightarrow\Diamond Fm\>(\text{in }\mathbb{K}_{tmp})$
(6.4) $\displaystyle B^{out}\rightarrow m^{out}\>(\text{in }\mathbb{K}_{tt})$
$\displaystyle\models\Box\,GB\rightarrow\Box\,Gm\>(\text{in
}\mathbb{K}_{tmp})$ (6.5) $\displaystyle m_{1}^{out}\rightarrow
m_{2}^{out}\>(\text{in }\mathbb{K}_{tt})$ $\displaystyle\models\Diamond
Fm_{1}\rightarrow\Diamond Fm_{2}\>(\text{in}\>\mathbb{K}_{tmp})$ (6.6)

If there is no transition $(s^{in},s^{out})\in t(R)$ with extents
$(s^{in})^{I}=(s^{out})^{I}=M$, the inference holds:

$B^{in}\cup m^{out}\rightarrow\bot\>(\text{in }\mathbb{K}_{tt})\models
B\rightarrow\Box\,\neg Fm\>(\text{in }\mathbb{K}_{tmp})$ (6.7)

###### Proof.

We remind the reader that for relations $R\subseteq A\times B$ and $a\in A$
the notation $[a]R$ means $[a]R:=\\{b\in B\mid(a,b)\in R\\}$. First we show
item (6.5).

$\displaystyle B^{out}\rightarrow m^{out}\>(\text{in }\mathbb{K}_{tt})$
$\displaystyle\Leftrightarrow$ $\displaystyle\forall\,(s^{in},s^{out})\in
t(R)\colon s^{out}\in B^{I}\Rightarrow s^{out}Im$ $\displaystyle\Rightarrow$
$\displaystyle\forall\,s^{in}\in
S^{in}\colon\text{\large(}\forall\,(s^{in},s^{out})\in t(R)\colon s^{out}\in
B^{I}\text{\large)}\Rightarrow\text{\large(}\forall\,(s^{in},{s^{out}})\in
t(R)\colon s^{out}Im\text{\large)}$ $\displaystyle\Leftrightarrow$
$\displaystyle\Box\,GB\rightarrow\Box\,Gm\>(\text{in }\mathbb{K}_{tmp}).$

Now we show item (6.6).

$\displaystyle m_{1}^{out}\rightarrow m_{2}^{out}\>(\text{in
}\mathbb{K}_{tt})$ $\displaystyle\Leftrightarrow\>$
$\displaystyle\forall\,(s^{in},s^{out})\in t(R)\colon(s^{in},s^{out})\nabla
m_{1}^{out}\Rightarrow(s^{in},s^{out})\nabla m_{2}^{out}$
$\displaystyle\Leftrightarrow\>$ $\displaystyle\forall\,(s^{in},s^{out})\in
t(R)\colon s^{out}Im_{1}\Rightarrow s^{out}Im_{2}\>(\text{in
$\mathbb{K}_{s}$})$ $\displaystyle\Leftrightarrow\>$
$\displaystyle\forall\,s^{in}\in
S^{in},\>\forall\,s^{out}\in[s^{in}]t(R)\colon s^{out}\in m_{1}^{I}\Rightarrow
s^{out}Im_{2}$
$\displaystyle\overset{{s^{out}}^{\prime}:=s^{out}}{\Rightarrow}\>$
$\displaystyle\forall\,s^{in}\in
S^{in}\colon\text{\large(}\exists\,s^{out}\in[s^{in}]t(R)\colon s^{out}\in
m_{1}^{I}\text{\large)}\Rightarrow\text{\large(}\exists\,{s^{out}}^{\prime}\in[s^{in}]t(R)\colon{s^{out}}^{\prime}Im_{2}\text{\large)}$
$\displaystyle\Leftrightarrow\>$ $\displaystyle\Diamond
Fm_{1}\rightarrow\Diamond Fm_{2}\>(\text{in }\mathbb{K}_{tmp}).$

The remaining equivalences are proven analogously. The supplementary condition
for $\eqref{prop:5}$ ensures that $\bot^{I}=M^{I}=\emptyset$. Hence, the
presupposed implication signifies exclusion of $B^{in}$ and $m^{out}$, or
$B^{I}=\emptyset$. In the latter case the inferred conclusion is trivially
valid. ∎

The restriction of $\mathbb{K}_{tmp}$ to an object set $S^{in}$ (Definition
4.5.2) is necessary for the proofs. Regarding (6.4), consider e.g.
$S=\\{0,1\\}$, $s=0$, $R=\\{(1,1)\\}$ and $M=\\{m,n\\}$, $B=\\{n\\}$ and
$I=\\{(0,n),(1,m)\\}$. Then $B^{in}=\\{n^{in}\\}\not\subseteq(1,1)^{\nabla}$,
so the left-hand side of the entailment is trivially true. However,
$B\subseteq 0^{I}$ but $(0,\Diamond Fm)\notin I_{T}$, since
$Seq^{s}_{R}=\emptyset$ for $s=0$.

####  6.2.1 Incomplete determination of $\mathbb{K}_{tmp}$ by the stem base of
$\mathbb{K}_{tt}$

For $\Diamond F$, $\Box\,G$ and $\Box\,\neg F$, the complete dynamics of the
investigated system, thus $\mathbb{K}_{tmp}$, is determined by the respective
transitive (or transition) context, but there is no one-to-one correspondence
between the stem bases of $\mathbb{K}_{tmp}$ and $\mathbb{K}_{tt}$. Reducible
transitions may exist that prevent a temporal implication, for
nondeterministic processes or a data set consisting of different deterministic
time series. Omitting them does not change the stem base of $\mathbb{K}_{tt}$.
For an example, see Table 6.1.

Transition | $a^{in}$ | $b^{in}$ | $c^{in}$ | $a^{out}$ | $b^{out}$ | $c^{out}$
---|---|---|---|---|---|---
$(s_{0}^{in},s_{1}^{out})$ | $\times$ | $\times$ |  |  | $\times$ | $\times$
$(s_{0}^{in},s_{2}^{out})$ | $\times$ | $\times$ |  | $\times$ |  | $\times$
$(s_{1}^{in},s_{2}^{out})$ |  | $\times$ | $\times$ | $\times$ |  | $\times$
$(s_{3}^{in},s_{4}^{out})$ |  | $\times$ |  |  |  | $\times$
Table 6.1: The transitive context $\mathbb{K}_{tt}$ for two deterministic time
series $s_{0}-s_{1}-s_{2}$ and $s_{3}-s_{4}$.

The stem base of this transitive context is:

  1. 1.

$\top\rightarrow b^{in},c^{out}$

  2. 2.

$b^{in},c^{in},c^{out}\rightarrow a^{out}$

  3. 3.

$b^{in},b^{out},c^{out}\rightarrow a^{in}$

  1. 4.

$a^{in},b^{in},c^{in},a^{out},c^{out}\rightarrow b^{out}$

  2. 5.

$a^{in},b^{in},a^{out},b^{out},c^{out}\rightarrow c^{in}$

$(s_{3}^{in},s_{4}^{out})$ is a reducible object, because for example:

$\displaystyle(s_{3}^{in},s_{4}^{out})^{\prime}$
$\displaystyle=\\{b^{in},c^{out}\\}=\\{a^{in},b^{in},b^{out},c^{out}\\}\cap\\{b^{in},c^{in},a^{out},c^{out}\\}$
$\displaystyle=(s_{0}^{in},s_{1}^{out})^{\prime}\cap(s_{1}^{in},s_{2}^{out})^{\prime}$

Therefore, the context without this transition has the same stem base.
However, only without this observation $\top\rightarrow\Diamond Fa$ holds in
$\mathbb{K}_{tmp}$.

The following proposition concerns a linear order $R$ and specifies a special
case where the temporal context is determined by the stem base of the
transitive context: If it is known that only transitions with the first (or
only with the last) transition are reducible, not all of them can be reduced
and the order relation can be reconstructed.

######  Proposition 6.2.2.

Let $\mathbb{K}_{tt}=(t(R),M\times\\{in,out\\},\nabla)$ be a transitive
context with a linear order $R\subseteq S\times S$, $R\neq\emptyset$. Then the
removal from $R$ of all transitions with the first (last) state changes the
stem base of $\mathbb{K}_{tt}$. In general however, the following changes
might not affect the stem base of $\mathbb{K}_{tt}$, but result in a different
stem base of the temporal context $\mathbb{K}_{tmp}$ defined by
$\mathbb{K}_{tt}$:

  1. 1.

The removal of a state and all related transitions that is not the first or
last state.

  2. 2.

A switch of the order relation of two states.

###### Proof.

The implication logic determines $\mathbb{K}_{tt}$ up to object reduction. If
$\mathbb{K}_{tt}$ consists of a single transition, it is reducible only if
$(s_{0}^{in},s_{1}^{out})=(M\times\\{in,out\\})^{\prime}=\emptyset^{\prime}$.
But since the resulting concept lattice is isomorphic to the one element
lattice,
$\mathfrak{B}(\emptyset,\emptyset,\emptyset)\cong\mathfrak{B}((s_{0}^{in},s_{1}^{out}),\emptyset,\emptyset)$,
this case could be considered as attribute reduction and therefore excluded
(attribute reduction results in a different stem base).

A state $s_{k}$ can be removed from the linear order, if all transitions
$(s_{i},s_{k})$ and $(s_{k},s_{j})$ are reducible. Then all $s_{i}$ have to be
intersections of input, all $s_{j}$ intersections of output state intents,
which cannot be generelly excluded.

However, if $k=0$, only the output parts of the respective transitions are
available for intersection. With the order relation of intersection, these
intents build a lattice, and each nonempty lattice has $\bigvee$-irreducible
elements. Hence, a corresponding transition $(s_{0},s_{j})$ is irreducible,
and the linear order may be reconstructed. The same argument holds for a final
output state $s_{k}$: There exist irreducible $(s_{i},s_{k})$.

Changing the order of two states may result in the same stem base of
$\mathbb{K}_{tt}$, but generate a temporal context with different
implicational logic: In the transitive context derivable from the transition
context of Table 6.2, the transition $(s_{5},s_{6})$ is reducible. Changing
only the order of $s_{5}$ and $s_{6}$ results in the same transitive context,
with the exception of transition $(s_{6},s_{5})$. It is also reducible to the
same context. However, the corresponding temporal contexts are different. The
implication $\Diamond Fa\rightarrow\Diamond Fb$ only holds in the original,
$\Diamond Fb\rightarrow\Diamond Fa$ only in the modified temporal context. ∎

Transition | $a^{in}$ | $b^{in}$ | $c^{in}$ | $d^{in}$ | $a^{out}$ | $b^{out}$ | $c^{out}$ | $d^{out}$
---|---|---|---|---|---|---|---|---
$(s_{0}^{in},s_{1}^{out})$ | $\times$ |  |  | $\times$ |  | $\times$ |  | $\times$
$(s_{1}^{in},s_{2}^{out})$ |  | $\times$ |  | $\times$ | $\times$ |  | $\times$ |
$(s_{2}^{in},s_{3}^{out})$ | $\times$ |  | $\times$ |  |  | $\times$ | $\times$ |
$(s_{3}^{in},s_{4}^{out})$ |  | $\times$ | $\times$ |  | $\times$ | $\times$ |  | $\times$
$(s_{4}^{in},s_{5}^{out})$ | $\times$ | $\times$ |  | $\times$ | $\times$ |  |  |
$(s_{5}^{in},s_{6}^{out})$ | $\times$ |  |  |  |  | $\times$ |  |
$(s_{6}^{in},s_{7}^{out})$ |  | $\times$ |  |  |  |  |  |
Table 6.2: Transition context for a linearly ordered state set. If the order
of $s_{5}$ and $s_{6}$ is exchanged, the stem base of the respective reduced
$\mathbb{K}_{tt}$ remains the same, but a different $\mathbb{K}_{tmp}$ is
generated.

Nevertheless, note that there exist cases 1. and 2. where $\mathbb{K}_{tmp}$
is reconstructable from the stem base of $\mathbb{K}_{tt}$. For instance, if
the order is changed at an early point, this may result in the same temporal
context. In Table 6.3, the object $(s_{0},s_{1})$ is reducible. Thus,
supposing a linear order the relation of $s_{0}$ and $s_{1}$ is not reflected
by the stem base. In general, the inverse relation may induce different
temporal attributes. In this example, however, the context with
$(s_{1},s_{0})$ as first transition has the same stem base, but also the same
temporal context $\mathbb{K}_{tmp}$ (only the attributes $b^{in}$ and
$b^{out}$ are changed in the first row).

Transition | $a^{in}$ | $b^{in}$ | $c^{in}$ | $a^{out}$ | $b^{out}$ | $c^{out}$
---|---|---|---|---|---|---
$(s_{0}^{in},s_{1}^{out})$ |  | $\times$ |  |  |  |
$(s_{0}^{in},s_{2}^{out})$ |  | $\times$ |  | $\times$ | $\times$ |
$(s_{0}^{in},s_{3}^{out})$ |  | $\times$ |  |  | $\times$ | $\times$
$(s_{0}^{in},s_{4}^{out})$ |  | $\times$ |  |  |  | $\times$
$(s_{1}^{in},s_{2}^{out})$ |  |  |  | $\times$ | $\times$ |
$(s_{1}^{in},s_{3}^{out})$ |  |  |  |  | $\times$ | $\times$
$(s_{1}^{in},s_{4}^{out})$ |  |  |  |  |  | $\times$
$(s_{2}^{in},s_{3}^{out})$ | $\times$ | $\times$ |  |  | $\times$ | $\times$
$(s_{2}^{in},s_{4}^{out})$ | $\times$ | $\times$ |  |  |  | $\times$
$(s_{3}^{in},s_{4}^{out})$ |  | $\times$ | $\times$ |  |  | $\times$
Table 6.3: The transitive context for a linear order $s_{0}\leq s_{1}\leq
s_{2}\leq s_{3}\leq s_{4}$. $(s_{0},s_{1})$ is reducible, as well as
$(s_{1},s_{0})$ in a context with this transition instead, but both formal
contexts generate the same temporal context.

######  Remark 6.2.3.

Implications of the form $B\rightarrow\Box\neg Fm\text{ in }\mathbb{K}_{tmp}$
may be derived from implications $B^{in}\cup m^{out}\rightarrow\bot\text{ in
}\mathbb{K}_{tt}$ (compare Proposition 6.2.1). However, implications with
negated attributes in the premise can only be decided using the stem base of
$\mathbb{K}_{tt}$ in the case of dichotomic scaling. Else, there is no
explicit information regarding the non-occurrence of an attribute. In the
example of Table 6.2, the only implication in the stem base of
$\mathbb{K}_{tt}$ with $a^{out},b^{out}$ in the premise is
$a^{out},b^{out}\rightarrow d^{out}$. With
$b^{out},c^{out},d^{out}\rightarrow\bot$,
$\Box\,Ga,\Box\,Gb\rightarrow\Box\,\neg Fc$ is derivable, but there is no
inference for deriving from $\mathbb{K}_{tt}$ the valid implication
$\Box\,Fa,\Box\,Fb,\Box\,\neg Fc\rightarrow b$, which is supported by
$\\{s_{3}\\}$ in $\mathbb{K}_{tmp}$. This can be easily seen, since there is
no $\mathbb{K}_{tt}$ implication with $b^{in}$ in the conclusion. The same
holds for the possibility operator $\Diamond$, since it is equivalent to the
necessity operator in the case of deterministic time series.

####  6.2.2 The test context

In order to get a complete overview on valid “pure” or “mixed” entailments
between implications of $\mathbb{K}_{tt}$ and $\mathbb{K}_{tmp}$, we performed
attribute exploration of the following test context: Given fixed sets $S$ and
$M$, the attributes are implication forms $IF$ in variables $V:=\\{X,Y,Z\\}$,
the objects are all possible $\mathbb{K}_{tt}$ respectively the corresponding
$\mathbb{K}_{tmp}$ (Table 6.4) together with a variable assignment, and the
incidence relation means: “With the respective values of the set variables,
the implication holds in the context.” More precisely, the objects are
appositions ($\mathbb{K}_{tt}|\mathbb{K}^{\prime}_{tmp})$, where
$\mathbb{K}^{\prime}_{tmp}$ proceeds from $\mathbb{K}_{tmp}$ by replacing an
object $s^{in}$ of the latter by all transitions $(s^{in},s^{out})\in t(R)$.
This state context $\mathbb{K}_{tmp}^{\prime}$ is not object clarified, i.e.
redundant. The attributes are given by $(s^{in},s^{out})^{\prime}=s^{in}$′.
According to Definition 4.5.2 of a temporal context, the last state of a
finite path is omitted.

The investigated temporal operators are restricted to
$\operatorname{ev}:=\Diamond F$, $\operatorname{alw}:=\Box G$ and
$\operatorname{nev}:=\Box\neg F$ decidable by $\mathbb{K}_{tt}$, where the
same quantifier $\exists$ or $\forall$ applies to paths and transitions
(Definition 4.5.2).

Thus, we performed attribute exploration of the following test context:

$\mathbb{K}_{test}=(\\{\alpha:\\{X,Y,Z\\}\rightarrow\mathfrak{P}(M)\setminus\emptyset\\}/S_{M}\times\\{\mathbb{K}_{tt}|\mathbb{K}_{tmp}^{\prime}\\},IF,\models)$

Variable assignments $\operatorname{mod}S_{M}$ (the symmetric group on $M$)
are sufficient, because also $\\{\mathbb{K}_{tt}|\mathbb{K}_{tmp}^{\prime}\\}$
is symmetric in the attributes $M$.

|  $a^{in}$ |  $b^{in}$ |  $c^{in}$ |  $a^{out}$ |  $b^{out}$ |  $c^{out}$ |  $\operatorname{ev}a$ |  $\operatorname{ev}b$ |  $\operatorname{ev}c$ |  $\operatorname{alw}a\>$ |  $\operatorname{alw}b$ |  $\operatorname{alw}c$ |  $\operatorname{nev}a$ |  $\operatorname{nev}b$ |  $\operatorname{nev}c$
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---
$(s_{0}^{in},s_{1}^{out})$ | $\times$ |  |  | $\times$ | $\times$ |  | $\times$ | $\times$ | $\times$ |  |  |  |  |  |
$(s_{0}^{in},s_{2}^{out})$ | $\times$ |  |  | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ |  |  |  |  |  |
$(s_{0}^{in},s_{3}^{out})$ | $\times$ |  |  |  |  | $\times$ | $\times$ | $\times$ | $\times$ |  |  |  |  |  |
$(s_{1}^{in},s_{2}^{out})$ | $\times$ | $\times$ |  | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ | $\times$ |  |  | $\times$ |  |  |
$(s_{1}^{in},s_{3}^{out})$ | $\times$ | $\times$ |  |  |  | $\times$ | $\times$ | $\times$ | $\times$ |  |  | $\times$ |  |  |
$(s_{2}^{in},s_{3}^{out})$ | $\times$ | $\times$ | $\times$ |  |  | $\times$ |  |  | $\times$ |  |  | $\times$ | $\times$ | $\times$ |
Table 6.4: A single object of the test context: the apposition of the
transitive and temporal contexts corresponding to the time series $a-ab-
abc-c.$

Since it was not feasible to investigate all possible implications, we chose
the following classes with at most two premises (with different variables $X$,
$Y$ or the constant $\top$) and a single conclusion. Many implications with
more than two different attribute sets in the premise can be derived by the
second and third Armstrong rule.

| $\mathbb{K}_{tt}$ | $\mathbb{K}_{tmp}$
---|---|---
1 or 2 premises | $X^{in},Y^{out},\top$ | $X,\,\Diamond FY,\,\Box GY,\,\Box\neg FY,\top$
1 conclusion | $Z^{in},Z^{out},\bot$ | $Z,\,\Diamond FZ,\,\Box\,GZ,\,\Box\neg FZ,\bot$

The sets were supposed to be nonempty. Thus, $\top:=\emptyset$ was considered
explicitly, in order to avoid redundancies like $\Diamond F\emptyset=\Box
G\emptyset$. Tautologic or unsatisfiable implication forms were not
considered, like $\Box GY\rightarrow\Diamond FY$ or $\Diamond FY,\>\Box\neg
FY\rightarrow\bot$.

###  6.3 Inference rules for a three element attribute set $M$

Even with computational optimisation, it took 10 days, partly on two desktop
computers, to generate the test context with $|M|=3$. Since computation time
is exponential in $|M|$, it is not feasible to compute the test context for
larger attribute sets. For $M=\\{a,b,c\\}$, we generated all deterministic
time series (linear orders) including cycles.

If the 81 inference rules of the stem base are proven, the hypothesis is
confirmed that this attribute set is general enough. However, this was only
possible for rules 1 to 56. For rule 57, 59 and 65, a supplementary condition
is necessary restricting the allowed transitions (Propositions 6.3.6 and
6.3.7). Since during the computation of a stem base the generated rules depend
on the previous, I proved only several further rules resulting in a large, but
not complete set of inference rules for transitive and temporal context.
Further research is needed: Expert centered attribute exploration should be
performed by introducing counterexamples to rules that are not generalisable
and by proving the remaining or new implications. Then the Theorem of
Duquenne-Guigues 2.2.2 ensures the completeness of the stem base rules for
drawing all rule-like conclusions between the implications investigated as
attributes of the test context.

A further purpose of the following proofs is to determine presuppostions as
generally as possible. It turned out that most rules are also valid for
nondeterminstic processes.

As indicated by the used sofware ConImp [26], we have to prove only the parts
of the premise and conclusion not following from previous implications.
Several implications follow trivially, since $\bot$ means “every attribute
occurs”, for instance
$\operatorname{alw}Y\rightarrow\bot\>\models\operatorname{alw}Y\rightarrow
Z^{in}$.

In a first step, general propositions are proven for example inferences. The
attached file testCxt.pro – the output of the test context exploration –
contains all 81 inference rules. Their indices are listed in Table 6.5
together with the propositions necessary for the proofs (sometimes easy
consequences are needed, or analogous applications of the proofs).

For the subsequent propositions, the following presuppositions are made:
$\mathbb{K}_{tt}=(t(R),M\times\\{in,out\\},\nabla)$ with $R\subseteq S\times
S$ and $\mathbb{K}_{tmp}=(S^{in},M\cup T,I^{in}\cup I_{T})$ are formal
contexts generated by the same process. $B$, $X$, $Y$ and $Z\subseteq M$ are
their basic attribute sets. If the process is not qualified, it may be
deterministic or nondeterministic. $i,j,k\in\mathbb{N}_{0}$ are indices from
sets according to the number of transitions of a path. Implications with
attribute sets indexed by $.^{in}$ or $.^{out}$ refer to a transitive context
and the left part of the apposition
$\mathbb{K}_{tt}\mid\mathbb{K}_{tmp}^{\prime}$, the remaining attributes to
$\mathbb{K}_{tmp}^{\prime}$ and therefore to the temporal context
$\mathbb{K}_{tmp}$ generated by $\mathbb{K}_{tt}$.

######  Proposition 6.3.1.

For all $\mathbb{K}_{tt}$ and $\mathbb{K}_{tmp}$ generated by the same
process, the following inference rules hold by the second Armstrong rule.

$\displaystyle 11:\>$ $\displaystyle\operatorname{alw}Y\rightarrow\bot$
$\displaystyle\models\>$ $\displaystyle
X\wedge\operatorname{alw}Y\rightarrow\bot,\>\operatorname{ev}Y\wedge\operatorname{alw}Y\rightarrow\bot,$
$\displaystyle X\wedge\operatorname{nev}Y\rightarrow\operatorname{nev}Z$
$\displaystyle 5:\>$ $\displaystyle\top\rightarrow Z^{in}$
$\displaystyle\models\>$ $\displaystyle X^{in}\rightarrow
Z^{in},\>Y^{out}\rightarrow Z^{in},\>\operatorname{ev}Y\rightarrow
Z,\>X^{in}\wedge Y^{out}\rightarrow Z^{in},...$

###### Proof.

Rule 11 follows by the second Armstrong rule, i.e. an expansion of the premise
$P$, with attributes $A_{i}\subseteq M\cup(M\times\\{in,out\\})\cup T$ (where
attributes of $\mathbb{K}_{tmp}$ are in $M$ or $T$):

$\displaystyle P:\underline{\qquad A_{2}\>}$
$\displaystyle\underline{\>\rightarrow A_{3}}$ (6.8) $\displaystyle
C:A_{1}\wedge A_{2}$ $\displaystyle\rightarrow A_{3}$

In rule 5, $A_{2}=\emptyset$. With the presupposed implication of
$\mathbb{K}_{tt}$, all implications of $\mathbb{K}_{tt}$ with the conclusion
$Z^{in}$ and all implications of $\mathbb{K}_{tmp}$ with the conclusion $Z$
can be inferred, since the extents are equal: $Z^{in}=Z\subseteq
M\Rightarrow(Z^{in})^{I^{in}}=Z^{I^{in}}$ (remember that in $\mathbb{K}_{tmp}$
the object set is restricted to the set of input states $S^{in}$, consequently
the relation $I$). By further applications of the second Armstrong rule,
implications with arbitrarily enlarged premises are shown to be valid. ∎

######  Proposition 6.3.2.

For all $\mathbb{K}_{tt}$ and $\mathbb{K}_{tmp}$ generated by the same
process, the following inference rules hold by definition of the temporal
operators $\operatorname{ev},\>\operatorname{alw}$ and $\operatorname{nev}$:

$\displaystyle 1.\>$ $\displaystyle 26\colon\>$
$\displaystyle\operatorname{ev}Y\wedge\operatorname{alw}Y\rightarrow\bot\qquad$
$\displaystyle\models$ $\displaystyle\operatorname{alw}Y\rightarrow\bot$
$\displaystyle 27\colon\>$
$\displaystyle\operatorname{ev}Y\wedge\operatorname{alw}Y\rightarrow\operatorname{nev}Z\qquad$
$\displaystyle\models$
$\displaystyle\operatorname{alw}Y\rightarrow\operatorname{nev}Z$
$\displaystyle 2.\>$ $\displaystyle 41:\>$ $\displaystyle
X\wedge\operatorname{ev}Y\rightarrow\bot\qquad$ $\displaystyle\models$
$\displaystyle X^{in}\wedge Y^{out}\rightarrow\bot$ $\displaystyle 44:\>$
$\displaystyle X\wedge\operatorname{ev}Y\rightarrow\operatorname{ev}Z\qquad$
$\displaystyle\models$ $\displaystyle
X\wedge\operatorname{alw}Y\rightarrow\operatorname{ev}Z$ $\displaystyle 46:\>$
$\displaystyle X\wedge\operatorname{ev}Y\rightarrow Z^{in}\qquad$
$\displaystyle\models$ $\displaystyle X^{in}\wedge Y^{out}\rightarrow
Z^{in},\>X\wedge\operatorname{alw}Y\rightarrow Z$ $\displaystyle 3.\>$
$\displaystyle 32:\>$ $\displaystyle
X\wedge\operatorname{nev}Y\rightarrow\operatorname{alw}Z\qquad$
$\displaystyle\models$ $\displaystyle
X\wedge\operatorname{nev}Y\rightarrow\operatorname{ev}Z$ $\displaystyle 37:\>$
$\displaystyle X\wedge\operatorname{alw}Y\rightarrow\operatorname{alw}Z\qquad$
$\displaystyle\models$ $\displaystyle
X\wedge\operatorname{alw}Y\rightarrow\operatorname{ev}Z$ $\displaystyle 43:\>$
$\displaystyle X\wedge\operatorname{ev}Y\rightarrow\operatorname{alw}Z\qquad$
$\displaystyle\models$ $\displaystyle X^{in}\wedge Y^{out}\rightarrow
Z^{out},\>X\wedge\operatorname{alw}Y\rightarrow\operatorname{alw}Z.$

###### Proof.

Let $D$ be an implication valid in the test context that follows immediately
from the definitions. Examples are the subsequent implications of
$\mathbb{K}_{tmp}$ (6.9) or with attributes of $\mathbb{K}_{tmp}$ and
$\mathbb{K}_{tt}$:

$\displaystyle\operatorname{alw}B$
$\displaystyle\rightarrow\operatorname{ev}B$ (6.9)
$\displaystyle\operatorname{alw}B$ $\displaystyle\rightarrow B^{out}$ (6.10)
$\displaystyle B^{out}$ $\displaystyle\rightarrow\operatorname{ev}B.$ (6.11)

We distinguish the following inference modi, with attribute sets
$A_{i}\subseteq M\cup(M\times\\{in,out\\})\cup T$. They are special cases of
the third Armstrong rule that expresses generalised transitivity.

  1. 1.

$\displaystyle P:A_{1}\wedge A_{2}$ $\displaystyle\rightarrow A_{3}$ (6.12)
$\displaystyle D:\underline{\qquad\>\,A_{2}}$
$\displaystyle\underline{\>\rightarrow A_{1}}$ $\displaystyle
C:\qquad\>\,A_{2}$ $\displaystyle\rightarrow A_{3}$

With $A_{1}:=\operatorname{ev}Y,\>A_{2}:=\operatorname{alw}Y$ and
$A_{3}:=\bot$, $P\models C$ is inference rule 26. Rule 27 and others follow
with different attribute sets $A_{3}$ (see Table 6.5, where also the used
implications $D$ are indicated in the column “Definition”).

  2. 2.

In 41, 44 and 46, a part of the premise is replaced by a stronger assumption.
Here D is either $\operatorname{alw}Y\rightarrow\operatorname{ev}Y$ or
$Y^{out}\rightarrow\operatorname{ev}Y$:

$\displaystyle P:A_{1}\wedge A_{2}$ $\displaystyle\rightarrow A_{3}$ (6.13)
$\displaystyle D:\underline{\qquad\;A_{4}}$
$\displaystyle\underline{\>\rightarrow A_{2}}$ $\displaystyle C:A_{1}\wedge
A_{4}$ $\displaystyle\rightarrow A_{3}$

  3. 3.

In 32 and 37, $D\colon\operatorname{alw}Y\rightarrow\operatorname{ev}Y$ is
applied to the conclusion of the presupposed rule (ordinary transitive
inference):

$\displaystyle P:A_{1}\wedge A_{2}$ $\displaystyle\rightarrow A_{3}$ (6.14)
$\displaystyle D:\underline{\qquad\;A_{3}}$
$\displaystyle\underline{\>\rightarrow A_{4}}$ $\displaystyle C:A_{1}\wedge
A_{2}$ $\displaystyle\rightarrow A_{4}$

In 43, $D\colon\operatorname{alw}Z\rightarrow Z^{out}$ is used, additionally
$\operatorname{alw}Y\rightarrow\operatorname{ev}Y$ and
$Y^{out}\rightarrow\operatorname{ev}Y$ according to inference pattern (6.13).

∎

If the inference rules are implemented as an extension of an attribute
exploration software, it has to be decided if the rules according to this
proposition are an immediate input to a reasoner. Alternatively, implications
as (6.9), (6.10) and (6.11) could be assembled, together with an
implementation of the Armstrong rules for attribute exploration itself.
Proposition 6.3.1 may have little practical relevance: If an implication
$A_{2}\rightarrow A_{3}$ is accepted, $A_{1}\cup A_{2}$ does not contain the
closure $A_{3}$ of the pseudo-intent $A_{2}$. Therefore, it is no pseudo-
intent and cannot be proposed as implication of the stem base. At least the
proposition could be useful for “mixed” implications: rule 5 translates the
implication $\top\rightarrow Z^{in}$ of $\mathbb{K}_{tt}$ into implications of
$\mathbb{K}_{tmp}$. However, I will not discuss such issues of practical
applicability further.

######  Proposition 6.3.3.

Let $\mathbb{K}_{tmp}$ be a temporal context and $\mathbb{K}_{tt}$ the related
transitive context. Then the entailment between implications of
$\mathbb{K}_{tmp}$ and $\mathbb{K}_{tt}$ is valid:

$53\colon X^{in}\rightarrow Z^{out}\models X\rightarrow\operatorname{alw}Z.$

###### Proof.

The rule follows from Proposition 6.2.1 (6.3) applied to every $z\in Z$. ∎

If the inferences of Proposition 6.2.1 are entered as background knowledge for
the exploration of the test context (with variants for the set variables $X,Y$
and $Z$), rule 53 and a few others can be decided automatically.

######  Proposition 6.3.4.

For all $\mathbb{K}_{tt}$ and $\mathbb{K}_{tmp}$ generated by the same
process, the following inference rules hold by exclusion of
$\operatorname{ev}/\operatorname{alw}$ and $\operatorname{nev}$:

$\displaystyle\;1:\>\
\top\models\>\operatorname{ev}Y\wedge\operatorname{nev}Y\rightarrow\bot,\>\operatorname{alw}Y\wedge\operatorname{nev}Y\rightarrow\bot$
(6.15) $\displaystyle
38:\>X\wedge\operatorname{alw}Y\rightarrow\operatorname{ev}Z,\>X\wedge\operatorname{alw}Y\rightarrow\operatorname{nev}Z\models\>X\wedge\operatorname{alw}Y\rightarrow\bot$
(6.16)

###### Proof.

By definition, $\operatorname{ev}y$ and $\operatorname{nev}y$ cannot be both
attributes of a state $s\in S^{in}$, for all $y\in Y$. By pairwise exclusion,
the extent $(\operatorname{ev}Y\cup\,\operatorname{nev}Y)^{I_{T}}$ is empty;
this means $\operatorname{ev}Y\wedge\,\operatorname{nev}Y\rightarrow\bot$. The
second implication of rule 1 follows with $\eqref{eq:alwEv}$ and the third
Armstrong rule (6.13). 38 is inferred by $\eqref{eq:conPremise}$ with the
attribute set $A_{3}=\operatorname{ev}Z\,\cup\,\operatorname{nev}Z$. ∎

A surprising rule expressing more complex temporal relationships is the
following.

######  Proposition 6.3.5.

Let $\mathbb{K}_{tmp}$ be a temporal context of a deterministic process, i.e.
$\forall s\in S^{in}\colon|[s]R|:=|\\{s^{out}\in S\mid\exists(s,s^{out})\in
R\\}|=1$. Then the subsequent entailments between implications of
$\mathbb{K}_{tmp}$ are valid:

$\displaystyle 39\colon\operatorname{alw}Y\rightarrow
Z,\>\operatorname{alw}Y\rightarrow\operatorname{ev}Z$
$\displaystyle\models\operatorname{alw}Y\rightarrow\operatorname{alw}Z$
$\displaystyle 34\colon\operatorname{nev}Y\rightarrow
Z,\>\operatorname{nev}Y\rightarrow\operatorname{ev}Z$
$\displaystyle\models\operatorname{nev}Y\rightarrow\operatorname{alw}Z.$

###### Proof.

We consider an arbitrary transitive context
$\mathbb{K}_{tt}=(t(R),M\times\\{in,out\\},\nabla)$ generating
$\mathbb{K}_{tmp}$ and differentiate between two cases for a state
$s_{0}^{in}\in S^{in}$:

  1. 1.

$\operatorname{alw}Y\nsubseteq(s_{0}^{in})^{I_{T}}$.
$\Rightarrow$ The implications and the entailment trivially hold.

  2. 2.

$\operatorname{alw}Y\subseteq(s_{0}^{in})^{I_{T}}$. Then
$\operatorname{alw}Y$ $\rightarrow
Z,\>\operatorname{alw}Y\rightarrow\operatorname{ev}Z$ is supported by
$s_{0}^{in}$. $\Leftrightarrow$ $\forall\,(s_{0}^{in},s^{out})\in
t(R),\>\forall\,y\in Y\colon(s^{out},y)\in I\qquad\qquad(*)$ $\wedge$ $\forall
z\in Z\colon(s_{0}^{in},z)\in I$ $\wedge$ $\forall z\in
Z\>\exists\,(s_{0}^{in},s^{out})\in t(R)\colon(s^{out},z)\in I$. $\Rightarrow$
$\forall\,(s_{0}^{in},s^{out})\in
t(R)\colon\operatorname{alw}Y\subseteq(s_{0}^{out})^{I_{T}}$, if
$s^{out}\in\mathbb{K}_{tmp}$, i.e.
$\exists\,s^{out^{\prime}}\colon(s^{out},s^{out^{\prime}})\in t(R)$.
$\Rightarrow$ $\forall\,(s_{0}^{in},s^{out})\in t(R),\>\forall z\in
Z\colon(s^{out},z)\in I$: If $s^{out}$ is a final state, $(s^{out},z)\in I$
follows with $\operatorname{alw}Y\rightarrow\operatorname{ev}Z$ for an
immediately antecedent state and a deterministic process. $\Leftrightarrow$
$\operatorname{alw}Y\rightarrow\operatorname{alw}Z$ holds for $s_{0}^{in}$.

Like $\operatorname{alw}$, $\operatorname{nev}$ applies to every state
subsequent to $s_{0}^{in}$, if defined and
$\operatorname{nev}Y\subseteq(s_{0}^{in})^{I_{T}}$. Therefore, the entailment
for $\operatorname{nev}Y$ is proven in the same way with $(s^{out},y)\notin I$
in statement $(*)$. ∎

Rule | Inference modus | Definition
---|---|---
1. | Proposition 6.3.4, (6.13) | (6.9)
2. | (6.8) |
3. | (6.14), (6.8) | (6.9), (6.10), (6.11)
4. | (6.8) |
5. | (6.8) |
6. | trivial, (6.8) |
7. | (6.8) |
8. | (6.14), (6.8) | (6.9)
9. | (6.8) |
10. | (6.8) |
11. | trivial, (6.8) |
12. | (6.8) |
13. | (6.14), (6.8) | (6.9)
14. | (6.8) |
15. | (6.8) |
16. | trivial, (6.8) |
17. | (6.13), (6.8) | (6.9)
18. | (6.13), (6.14), (6.8) | (6.9), (6.10), (6.11)
19. | (6.13), (6.8) | (6.9)
20. | (6.13), (6.8) | (6.9), (6.11)
21. | trivial, (6.8) |
22. | (6.8) |
23. | (6.14), (6.8) | (6.9), (6.10)
24. | (6.8) |
25. | (6.8) |
26. | (6.12) | (6.9)
27. | (6.12) | (6.9)
28. | (6.12) | (6.9)
29. | (6.12) | (6.9)
30. | (6.12) | (6.9)
31. | trivial |
32. | (6.14) | (6.9)
33. | (6.14), (6.15) |
34. | Proposition 6.3.5 |
35. | (6.14), (6.15) |
36. | trivial |
37. | (6.14) | (6.9)
38. | Proposition 6.3.4 |
39. | Proposition 6.3.5 | (6.9)
40. | (6.14), (6.15) |
41. | trivial, (6.13) | (6.9), (6.11)
42. | (6.13) | (6.9)
43. | (6.13), (6.14) | (6.9), (6.10), (6.11)
44. | (6.13) | (6.9)
45. | (6.14), (6.15) |
46. | (6.13) | (6.9), (6.11)
47. | Proposition 6.3.3 |
Rule | Inference modus | Definition
---|---|---
48. | identical |
49. | trivial, (6.8) |
50. | (6.13), (6.8), Proposition 6.3.3 | (6.10)
51. | (6.8) |
52. | identical |
53. | Proposition 6.3.3 |
54. | identical |
55. | trivial |
56. | (6.13), Proposition 6.3.3 | (6.10)
57. | Proposition 6.3.6 with supplementary condition |
58. | (6.13) | (6.10)
59. |  6.3.7 with supplementary condition |
65. |  6.3.7 with supplementary condition |
68. | 6.3.8 |
Table 6.5: Inference rules for implications of $\mathbb{K}_{tt}$ and
$\mathbb{K}_{tmp}$. The second column lists the inference modi or propositions
required for the proofs, the third column implications following from the
definitions of a temporal context.

######  Proposition 6.3.6.

For all $\mathbb{K}_{tt}$ and $\mathbb{K}_{tmp}$ generated by the same
process, the following inference rule holds, if $\forall(s^{in},s^{out})\in
R,\forall y\in Y\colon y\in(s^{out})^{I}\Rightarrow Y\subseteq(s^{out})^{I}$,
especially for $|Y|=1\\!:$

$57\colon X^{in}\wedge Y^{out}\rightarrow
Z^{out},\>X\wedge\operatorname{ev}Y\rightarrow\operatorname{nev}Z\models
X\wedge\operatorname{ev}Y\rightarrow\bot.$

###### Proof.

Suppose there is a state $s_{0}^{in}\in S^{in}$ with attributes $X$ and
$\operatorname{ev}Y$. Then a transition $(s_{0}^{in},s^{out})$ exists in
$\mathbb{K}_{tt}$ with $Y\subseteq(s^{out})^{I}$. For this step the condition
of the proposition is important: A single transition with the property has to
exist, the $y\in Y$ must not be attributes of subsequent states or of states
belonging to different paths. By the first presupposed implication, then also
$Z\subseteq(s^{out})^{I}$. This contradicts the second implication. Hence,
there is no state with attributes $X$ and $\operatorname{ev}Y$ and the second
implication trivially holds, i.e. $X\wedge\operatorname{ev}Y\rightarrow\bot$.
∎

Without the condition for the transitions $(s^{in},s^{out})\in R$, the
inference is valid:

$X^{in}\wedge Y^{out}\rightarrow
Z^{out},\>X\wedge\operatorname{ev}Y\rightarrow\operatorname{nev}Z\models
X^{in}\wedge Y^{out}\rightarrow\bot.$

This is the first inference rule which could not be generally proven during
the attribute exploration of the test context restricted to a three element
attribute set. The supplementary condition mostly restricts $Y$ to a one
element set. This contradicts the aim of proving rules for implications with
set variables, so the condition was not presupposed generally. As mentioned in
the introduction of this section, an alternative would be an expert centered
exploration, where counterexamples are introduced. However, this is out of the
scope of this thesis. Nevertheless, I proved three further rules which express
interesting dynamic dependencies.

######  Proposition 6.3.7.

For all $\mathbb{K}_{tt}$ and $\mathbb{K}_{tmp}$ generated by the same
process, the following inference rules holds, if $\forall\,(s^{in},s^{out})\in
R,\forall\,y\in Y\colon y\in(s^{out})^{I}\Rightarrow Y\subseteq(s^{out})^{I}$,
especially for $|Y|=1\\!:$

$65:Y^{out}\rightarrow
Z^{in},\>\operatorname{ev}Y\rightarrow\operatorname{nev}Z\models\operatorname{ev}Y\rightarrow
Z$ $59:X^{in}\wedge Y^{out}\rightarrow
Z^{in},\>X\wedge\operatorname{ev}Y\rightarrow\operatorname{nev}Z\models\>X\wedge\operatorname{ev}Y\rightarrow
Z.$

###### Proof.

If $Y^{out}\rightarrow Z^{in}$ is supported by any, then by the immediate
preceding transition $(s_{k},s_{k+1})$ and by the transitions
$(s_{k-i},s_{k+1})$ with all previous input states. All underlying paths have
the structure:

$Z-\cdots-Z-Y-\cdots$

Since $\operatorname{ev}Y$ is an attribute of the first state of a path,
$\operatorname{ev}Y\rightarrow\operatorname{nev}Z$ requires the structure:

$Z-Y\overline{Z}-\overline{Z}-\cdots$

Thus, only the first state has the attribute $\operatorname{ev}Y$ and also the
attributes in $Z=Z^{in}$ as demonstrated.
The condition makes sure that there is no other path with a state
$s\in(\operatorname{ev}Y)^{I_{T}}$, but there is no subsequent state
$s^{\prime}\in Y^{I}$. If there is no transition with $Y^{out}$ at all, the
condition implies that $\operatorname{ev}Y$ does not apply to any state, and
the inferred implication trivially holds.

Rule 59 is proven analogously. ∎

######  Proposition 6.3.8.

For all $\mathbb{K}_{tt}$ and $\mathbb{K}_{tmp}$ generated by the same
deterministic process, the inference rule holds:

$68:\top\rightarrow
Z^{in},\>X^{in}\wedge\,\operatorname{alw}Y\rightarrow\operatorname{ev}Z\models
X^{in}\wedge\,\operatorname{ev}Y\rightarrow\operatorname{ev}Z.$

###### Proof.

By $\top\rightarrow Z^{in}$, all but the final states have attributes $Z$. The
same holds for the corresponding output states of a transition. For the last
input state of a path and a deterministic process, $\operatorname{ev}Y$ and
$\operatorname{alw}Y$ have the same meaning, thus the inferred implication
holds, too. ∎

###  6.4 Inference rules for Boolean attributes

In order to get a complete overview on valid entailments for Boolean attribute
values, we performed manual attribute exploration of a test context similar to
Section 6.2.2 with attributes $IF$ as listed below. Formal contexts are
considered where the attributes are dichotomically scaled, i.e.
$\mathbb{K}_{tmp}$ is an extension of a state context according to Definition
4.2.2: $\mathbb{K}_{s}=(S,M,I)$ and $M\subseteq E\times F$. Now
$F:=\\{0,1\\}$. The attributes of $\mathbb{K}_{tt}$ and $\mathbb{K}_{tmp}$ are
constructed as usual from $M$. In the subsequent implications, the sets
$B_{0},B_{1},C_{0},C_{1}$ and $C$ are nonempty subsets of $M$. The indices
express which of the fluents is assigned to the entities: $m=(e,f)\in
B_{0}\text{ or }C_{0}\Rightarrow\gamma(s)(e)=0$ and $m\in B_{1}\text{ or
}C_{1}\Rightarrow\gamma(s)(e)=1$. We suppose that all states and transitions
are completely defined.

  1. 1.

$B^{in}\rightarrow C^{in}$

  2. 2.

$B^{in}\rightarrow C_{0}^{out}\equiv B^{in}\rightarrow$
$\operatorname{nev}C_{1}$

  3. 3.

$B^{in}\rightarrow C_{1}^{out}\equiv B^{in}\rightarrow$
$\operatorname{alw}C_{1}$

  4. 4.

$B^{in}\rightarrow$ $\operatorname{ev}C_{1}$

  5. 5.

$B_{0}^{out}\rightarrow C^{in}$

  6. 6.

$B_{1}^{out}\rightarrow C^{in}$

  7. 7.

$\operatorname{ev}B_{1}$ $\rightarrow C$

  8. 8.

$\operatorname{alw}B_{1}$ $\rightarrow C$

  9. 9.

$\operatorname{nev}B_{1}$ $\rightarrow C$

  10. 10.

$B_{0}^{out}\rightarrow C_{0}^{out}$

  11. 11.

$B_{0}^{out}\rightarrow C_{1}^{out}$

  1. 12.

$B_{1}^{out}\rightarrow C_{0}^{out}$

  2. 13.

$B_{1}^{out}\rightarrow C_{1}^{out}$

  3. 14.

$\operatorname{ev}B_{1}$ $\rightarrow$ $\operatorname{ev}C_{1}$

  4. 15.

$\operatorname{ev}B_{1}$ $\rightarrow$ $\operatorname{alw}C_{1}$

  5. 16.

$\operatorname{ev}B_{1}$ $\rightarrow$ $\operatorname{nev}C_{1}$

  6. 17.

$\operatorname{alw}B_{1}$ $\rightarrow$ $\operatorname{ev}C_{1}$

  7. 18.

$\operatorname{alw}B_{1}$ $\rightarrow$ $\operatorname{alw}C_{1}$

  8. 19.

$\operatorname{alw}B_{1}$ $\rightarrow$ $\operatorname{nev}C_{1}$

  9. 20.

$\operatorname{nev}B_{1}$ $\rightarrow$ $\operatorname{ev}C_{1}$

  10. 21.

$\operatorname{nev}B_{1}$ $\rightarrow$ $\operatorname{alw}C_{1}$

  11. 22.

$\operatorname{nev}B_{1}$ $\rightarrow$ $\operatorname{nev}C_{1}$

The equivalences in 2. and 3. follow from Proposition 6.2.1 (6.3). Since the
implications comprising input attributes are independent from those related
only to output attributes, attribute exploration was performed separately for
the first 9 and the remaining 13 implications. Results for the second part are
shown here.

The exploration with ConImp started from a hypothetical context as single
object of the test context, where no implications are valid. Before, 25 known
entailments were added as background rules (BR) like those of Proposition
6.2.1 or other rules following from the definitions like
$\operatorname{alw}B_{1}\rightarrow\operatorname{ev}B_{1}$. A counterexample
had to be chosen carefully, since an object not having its maximal attribute
set might preclude a valid entailment (compare p. 2.2). The exploration
resulted in the following stem base of only 14 entailments. Most of them are
background rules (they are accepted automatically during the exploration), but
not all of these are needed in order to derive all valid entailments between
the chosen implications. This demonstrates the effectivity and minimality of
the algorithm. Entailments 5., 6., 7. and 10. were new findings.

  1. 1.

$\operatorname{nev}B_{1}$ $\rightarrow$ $\operatorname{alw}C_{1}$ $\models$
$\operatorname{nev}B_{1}$ $\rightarrow$ $\operatorname{ev}C_{1}$ (BR 1)

  2. 2.

$\operatorname{nev}B_{1}$ $\rightarrow$ $\operatorname{ev}C_{1}$,
$\operatorname{nev}B_{1}$ $\rightarrow$ $\operatorname{nev}C_{1}$
$\models\bot$ (BR 11)

  3. 3.

$\operatorname{alw}B_{1}$ $\rightarrow$ $\operatorname{alw}C_{1}$ $\models$
$\operatorname{alw}B_{1}$ $\rightarrow$ $\operatorname{ev}C_{1}$ (BR 2)

  4. 4.

$\operatorname{alw}B_{1}$ $\rightarrow$ $\operatorname{ev}C_{1}$,
$\operatorname{alw}B_{1}$ $\rightarrow$ $\operatorname{nev}C_{1}$
$\models\bot$ (BR 14)

  5. 5.

$\operatorname{ev}B_{1}$ $\rightarrow$ $\operatorname{nev}C_{1}$,
$\operatorname{nev}B_{1}$ $\rightarrow$ $\operatorname{nev}C_{1}$ $\models$
$B_{0}^{out}$ $\rightarrow$ $C_{0}^{out}$, $B_{1}^{out}$ $\rightarrow$
$C_{0}^{out}$

  6. 6.

$\operatorname{ev}B_{1}$ $\rightarrow$ $\operatorname{nev}C_{1}$,
$\operatorname{alw}B_{1}$ $\rightarrow$ $\operatorname{nev}C_{1}$ $\models$
$B_{1}^{out}$ $\rightarrow$ $C_{0}^{out}$

  7. 7.

$\operatorname{ev}B_{1}$ $\rightarrow$ $\operatorname{nev}C_{1}$,
$\operatorname{alw}B_{1}$ $\rightarrow$ $\operatorname{ev}C_{1}$ $\models\bot$

  8. 8.

$\operatorname{ev}B_{1}$ $\rightarrow$ $\operatorname{alw}C_{1}$ $\models$
$\operatorname{ev}B_{1}$ $\rightarrow$ $\operatorname{ev}C_{1}$,
$\operatorname{alw}B_{1}$ $\rightarrow$ $\operatorname{ev}C_{1}$,
$\operatorname{alw}B_{1}$ $\rightarrow$ $\operatorname{alw}C_{1}$ (BR 3)

  9. 9.

$\operatorname{ev}B_{1}$ $\rightarrow$ $\operatorname{ev}C_{1}$ $\models$
$\operatorname{alw}B_{1}$ $\rightarrow$ $\operatorname{ev}C_{1}$ (BR 4)

  10. 10.

$\operatorname{ev}B_{1}$ $\rightarrow$ $\operatorname{ev}C_{1}$,
$\operatorname{nev}B_{1}$ $\rightarrow$ $\operatorname{ev}C_{1}$ $\models$
$B_{0}^{out}$ $\rightarrow$ $C_{1}^{out}$, $B_{1}^{out}$ $\rightarrow$
$C_{1}^{out}$, $\operatorname{ev}B_{1}$ $\rightarrow$
$\operatorname{alw}C_{1}$

  11. 11.

$B_{1}^{out}$ $\rightarrow$ $C_{1}^{out}$ $\models$ $\operatorname{ev}B_{1}$
$\rightarrow$ $\operatorname{ev}C_{1}$, $\operatorname{alw}B_{1}$
$\rightarrow$ $\operatorname{ev}C_{1}$, $\operatorname{alw}B_{1}$
$\rightarrow$ $\operatorname{alw}C_{1}$
(BR 4, BR 5 $\Leftarrow$ Proposition 6.2.1 (6.5) (6.6))

  12. 12.

$B_{1}^{out}$ $\rightarrow$ $C_{0}^{out}$ $\models$ $\operatorname{alw}B_{1}$
$\rightarrow$ $\operatorname{nev}C_{1}$ (BR 9 $\Leftarrow$ Proposition 6.2.1
(6.5))

  13. 13.

$B_{0}^{out}$ $\rightarrow$ $C_{1}^{out}$ $\models$ $\operatorname{nev}B_{1}$
$\rightarrow$ $\operatorname{ev}C_{1}$, $\operatorname{nev}B_{1}$
$\rightarrow$ $\operatorname{alw}C_{1}$
(BR 1, 10 $\Leftarrow$ Proposition 6.2.1 (6.5))

  14. 14.

$B_{0}^{out}$ $\rightarrow$ $C_{0}^{out}$ $\models$ $\operatorname{nev}B_{1}$
$\rightarrow$ $\operatorname{nev}C_{1}$ (BR 6 $\Leftarrow$ Proposition 6.2.1
(6.5))

It remains to prove the rules of this stem base, which is straightforward from
the definitions. I am giving some hints.

BR 1, 2, 3 and 4 are based on
$\operatorname{alw}A\rightarrow\operatorname{ev}A$, $A\subseteq M$, and BR 11
and 14 on
$\operatorname{nev}C_{1}\wedge\operatorname{ev}C_{1}\rightarrow\bot$. Hence,
in BR 14 $\operatorname{alw}B_{1}\rightarrow\bot$ follows in the underlying
contexts. This implication has not been considered explicitly, but it is
presupposed that other implications with $\operatorname{alw}B_{1}$ do not hold
in this case. Their common extent is empty in the test context and
$\emptyset^{\prime}=\bot$ follows.

7.: By the third Armstrong rule (6.13) and
$\operatorname{alw}B_{1}\rightarrow\operatorname{ev}B_{1}$,
$\operatorname{alw}B_{1}\rightarrow(\operatorname{nev}C_{1}\wedge\operatorname{ev}C_{1})$
follows from the presupposed implications. This is precisely the premise of
rule 4 (BR 14).

10.: Inversely, in all possible cases the states / transitions have the
attribute $\operatorname{ev}C_{1}$ and therefore also
$\operatorname{alw}C_{1}$ and $C_{1}^{out}$. This means explicitly:
$\top\rightarrow\operatorname{ev}C_{1}$,
$\top\rightarrow\operatorname{alw}C_{1}$, $\top\rightarrow C_{1}^{out}$. 5. is
a parallel rule concerning $\operatorname{nev}C_{1}$. Rules 7. and 10. suggest
that implications with empty premise $\top$ or with conclusion $\bot$ should
be considered explicitly.

11.: This rule has to be modified slightly for the first inference, according
to a restriction of Proposition 6.2.1 after this exploration had been
finished:

$m_{1}^{out}\rightarrow
C_{1}^{out}\models\operatorname{ev}m_{1}\rightarrow\operatorname{ev}C_{1}\>(m_{1}=(e,1)\in
M).$

As a conclusion it can be stated that we have derived another set of rules
(for Boolean attributes), which can shorten attribute exploration and narrow
the decisions of an expert to really new implications. This rule set
represents a sound and complete entailment calculus for the selected class of
implications for transition and state contexts under the condition of
Proposition 6.3.6:

$\forall(s^{in},s^{out})\in R,\forall m\in B_{1}\colon
m\in(s^{out})^{I}\Rightarrow B_{1}\subseteq(s^{out})^{I},$

in particular if $|B_{1}|=1$.

###  6.5 Overview of the implemented R scripts

Concept Explorer [2] and ConImp [26] were used for attribute exploration. R
scripts were programmed for the following tasks:

  * •

First, thanks to Mike Behrisch for generating all deterministic time series
(including cycles) for 1 to 3 attributes, by his C++ program AllinOne1.1.cpp.
The output files are stored as inferenceRules/ergebnis2-3/ergebnis1.xt,
.../ergebnis2.txt, .../ergebnis.3.txt.

  * •

generateTestContext3.2.r uses:

    * –

The file generateKttKtmpFct1.0.r contains a function generating an apposition
of $\mathbb{K}_{tt}$ (or $\mathbb{K}_{t}$) and $\mathbb{K}_{tmp}^{\prime}$.

    * –

The function testImpFct2.0.r decides about he validity of an implication in an
arbitrary one-valued formal context.

Felix Steinbeck optimised the code so that the script terminated in yet
acceptable time.

  * •

startPartContext.r: R script for the serial computation of the test context.

  * •

The output files were object reduced with ConExp and concatenated to
testContext3AttrImpForms_noEmptyset3.2_complete.txt, a tabulator separated
text file. “noEmptyset” indicates that the empty premise or conclusion were
considered explicitly and only nonempty sets were assigned to the variables
$X,Y$ and $Z$.

  * •

testCxt.cxt: The test context converted by ConExp to the Burmeister format
readable by ConImp.

  * •

testContext3AttrImpForms_noEmptyset3.2_imp.txt: Stem base (inference rules) as
computed by ConExp.

  * •

testCxt.pro (text file): Stem base as computed by ConImp, with short form of
rules highlighting attributes (implicaton forms) not following from previous
rules.

  * •

tCxtImp.duq: Stem base stored in ConImp format.

For details, see the comments within the R files on the attached CD.

##  Chapter 7 Gene regulatory networks I: Analysis of a Boolean network from
literature

###  7.1 Gene regulatory networks

Figure 7.1: Gene expression: the two phases of transcription and translation
[www.scientificpsychic.com/fitness/aminoacids1.html].

To understand normal and destructive cellular reactions, systems biology has
developed models describing processes at the molecular level. A fundamental
process is gene expression, which is a sequence of two phases, transcription
and translation (Figure 7.1): i) during transcription, messenger ribonucleic
acid (mRNA) is produced according to the genetic DNA template (i.e., a DNA
sequence coding for a single protein); and ii) during translation, proteins
are built from amino acids using these mRNA templates. [9]

Proteins are the main regulators of living organisms; they activate almost
every chemical reaction within an organism as enzymes, build new structures
during cell division or transduce biochemical signals from the cell surface to
the cytoplasm and the nucleus, e.g., by phosphorylation of target proteins.
These signals can activate another class of proteins, the transcription
factors, which bind to the DNA and thus are able to initiate, enhance or
repress transcription. [9]

Mathematical and computational models may assist biologists in further
research activities by generating predictions and hypotheses that can be
experimentally tested. Network models, generated on the basis of extracted
information and/or experimental data, facilitate the analysis of interactions
among different key molecules and provide new insight into complex biological
pathways and interactions (for an overview of methods see [88] and [50]).

In the present chapter, the proposed method is applied to the analysis of a
gene regulatory network assembled from literature and database information in
[31] and transformed to a Petri net as well as a Boolean network in [91].

###  7.2 Sporulation in Bacillus subtilis

B. subtilis is a gram positive soil bacterium. Under extreme environmental
stress, it produces a single endospore, which can survive ultraviolet or gamma
radiation, acid, hours of boiling or long periods of starvation. The bacterium
leaves the vegetative growth phase in favour of a dramatically changed and
highly energy consuming behaviour, and it dies at the end of the sporulation
process. This corresponds to a switch between two clearly distinguished
genetic programs, which are complex but comparatively well understood.

By literature and database search, de Jong et al. [31] identified 12 main
regulators, constructed a model of piecewise linear differential equations and
obtained realistic simulation results. An exogenous signal (starvation)
triggers the phosphorylation of the transcription factor Spo0A to Spo0AP by
the kinase KinA. This process is reversible by the phosphatase Spo0E. Spo0AP
is necessary to transcribe SigF, which regulates genes initiating sporulation
and therefore is an output of the model. The interplay with other
transcription factors AbrB, Hpr, SigA, SigF, SigH and SinR is graphically
represented in [31, Figure 3]. SinI inactivates SinR by binding to it. SigA
and Signal are considered as an input to the model and are always on. Table
7.1 lists the Boolean equations building the model in [91]. They exhibit a
certain degree of nondeterminism, since the functions for the off fluents
sometimes are not the negation of the on functions. This accounts for
incomplete or inconsistent knowledge. In the case of state transitions
determined by $k$ conflicting function pairs, $2^{k}$ output states were
generated.

AbrB | = | SigA $\overline{\text{AbrB}}$ $\overline{\text{Spo0AP}}$
---|---|---
$\overline{\text{AbrB}}$ | = |  $\overline{\text{SigA}}$ \+ AbrB + Spo0AP
SigF | = | (SigH Spo0AP $\overline{\text{SinR}})$ \+ (SigH Spo0AP SinI)
$\overline{\text{SigF}}$ | = | (SinR $\overline{\text{SinI}}$) + $\overline{\text{SigH}}$ \+ $\overline{\text{Spo0AP}}$
KinA | = | SigH $\overline{\text{Spo0AP}}$
$\overline{\text{KinA}}$ | = |  $\overline{\text{SigH}}$ \+ Spo0AP
Spo0A | = | (SigH $\overline{\text{Spo0AP}}$) + (SigA $\overline{\text{Spo0AP}}$)
$\overline{\text{Spo0A}}$ | = | ($\overline{\text{SigA}}$ SinR $\overline{\text{SinI}}$) + ($\overline{\text{SigH}}$ $\overline{\text{SigA}}$ ) + Spo0AP
Spo0AP | = | Signal Spo0A $\overline{\text{Spo0E}}$ KinA
$\overline{\text{Spo0AP}}$ | = |  $\overline{\text{Signal}}$ \+ $\overline{\text{Spo0A}}$ \+ Spo0E + $\overline{\text{KinA}}$
Spo0E | = | SigA $\overline{\text{AbrB}}$
$\overline{\text{Spo0E}}$ | = |  $\overline{\text{SigA}}$ \+ AbrB
SigH | = | SigA $\overline{\text{AbrB}}$
$\overline{\text{SigH}}$ | = |  $\overline{\text{SigA}}$ \+ AbrB
Hpr | = | SigA AbrB $\overline{\text{Spo0AP}}$
$\overline{\text{Hpr}}$ | = |  $\overline{\text{SigA}}$ \+ $\overline{\text{AbrB}}$ \+ Spo0AP
SinR | = | (SigA $\overline{\text{AbrB}}$ $\overline{\text{Hpr}}$ $\overline{\text{SinR}}$ $\overline{\text{SinI}}$ Spo0AP) +
|  | (SigA $\overline{\text{AbrB}}$ $\overline{\text{Hpr}}$ SinR SinI Spo0AP)
$\overline{\text{SinR}}$ | = |  $\overline{\text{SigA}}$ \+ AbrB + Hpr + (SinR $\overline{\text{SinI}}$) + ($\overline{\text{SinR}}$ SinI) + $\overline{\text{Spo0AP}}$)
SinI | = | SinR
$\overline{\text{SinI}}$ | = | $\overline{\text{SinR}}$
SigA | = | TRUE (input to the model)
Signal | = | TRUE or FALSE (constant, depending on the initial state)
Table 7.1: Boolean rules for the nutritional stress response regulatory
network, derived in [91] from [31]. $\overline{x}\hat{=}\neg
x,\>x+y\,\hat{=}\,x\vee y,\>xy\,\hat{=}\,x\wedge y$.

Since the validation of the model by data and experimental literature has been
done before in [31], we analysed pure knowledge-based simulations. For that
reason, in step 5 of the protocol (p. 5.2), the stem base is computed
automatically without further confirmation by an expert. The developed R [6]
scripts for simulation, for generating the transitive contexts and for
converting a stem base into Prolog format are indicated in Section 8.2.7.

###  7.3 Simulation starting from a state typical for the vegetative growth
phase

We performed supplementary analyses of the transitions starting from a typical
state without the starvation signal [91, Table 4].

Transition |  KinAin |  Spo0Ain |  Spo0APin |  AbrBin |  Spo0Ein |  SigHin |  Hprin |  KinAout |  Spo0Aout |  Spo0APout |  AbrBout |  Spo0Eout |  SigHout |  Hprout
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---
$(s_{0}^{in},s_{1}^{out})$ | - | + | - | - | - | - | + | - | + | - | + | + | + | -
$(s_{0}^{in},s_{2}^{out})$ | - | + | - | - | - | - | + | + | + | - | - | - | - | +
$(s_{1}^{in},s_{1}^{out})$ | - | + | - | + | + | + | - | - | + | - | + | + | + | -
$(s_{1}^{in},s_{2}^{out})$ | - | + | - | + | + | + | - | + | + | - | - | - | - | +
$(s_{2}^{in},s_{1}^{out})$ | + | + | - | - | - | - | + | - | + | - | + | + | + | -
$(s_{2}^{in},s_{2}^{out})$ | + | + | - | - | - | - | + | + | + | - | - | - | - | +
Table 7.2: The (many-valued) transitive context corresponding to a simulation
starting from a B. subtilis state without nutritional stress [91, Table 4]. +:
on, -: off. Only the attributes are listed that are changing during the
simulation as well as Spo0A and Spo0AP.

The concept lattice for the resulting transitive context (Table 7.2, with only
a part of the attribute set only) is shown in Figure 7.2.

Figure 7.2: Concept lattice (computed and drawn with Concept Explorer [2])
representing a simulation without nutritional stress. Signal: starvation;
AbrB, Hpr, SigA, SigF, SigH, SinR, Spo0A (phosporylated form Spo0AP):
transcription factors – SigF initiates sporulation; KinA: kinase; Spo0E:
phosphatase; SinI inactivates SinR by binding to it. $i$-$j$ indicates a
transition ($s_{i}^{in},s_{j}^{out})$. Bold / blue lines: Filter
(superconcepts) and ideal (subconcepts) of the concept
({($s_{0}^{in},s_{1}^{out}),(s_{0}^{in},s_{2}^{out}),(s_{2}^{in},s_{1}^{out}),(s_{2}^{in},s_{2}^{out})$},
{AbrB.in.off, SigH.in.off, Spo0E.in.off, Hpr.in.on})

The larger circles at the bottom represent object concepts; their extents are
the four single transitions with the input state at $t=0$ or $t=2$, and the
intents are all attributes above a concept. Thus for instance, the two latter
transitions have the attribute KinA.in.on in common, designating the
respective concept. Moreover, they are distinguished unambigously from other
sets of transitions by this attribute – the concept is generated by
“KinA.in.on”.

Implications of the stem base can be read from the lattice. For instance there
are implications between the generators of a concept:

$<4>\text{ AbrB.in.off $\rightarrow$ SigH.in.off, Spo0E.in.off, Hpr.in.on}$
(7.1)

Analogous implications hold for the attributes of the conclusion, and there
are implications between attributes of sub- and superconcepts. $<4>$ indicates
that the rule is supported by four transitions.

The bottom concept has an empty extent. Its intent is the set of attributes
never occuring during this simulation comprising only three time steps. The
top concept does not have an empty intent – as it is often the case –, but it
consists of 10 attributes common to all 6 transitions. The corresponding rule
has an empty body ($\top$):

$\displaystyle<6>\>\top\rightarrow$ Signal.in.off, SigA.in.on, SigF.in.off,
Spo0A.in.on, Spo0AP.in.off, (7.2) SinR.in.off, SinI.in.off, Signal.out.off,
SigA.out.on, SigF.out.off, Spo0A.out.on, Spo0AP.out.off, SinR.out.off,
SinI.out.off

The transitive context generated by a simulation following nutritional stress
has about 20 transitions, 500 concepts and 50 implications. In such a case it
is more convenient to query the implicational knowledge base. But also for the
visualisation of large concept hierarchies, there exist more sophisticated
tools like the ToscanaJ suite [7].

###  7.4 Analysis of all possible transitions

In order to analyse the dynamics of the B. subtilis network exhaustively, I
generated 4224 transitions from all possible $2^{12}=4096$ initial states
(thus the rules are nearly deterministic). There were 11.700 transitions in
the transitive context, from which the stem base was computed containing 524
implications with support $>$ 0, but $11.023.494\approx 2^{24}$ concepts.

It was not feasible to provide biological evidence for a larger part of the
implications, within the scope of this methodological study. This could be
done by literature search, especially automatic text mining, by new specific
experiments or by comparison with observed time series ([110, 3.2], Chapter
8). Instead examples will be given for classes of implications that can be
validated or falsified during attribute exploration in specific ways. I start
with the examples of [91, 4.3].

  * •

“For example, we know that in the absence of nutritional stress, sporulation
should never be initiated [31]. We can use model checking to show this holds
in our model by proving that no reachable state exists with SigF = 1 starting
from any initial state in which Signal = 0, SigF = 0 and Spo0AP = 0.” [91, p.
341] This is equivalent to the rule following from the stem base:

$\text{Signal.in.off, SigF.in.off,
Spo0AP.in.off}\rightarrow\text{SigF.out.off}$ (7.3)

  * •

SigF.out.on $\rightarrow$ KinA.out.off, Spo0A.out.off, Hpr.out.off,
AbrB.out.off:
Spo0AP is reported to activate the production of SigF but also to repress its
own production (mutual exclusion). [31]

  * •

SigH.out.off $\rightarrow$ AbrB.out.off, Spo0E.out.off, SinR.out.off,
SinI.out.off
All these genes are regulated
$\overline{gene.out}=\overline{\text{SigA.in}}+\text{AbrB.in}$ (+ …).

In our approach, such dependencies and mutual exclusions can be checked
systematically. We searched the stem base for further interesting and simple
implications:

$\displaystyle<4500>\text{Spo0AP.in.on,
KinA.out.off}\rightarrow\text{Hpr.out.off}$ (7.4)
$\displaystyle<4212>\text{SigH.in.on.
KinA.out.off}\rightarrow\text{Hpr.out.off}$ (7.5)
$\displaystyle<3972>\text{AbrB.in.off,
KinA.out.off}\rightarrow\text{Hpr.out.off}$ (7.6)

$\overline{\text{Hpr}}$ and $\overline{\text{KinA}}$ are determined by
different Boolean functions, but they are coregulated in all states emerging
from any input state characterised by the single attributes Spo0AP.on, SigH.on
or AbrB.on.

$\displaystyle<3904>\text{AbrB.out.on }\rightarrow$ SigA.in.on, SigA.out.on,
SigF.out.off, (7.7) Spo0A.out.on, Spo0E.out.on, SigH.out.on, Hpr.out.off,
SinR.out.off, SinI.out.off

AbrB is an important “marker” for the regulation of many genes, which is
understandable from the Boolean rules with hindsight. By a PubMed query, a
confirmation was found for the downregulation of SigF together with the
upregulation of AbrB [96].

Finally, we entered sets of interesting attributes into the Prolog knowledge
base, such that a derived implication was computed, and accordingly the
closure of the attribute set. In order to avoid infinite regresses, tabled
resolution has been applied, which is implemented in the Prolog extension XSB
[http://xsb.sourceforge.net]. Complementary to (7.3), we searched after
conditions for an eventual switch towards sporulation (SigF.out.on). If the
premise is entered as set of facts off(sigF.in), off(Spo0AP.in) and
on(sigF.out), then with the implications of the stem base the conclusion is
returned as a set of derived facts. For the analysed complete simulation, the
conditions Signal = SigA = TRUE had been dropped, but they were supposed to be
constant (see the first four implications, which in Prolog are read from right
to left).

          :- table off/1.
          :- table on/1.

          off(sigF.in).
          off(Spo0AP.in).
          on(sigF.out).

          on(signal.in)   :- on(signal.out).
          on(signal.out)  :- on(signal.in).
          on(sigA.in)     :- on(sigA.out).
          on(sigA.out)    :- on(sigA.in).
          off(abrB.out)   :- on(sigF.out).
          off(kinA.out)   :- on(sigF.out).
          off(Spo0AP.out) :- off(spo0A.in), on(sigF.out).
          on(signal)      :- off(sigH.in), on(sigF.out).
          ...

The subsequent implication was found:

SigF.in.off, Spo0AP.in.off, SigF.out.on (7.8) $\displaystyle\rightarrow$
Signal.in.on, Signal.out.on, SigA.in.on, SigA.out.on, Spo0AP.out.off,
Spo0A.out.off, AbrB.out.off, KinA.out.off, Hpr.out.off.

The latter four attributes follow immediately from the Boolean rules, but
Spo0AP.out.off depends in a more complex manner on the premises. It is also
noteworthy that the class of input states developing to a final state with
attribute SigF.out.on is characterised only by the attributes Signal.in.on and
the ubiquitous transcription factor SigA.in.on, i.e. the initial presence or
absence of no other gene is necessary for the initiation of sporulation.

##  Chapter 8 Gene regulatory networks II: Adapted Boolean network models for
extracellular matrix formation

###  8.1 Biomedical and bioinformatics background

Rheumatoid arthritis (RA) is a systemic (whole body) autoimmune disease, the
causes of which are incompletely elucidated so far. Autoantibodies are
directed against citrullinated proteins, where one or several arginine amino
acids are post-translationally modified. Susceptibility factors are the
genotype of the antigen presenting major histocompatibility complex HLA-DRB1,
smoking, and there is a higher risk for women pointing at hormonal factors.
The immune disorder might also be triggered by a viral or bacterial infection.
[101]

Our focus is a better understanding of the symptom generating processes and
the therapy against the cytokine TNF$\alpha$. RA is characterised by chronic
inflammation and destruction of multiple joints perpetuated by the synovial
membrane (SM). A major component of the inflamed SM (also called pannus
tissue) are activated, semi-transformed synovial fibroblasts (SFB, or
synoviocytes) [8] [55] [57] [65] [90]. In normal joints, SFB show a balanced
expression of proteins, regulating the formation and degradation of the
extracellular matrix (ECM), a fibrous structure providing support to the cells
(besides other functions). In RA, however, SFB are known for predominant
expression and secretion of pro-inflammatory cytokines and tissue-degrading
enzymes [57] [65], thus maintaining joint inflammation and degradation of ECM
components of cartilage and bone, which are also invaded by SFB. In addition,
enhanced formation of soft ECM components such as collagens in the affected
joints (an attempt of wound healing resulting in fibrosis) is also driven by
SFB [81].

Figure 8.1: The knee joint: normal morphology (left) and schematic
representation of rheumatoid arthritis features (right) [90, Figure 1].

Central transcription factors (TFs) involved as key players in RA pathogenesis
[34] [115] and in the activation of SFB in RA patients are AP‑1, NF-$\kappa$B,
ETS‑1, and SMADs [13] [16] [34] [47]. These TFs show binding activity for
their cognate recognition sites in the promoters of inflammation-related
cytokines (e.g., TNF$\alpha$, IL1$\beta$, IL6 [8]) and matrix-degrading target
genes [34] [48] [76] [104] [115], e.g., collagenase (MMP‑1) [8] and
stromelysin1 (MMP‑3) [76]. The latter two show high expression levels in RA
[35] [43] [73] and contribute to tissue degradation [103] by destruction of
ECM components, including aggrecan or collagen types IV, X, and XI [102]
[113].

Mathematical and computational models are of particular importance in the
context of rheumatic diseases and cartilage/bone metabolism, since the
development of new and/or adapted molecular therapies depends on the
understanding of superordinate pathway interrelationships in the pro-
inflammatory microenvironment of the joint [57]. Therefore, we developed a
method for simulating the temporal behaviour of regulatory and signalling
networks. It was used to create two gene regulatory networks emulating ECM
formation and destruction, based on literature information about SFB on the
one hand and on experimental data on the other, which we obtained from
TGF$\beta$1 or TNF$\alpha$ stimulated SFB. As motivated in Section 3.3.2, we
applied Boolean network architecture for modelling. Using attribute
exploration, the simulation results and the observed time series were further
integrated in a fine-tuned and automated manner resulting in sets of rules
that determine system dynamics.

For our analysis we used a collection of 18 genes, which can be classified
into five functional groups, sufficient to create a self-contained regulatory
network of ECM maintenance: (1) structural proteins which are the target
molecules (i.e., the collagen-forming subunits COL1A1 and COL1A2); (2) enzymes
degrading them (i.e., the matrix metalloproteinases MMP1, -3, ‑9, and ‑13);
(3) molecules that inhibit these proteases (tissue inhibitor of
metalloproteinases TIMP1); (4) TFs (i.e., ETS1, FOS, JUN, JUNB, JUND, NKFB1)
and modulators acting as TFs (i.e., SMAD3, SMAD4, SMAD7) which are regulated
by (5) the external signalling molecules TNF$\alpha$ (TNF) and TGF$\beta$1
(TGFB1). These genes (Figure 8.2) are known to be expressed by SFB, except for
TNF and MMP9, for which the expression is still under question (compare p. 10,
8.3.7).

Figure 8.2: List of genes used in this analysis.

###  8.2 Methods

####  8.2.1 Clinical data

##### Patients and samples

Synovial membrane samples were obtained following tissue excision upon joint
replacement/synovectomy from RA and osteoarthritis (OA) patients ($n$ = 3
each; Figure 8.3). Informed patient consent was obtained and the study was
approved by the ethics committees of the respective university. RA patients
were classified according to the American College of Rheumatology (ACR)
criteria [14, p. 234], OA patients according to the respective criteria for
osteoarthritis [11, p. 237].

The preparation of primary SFB from RA and OA patients was performed as
previously described [116, p. 235]. Briefly, the tissue samples were minced
and digested with trypsin/collagenase P. The resulting single cell suspension
was cultured for seven days. Non-adherent cells were removed by medium
exchange. SFB were then negatively clarified using
Dynabeads${}^{\text{\textregistered}}$ M‑450 CD14 and subsequently cultured
over 4 passages in DMEM containing 100 $\mu$g/ml gentamycin, 100 $\mu$g/ml
penicillin/streptomycin, 20 mM HEPES (all from PAA Laboratories, Coelbe,
Germany), and 10 % FCS (BioWhittaker-Lonza, Basel, Switzerland).

Figure 8.3: Clinical characteristics of the patients at the time of
synovectomy/sampling. 1Erythrocyte sedimentation rate, 2C-reactive protein,
normal range: $<$ 5 mg/l, 3American Rheumatism Association (now: American
College of Rheumatology) 4Methotrexate 5Non steroidal anti-inflammatory drugs.

##### Cell stimulation and isolation of total RNA

At the end of the fourth passage, SFB were stimulated by 10 ng/ml TGF$\beta$1
or TNF$\alpha$ (PeproTech, Hamburg, Germany) in serum-free DMEM for 0, 1, 2,
4, and 12 h. At each time point, the medium was removed and the cells were
harvested after treatment with trypsin (0.25% in versene; Invitrogen,
Karlsruhe, Germany). After washing with PBS, they were lysed with RLT buffer
(Qiagen, Hilden, Germany) and frozen at ‑70°C. Total RNA was isolated using
the RNeasy Kit (Qiagen) according to the supplier’s recommendation.

##### Microarray data analysis

Analysis of gene expression was performed using U133 Plus 2.0 RNA microarrays
(Affymetrix${}^{\text{\textregistered}}$, Santa Clara, CA, USA). Labelling of
RNA probes, hybridisation, and washing were carried out according to the
supplier’s instructions. Microarrays were analysed by laser scanning (Hewlett-
Packard Gene Scanner). Background-corrected signal intensities were determined
and normalised using the MAS 5.0 software
(Affymetrix${}^{\text{\textregistered}}$). For this purpose, arrays were
grouped according to the respective stimulus (TGF$\beta$1 and TNF$\alpha$,
$n=6$ each). The arrays in each group were normalised using quantile
normalisation [24, p. 236]. Original data from microarray analysis have been
deposited in NCBI Gene Expression Omnibus [3] and are accessible through GEO
series accession number GSE13837. A list of probe sets and all expression time
courses are provided in additional file 4.

####  8.2.2 Creating network and Boolean functions

For the selection of genes and proteins involved in ECM maintenance and for
network generation, Boolean queries were performed in PubMed [5]. Articles
were selected containing information about relevant genes expressed in SFB and
involved in ECM maintenance. For information extraction, the abstracts were
screened and filtered manually for statements on healthy conditions only. This
knowledge-based collection yielded the set of gene candidates analysed in
detail. The final gene list is presented in Figure 8.2.

The genes were also analysed using Bibliosphere [1] and literature not
extracted from PubMed was added. Subsequently, information concerning
regulatory relationships was collected and transformed into short statements
serving as input relations (edges) for the network building program Cytoscape,
version 2.6.0 [89]. Contradictory literature information was resolved by
preferring facts applying to the target cell type (human fibroblasts) and/or
by comparison with experimental gene expression results from our and other
microarrray data (GSE1742 and GSE2624, see additional file 5). The complete
list of used statements and the respective literature basis can be found in
additional file 1. In a further step, simulation results were iteratively
compared to the experimental data in the present study, resulting in two
adapted Boolean networks which represent hypotheses about regulatory processes
initiated by TGF$\beta$1 and TNF$\alpha$.

####  8.2.3 Data discretisation

Since we were interested in regulatory interactions, the fold-change of the
expression values was more important than absolute levels. Hence, we
discretised individual time series separately. The discretised data served to
verify or falsify the temporal dependencies predicted from the extracted
literature knowledge. For that reason, we wanted to conserve as many effects
on gene expression as possible and set weak criteria for up-regulation: if the
highest fold-change (i.e., the difference of $\operatorname{log}_{2}$ values)
between two arbitrary time points was larger than 1, then the time profile was
discretised to 0 or 1 by k-means clustering (100 iterations, vote of 25
restarts). We set the constant value 0 if: (i) the highest fold-change between
two arbitrary points in a time series was less than 1; (ii) the absolute
expression value was below the threshold of 100 for one probe set; or (iii)
the Affymetrix detection value $p$ indicating the reliability of the
measurement exceeded 0.05. In all other cases, the constant was set to 1.
Applying these criteria, also individual values were set to 0 (i.e., off)
following clustering.

####  8.2.4 Principles of simulation

Using the deterministic Boolean network, simulations were generated using an
asynchronous update scheme based on the subsequent biologically-founded
assumptions. In order to simulate the time courses more realistically,
transcription and translation were separated, i.e., the left side of a Boolean
function (output) was considered as mRNA and the right side as TF and/or
stimulus (input). Unfortunately, time-resolved data for gene expression
events, mRNA, or protein half-life are scarce in the literature. Therefore,
time steps were selected based on general expert knowledge and comparison of
literature and experimental data, if available. For example, the duration of
transcription was generally set to 1 time unit, for NF-$\kappa$B it was set to
a doubled time period, reflecting its markedly prolonged response time before
expression compared to the immediate early response transcription factors AP-1
and ETS1 [25].

In summary, we selected the time steps as follows: transcription 1 (NFKB1: 2),
translation: 1, mRNA lifespan: 1, and protein lifespan: 2. Since TGF$\beta$1
and TNF$\alpha$ have to be released into the extracellular medium after
translation, they were assumed to take effect three time units after
induction. The starting conditions of the simulations were characterised by
the initially observed, discretised states, and an initial state was
introduced, for which the TFs were set to on. Supposing a steady state
situation before starting the stimulation with TGF$\beta$1 and TNF$\alpha$,
the protein levels at step 0 and 1 were defined according to that of the
corresponding mRNA, and, in addition, the respective stimulating protein was
set to on. The simulations were performed over twelve time units, roughly
corresponding to the twelve hour duration of the gene expression experiments.

####  8.2.5 Creation of a temporal rule knowledge base

The sets of observed and simulated states $S^{obs}$ and $S^{sim}$ were
characterised by the expression levels of each gene, i.e., by a subset of
attributes $M = E \times F$, with entities or genes $E$, and the corresponding
values $F = \\{\text{off, on}\\}$. Hence, they were assembled into state
contexts (Definition 4.2.2) $\mathbb{K}_{s}^{obs}$ and $\mathbb{K}_{s}^{sim}$.
A state can be considered as a tuple $(f_{1},..., f_{n})$ with $f_{i} \in F,n
= |E|$.

The transitions after one time step define relations $R^{obs}\subseteq S^{obs}
\times S^{obs}$ and $R^{sim} \subseteq S^{sim} \times S^{sim}$ on the states.
Thus, in general multiple output states $s^{out}$ following an input state
$s^{in}$ are possible. However, this case rarely occurred, justifying the use
of a deterministic simulation procedure.

We computed the transitive closure of these relations, since we were
interested in all states emerging from a given one, within the observation or
simulation time. The data of all time series related to one stimulus was
assembled in the transitive contexts (Definition 4.4.1)
$\mathbb{K}_{tt}^{obs}$ and $\mathbb{K}_{tt}^{sim}$. These define relations
$I$ between objects (the transitions) and attributes (the discretised gene
expression levels in input and output states).

By attribute exploration, we compared the literature-based implications with
those merely derived from the data and applied a strong criterion:
implications of $\mathbb{K}_{tt}^{sim}$ had to be valid for all transitions of
the observed context $\mathbb{K}_{tt}^{obs}$. This is equivalent to an
exploration of the union of the two contexts, where every proposed implication
is accepted. Thus, the resulting stem base was computed automatically with the
Java tool Concept Explorer, which supports also expert centered attribute
exploration [2]. The other calculations were made with my own R [6] programs
(Section 8.2.7). Computing the 2713 (8785) TGF$\beta$1 (TNF$\alpha$) rules,
Concept Explorer ran 21 (30) minutes on a 2.66 GHz/2 GB computer.

####  8.2.6 Expert analysis of transition rules

The calculated transition rules were screened manually, focussing on the
appearance and the temporal behaviour of the following features: (i)
constitutive vs. induced gene expression; (ii) co-expression vs. divergent
expression of mediators, TFs, and target genes; (iii) expression of
mediators/transcription factors vs. expression of target genes; (iv)
regulation of target gene expression based on the expression of different
transcription factors; (v) expression of individual genes vs. expression of
their functional groups; and (vi) discrepancies to the literature.
Subsequently, the extracted rules were assessed with respect to biological
coherence and relevance.

####  8.2.7 Overview of the implemented R scripts

The following R scripts have been developed; most of them were also utilised
for the B. Subtilis network analysis of Chapter 7.

  * •

discretise4.1.r.
Data discretisation as described above.

  * •

simulationTnf.r, simulationTgf.r.
Simulations according to the Boolean networks.
(allStates.r: Simulations for the nondeterministic B. subtilis network,
starting from all possible initial states.)

  * •

aposterioriTrans2.0.r.
Generate a transition and a transitive context from observed or simulated
data.

  * •

selectGenes2.1.r.
Compute support and confidence of a rule in an (observed) transition context,
show transitions in the observed and simulated context with the premise
attributes.
Provides a decision criterion for expert attribute exploration.

  * •

convert2Prolog.r.
Convert a stem base into Prolog format for queries.

####  8.2.8 Additional files

In the data CD, the R scripts are included as well as the additional files
published with [109], at http://www.biomedcentral.com/content/supplementary/:

  * •

1752-0509-3-77-S1.doc.
Literature used for the network construction. Each citation corresponds to one
edge in the regulatory network.

  * •

7521-0509-3-77-S2.zip.
Cytoscape import file. Import this file into Cytoscape [89] to analyse the
gene regulatory network in more detail. It also includes external links for
the genes and references cited to GenBank, Uniprot, and PubMed.

  * •

7521-0509-3-77-S3.zip.
Cytoscape import file. Open this file after importing the CYS file (provided
by Additional file 2) into Cytoscape [89] if the layout of the CYS file cannot
be displayed correctly with your Cytoscape version.

  * •

7521-0509-3-77-S4.xls.
List of probe sets used, processed microarray data and visualisation of
expression time courses for the genes analysed. Raw data are deposited under
accession number GSE13837 at GEO [3].

  * •

7521-0509-3-77-S5.xls.
Processed and visualisation of GEO Data. Data were extracted from GSE1742
(TGF$\beta$1) and GSE2624 (TNF$\alpha$) at GEO [3].

  * •

7521-0509-3-77-S6.xls.
Discretised gene expression time courses.

  * •

7521-0509-3-77-S7.xls.
Histograms of gene expression simulation. The simulations for TGF$\beta$1
(blue) and TNF$\alpha$ (red) were run for 12 time steps (x-axis) and for each
initial state derived from the patients’ data separately. A simulated
expression of 100% (y-axis) means that in all six cases the gene was on.

  * •

7521-0509-3-77-S8.xls.
List of the top 500 knowledge base rules valid for the simulations as well as
for the data from stimulations with TGF$\beta$1 and TNF$\alpha$.

  * •

ECMData.xls
Measured values for probesets, after normalization of mean and variance for
all TGFB1 and TNF chips, respectively. Selection of probesets, logarithmic
values of the geometric mean for one gene.

Moreover, the attached CD contains the discretised measured and simulated data
as formal contexts (*.txt files readable also with Concept Explorer [2]), as
well as the complete stem bases in *.txt and PROLOG format (see contents at
readme.txt).

###  8.3 Results and discussion

####  8.3.1 Creating a regulatory network by information extraction from
literature

The available literature was screened for genes and proteins involved in ECM
maintenance and expressed in the lining layer SFB of the SM. In order to
derive a regulatory network, we comprehensively collected literature knowledge
related to the formation and degradation of ECM in human fibroblasts and
analysed it manually. We chose collagen type I, which is formed by the COL1A1
and COL1A2 gene products, as a connective tissue representative, several MMPs
as ECM-degrading enzymes, their inhibitors, and TFs regulating them. Finally,
we selected 18 genes (Figure 8.2) and the literature was screened again for
gene regulatory relations and interactions connecting them (see additional
file 1 for a complete list). Some contradictory literature findings were
resolved manually (see Section 8.3.5).

The resulting regulatory network is almost closed and represents the most
important ECM network functions. Here, we imply that the receptors for the
external signalling molecules are always available and functional in SFB.
Note, that TGF$\beta$1 (TGFB1) and TNF$\alpha$ (TNF) are the only entities
playing a dual role as both external signal molecules and target genes because
of their introduction into the simulation as starting effectors.

It turned out that the knowledge about gene regulatory events is limited and
that, to the best of our knowledge, the regulation of SMAD and SMAD expression
has not been fully characterised so far. The SMAD gene products seem to be
available in sufficient amounts and we were unable to find reports about their
regulated expression. In addition, not all influences of TGF$\beta$1 and
TNF$\alpha$ on gene expression could be described as direct effects of
transcription factors at the mRNA level because the important SMAD family
members act as regulators on the protein-protein interaction level. All
influences were included in the network at this point to avoid premature loss
of information.

Figure 8.4: Overview of the ECM network in hierarchical order. Regulatory
effects via TFs are shown as continuous lines, others as indirect effects as
dashed lines. Inhibition is marked by a red T-arrow, induction is illustrated
by black arrows. The external signals TGF$\beta$1 and TNF$\alpha$ are shown as
light grey circles, the internal SMAD signalling molecules as dark grey
squares, TFs are depicted as black (AP‑1 components) or white squares, and the
target genes are shown as white octagons. This picture was generated using
Cytoscape 2.6.0.

Although many TFs such as AP‑1 are also regulated at the protein level (e.g.,
by phosphorylation), those effects can be reflected simplistically by
regulatory processes at the transcriptional level. However, activating SMADs
as SMAD3 and SMAD4 are also regulated by inhibitory members of the SMAD family
(SMAD6 and SMAD7), which may counteract transcriptional activation and add an
extra level of complexity [85]. Therefore, SMAD7 was introduced into the
network as a TGF$\beta$1-dependent repressor of SMAD-dependent transcription.

In the case of SMAD3, we decided to subsume its influence under the SMAD4
effects because both are described to have nearly identical effects and act in
concert. Moreover, we could not find well-defined information about SMAD3
regulation. Hence, we added an inducing influence of SMAD4 on MMP13 (at
present only known for SMAD3) for keeping all the SMAD effects in the network.

The subunits of the homo- or heterodimer TF AP‑1, i.e., Jun, JunB, JunD, and
Fos (JUN, JUNB, JUND, FOS), determine its different regulatory activities (for
AP‑1 components see [51] and references therein). Therefore, we decided to
disassemble the transcriptional active entity AP‑1 into its subunits. In
contrast, for the dimeric TF NF‑$\kappa$B, which can be composed of the gene
products of NFKB1, NFKB2, RELA, RELB, and/or REL [79], we selected NFKB1 as
the representative gene with respect to our signalling framework. All the
genes and their interrelations were transferred into the program Cytoscape
[89] to visualise our network containing 19 nodes and 79 edges, respectively,
as shown in Figure 8.4. Detailed network examination is available through the
network description files (additional files 2 and 3), also providing external
links to GenBank, Uniprot, and PubMed for all edges and nodes.

Available tools for automatic text mining decide schematically, e.g., by pre-
built rules like co-occurrence of gene names and interaction verbs or pattern
matching, whereas a human expert is able to integrate unanticipated types of
information and to decide whether the paper confirms the investigated
situation. However, we used the tools Bibliosphere [1] and Pathway Studio [4]
in order to verify completeness and consistency of the assembled network (data
not shown).

####  8.3.2 Boolean functions

Due to its capability for displaying dynamic dependencies between individual
parameters, a Boolean network is more specific than the graphical network in
Figure 8.4, which summarises isolated literature facts. In order to decide
about the connectives OR/AND, which represent causally determined relations
between different genes, cellular signalling processes were also considered.

In the case of a known transcriptional activation of any gene by the stimuli
TNF$\alpha$ or TGF$\beta$1 via a specific TF, this activation was represented
in the network using the term GENE.out = STIMULUS AND TF. Without such
evidence, these influences were connected by GENE.out = STIMULUS OR TF. Since
it is well known that the so-called SMAD pathway is activated by TGF$\beta$1
but not influenced by TNF$\alpha$ [97], we used the AND connection for SMAD3/4
and TGF$\beta$1, even if there was no explicit literature evidence for an
impact of TGF$\beta$1 onto the respective gene.

Another example for setting up the functions is the integration of: (i) the
known auto-regulatory transcriptional activation of JUN by TNF$\alpha$ via
JUN, and (ii) the activation of JUN via SMAD4 (TNF$\alpha$-independent) into
the single Boolean function 5 (compare Table 8.5 with Tables 8.7 and 8.8):
JUN.out = (TNF AND JUN) OR SMAD4. Based on the illustrated principles, the
Boolean functions characterising formation and remodelling of the ECM were
generated (Table 8.5).

Figure 8.5: Boolean rules based on literature information.

####  8.3.3 Gene expression time courses following TGF$\beta$1 and TNF$\alpha$
stimulation

Figure 8.6: Gene expression time courses following TGF$\beta$1 or TNF$\alpha$
treatment. COL1A1 (A), JUNB (B), and SMAD7 (C) gene expression in response to
TGF$\beta$1 treatment (upper row); TNF$\alpha$ response (lower row) of NFKB1
(D), MMP1 (E), and SMAD7 (F). The average time course is shown as light red
curve without symbols, the data for individual samples are depicted in other
colours (OA1: blue, filled symbol; OA2: red, filled symbol; OA3: green, filled
symbol; RA1: purple, filled symbol; RA2: blue, open symbol; RA3: yellow, open
symbol). The time courses and the values calculated from the microarray
experiments for all analysed genes are included in additional file 4.

We analysed gene expression changes of SFB from patients with RA (3 patients)
or OA (3 patients) following TGF$\beta$1 and TNF$\alpha$ stimulation (Figure
8.3). Due to the strong stimuli, both groups of cells reacted in an almost
identical way, and we did not differentiate among them. In another study, for
example, OA cells were considered to be a disease control group [112].

Following pre-processing of the microarray data gained from U133 Plus 2.0
arrays, we extracted the data for probe sets related to our genes of interest
(see Methods). The data are available in the GEO database (GSE13837 at [3]).
For the following analyses we excluded values which exceeded the reliability
threshold of $p\leq 0.05$ for any patient at any time point (0, 1, 2, 4, 6,
and 12 hours). In Figure 8.6, some selected examples for the influence of
TGF$\beta$1 and TNF$\alpha$ on gene expression are presented. The time courses
of COL1A1 and JUNB expression are shown to illustrate the TGF$\beta$1 response
in SFB, and the TNF$\alpha$ response is illustrated by NFKB1 and MMP1
expression. SMAD7 expression data are also included for both treatments. The
data and the respective diagrams for all genes and both treatments can be
found in additional file 4.

For comparative purposes, we also analysed public data from the GEO database,
first, TGF$\beta$1 treated murine embryonic fibroblasts (GSE1742) and second,
TNF$\alpha$ stimulation of endothelial cells (HeLa, GSE2624). Following
prolonged TGF$\beta$1 treatment in murine cells, COL1A2, JUN and TIMP1 gene
expression increased, whereas FOS decreased. In contrast, FOS, JUN and JUNB
expression in HeLa cells rapidly increased following TNF$\alpha$ stimulation.
Unfortunately, no data about the protease genes were available in this dataset
(additional file 5). Even though cell type, experimental design and duration
of treatment differ from our experiments, they reflect the two general trends:
a positive effect on ECM formation by TGF$\beta$1 and a degradative influence
on ECM by TNF$\alpha$ (mediated at least in part by FOS and JUN), which is
consistent with our data. However, the evaluation of the complete data sets
revealed discrepancies between the expected expression profile of individual
genes and their time courses following stimulation in the experiment.

####  8.3.4 Data discretisation

We developed a data discretisation method which appropriately captures
biologically relevant differences in gene expression levels. The individual
time profiles for each gene were separately discretised to the values 0 or 1
by $k$-means clustering [49], a method which is often applied for gene
expression time series. No improvements were observed when applying Ward’s
hierarchical clustering [100] or single linkage clustering as proposed in [32]
(data not shown). We introduced several supplementary criteria (see Methods),
e.g., the values of a time series were all discretised to the constant value 0
or 1, if the differences of all $\operatorname{log}_{2}$ values (fold-changes)
were less than 1 [72]. For the discretised data see additional file 6.

####  8.3.5 Boolean functions adapted to the data

Figure 8.7: Revised Boolean functions for the simulation of TGF$\beta$1
stimulation. Rows marked by an asterisk indicate differences of the functions
for TGF$\beta$1 and TNF$\alpha$ stimulation, changes to Table 8.5 are
italicised and bold, and function numbers in bold indicate omitted (1, 2, 3,
8, 9, 11, 12, 14) or inserted (18) terms.

Simulations were generated using an asynchronous update scheme, assuming time
intervals – approximately equal to 1 h time steps – as follows: transcription
1 (NFKB1: 2), translation: 1, RNA lifespan: 1, and protein lifespan: 2. The
Boolean functions generated the transcriptional states according to the
functional influence of proteins (stimuli or TF); translation and mRNA/protein
degradation were computed from this output state according to the predefined
intervals (see Section 8.2.4).

As starting conditions of the simulations we chose the discretised initial
states derived from our experimental data. An additional initial state was
introduced in which solely the transcription factors were set to on, which
enables the model system to respond to the external stimulators TNF$\alpha$ or
TGF$\beta$1 immediately. The simulations were performed over twelve time
steps; however, we did not aim at an exact correspondence to the experimental
observation time of twelve hours, but tried to adjust the simulated time
courses to qualitative features such as early, intermediate or late up-
regulation. Improving the Boolean functions accordingly, the initially applied
literature-based information was completed by: (i) valid and specific
experimental information; (ii) knowledge and experience of biological experts;
and (iii) in some cases, a more focused and precise literature query. For a
comparison of the discretised observed time series and the final simulations
see the additional files 6 and 7. We developed several biologically
interesting and plausible data-independent hypotheses, for example, we
modelled the regulation of SMAD3/SMAD4 effects by a protein-protein
interaction with SMAD7.

Figure 8.8: Revised Boolean functions for the simulation of TNF$\alpha$
stimulation. Rows marked by an asterisk indicate differences of the functions
for TGF$\beta$1 and TNF$\alpha$ stimulation, changes to Table 8.5 are
italicised and bold, and function numbers in bold indicate omitted (1, 2, 8,
9, 11, 12, 13, 14) or inserted (18) terms.

The resulting optimised Boolean network with the revised Boolean functions
(Tables 8.7 and 8.8) represents an enhanced ECM model, roughly matching the
given biological conditions and extensively exceeding the present
possibilities of automatic methods such as text mining, symbolic computation
or machine learning. Considering the additional information available, we
accepted these biologically reasonable changes:

  1. 1.

In the case of TNF$\alpha$ (or TGF$\beta$1) stimulation, the production and
secretion of TGF$\beta$1 (or TNF$\alpha$) by SFB should not contradict the
influence of the abundant stimulating protein TNF$\alpha$ (or TGF$\beta$1). In
these cases (e.g., for the COL1A1.out function in Table 8.8, and for the
MMP1.out function in Table 8.7) we removed TGFB1 (TNF) AND (…) from the
Boolean function term. This adjustment did not always change the simulation
result, since, for example, TNF was always off following TGF$\beta$1
stimulation (numbers of the Boolean functions (BF) affected: 1, 2, 3, 8, 9,
11, 12 and 14).

  2. 2.

Down-regulation of gene expression is an essential biological principle. For
that reason we had to introduce a time-limited inactivation mechanism which
could not be derived from the literature because information regarding down-
regulatory mechanisms is very restricted. Moreover, complex and variable
mechanisms were hard to model, e.g., JUN down-regulation which is driven by:
(i) inactivation of the TF protein itself; (ii) a general shift in the
composition of the TF AP‑1, resulting in a reduced amount of TF enhancing JUN
transcription; and (iii) binding/inactivation of JUN by other proteins.
Therefore, a time-limited mRNA inactivation was introduced for JUN, JUNB, FOS
and ETS1. Accordingly, an inactivating rule was created: if these TFs are
expressed at $t > 0$, they will be set to off at $t+3$ and afterwards (no. of
BF affected: 18). In addition, at that step we included an inhibition of
TGFB1/SMAD4 signalling-based target gene expression by integrating a
SMAD4-inhibiting signal (i.e., SMAD7, included as AND NOT SMAD7) guaranteeing
the subsequent inactivation of TGF$\beta$1-related gene expression (BF
affected: 3, 5, 6, 14 and 15). JUND is constitutively expressed at an
intermediate level, which is consistent with GEO (GSE1742 and GSE2624) and our
own data, as well as with the literature [52]. For NFKB1 transcription, an
inhibitory effect was not implemented, since the activity of NF‑$\kappa$B at
the protein level is controlled by interaction with several IKB proteins [46]
which were not included in our ECM network model.

  3. 3.

SMAD4 induction is not dependent on TGF$\beta$1 stimulation, because it is
constitutively expressed (i.e., always TRUE, BF affected: 13). However,
without TGF$\beta$1-mediated phosphorylation, SMAD4 is not activated at the
protein level and shows no transcriptional activity, even though
constitutively expressed. Therefore, we amended the term SMAD4 to TGF AND
SMAD4 in order to represent the necessity of TGF$\beta$1 for SMAD4 activation
(BF affected: 3, 5).

  4. 4.

We considered the relation ETS1 AND NFKB1 for the target genes [68] instead of
assuming alternative pathways by ETS1 OR NFKB1 because regulation by
NF‑$\kappa$B seems to be dependent on ETS1, and the MMPs, for example, require
both factors [74] (BF for TGF stimulation affected: 9, 10 and 17, Table 8.7;
BF for TNF stimulation affected: 2, 8, 9, 10 and 17, Table 8.8).

  5. 5.

Since the inhibition of JUND expression by FOS is only observed in the case of
a concomitant JUND-based positive feedback, the inhibitory effect of FOS has
been restricted to this case [23] (BF affected: 7).

  6. 6.

Since a TF should not necessarily be required for its own expression (positive
feedback), in the case of JUND (and also NFKB1) the AND connective was changed
to OR. The revision of this function prevents the absence of JUND expression
following TGF$\beta$1 stimulation (BF affected: 7, 12).

  7. 7.

Concerning the regulation of MMP1 expression by FOS, there were contradictory
findings in the literature [22], [105]. We decided for an inhibitory influence
of FOS following TGF$\beta$1 stimulation, because otherwise MMP1 would have
been permanently down-regulated by TGF$\beta$1 during the simulation (BF
affected: 8, Table 8.7).

  8. 8.

The Boolean function MMP3.out = (…) OR TGFB1 was in obvious contradiction to
the data of the present study, thus, the term OR TGFB1 was deleted. The same
was done for the MMP13 function (BF affected: 9, 11).

  9. 9.

In the case of NFKB1, the absence of TNF$\alpha$ following TGF$\beta$1
stimulation had no decisive influence (NFKB1 was not always off). For that
reason, we changed NFKB1.out = TNF AND (ETS1 OR NFKB1) to NFKB1.out = TNF OR
ETS1 OR NFKB1 (BF affected: 12, Table 8.7).

  10. 10.

However, concerning the expression of TNF itself, the necessity of a positive
feedback could explain its complete absence following TGF$\beta$1 stimulation.
On the other hand, TNF was expressed at some time points following TNF$\alpha$
stimulation, whereas it is commonly assumed that fibroblasts do not express
TNF (BF not changed: 17).

In summary, we adjusted the set of BF obtained by adaptation to the gene
expression data measured under two experimental conditions (TNF$\alpha$ and
TGF$\beta$1 stimulation), in order to create an appropriate set of BF
representing the existing knowledge about naturally occurring
interrelationships as accurately as possible.

####  8.3.6 Computing temporal rules by attribute exploration

For each stimulus, the observed and the final simulated time series were
translated and merged into a single transitive context $\mathbb{K}_{tt}$ (see
Definition 4.4.1 and the Methods Section 8.2.5). States are defined by the
value on or off for each gene, and transitions were computed by linking an
occurring input state to an arbitrary future (output) state of the simulation
or observation. The set of all these transitions, represented by
$\mathbb{K}_{tt}$, was analysed by the automatic, non-interactive version of
the attribute exploration algorithm.

The implications of the resulting stem base are temporal rules expressing
hypotheses about attributes of states (e.g., co-regulation or mutual exclusion
of gene expression) or system dynamics, which are supported by pre-existing
knowledge and by the analysed data. Since an implication holds for the
transitions between all temporally related states, a rule such as GENE1.in.out
$\rightarrow$ GENE2.out.on means: if gene1 is expressed, gene2 always will be
up-regulated in the future, at all subsequent observation time points and
simulation steps. Due to this semantics, the implications neither depend on
the correspondence of a simulation time step to a specific observation
interval, nor on prior knowledge about time periods of direct or indirect
transcriptional effects. Within the large knowledge bases for TGF$\beta$1
(2713 rules) and TNF$\alpha$ (8785 rules) stimulation, the most frequent and
simple temporal rules were considered and analysed for dependencies between
stimuli, induced TFs and their target genes.

####  8.3.7 Results of the attribute exploration

##### Stimulation with TNF$\alpha$

Regarding stimulation with TNF$\alpha$, a coordinated down-regulation of the
two TF SMAD7 (inhibitor of TGF$\beta$1/SMAD4 signalling) and ETS1 emerges, as
indicated by the rules 33, 114, 135, 144, 157, and 186 (see combTransTnf.txt
or additional file 8). For example, rule 186:

$<90>\text{COL1A1.out.off, ETS1.out.off}\rightarrow\text{SMAD7.out.off}$

has the meaning: in all simulated and observed states characterised by the
absence of COL1A1 and ETS1, SMAD7 is also off. $<90>$ stands for the support
of the rule, i.e., the number of transitions (90 out of 294) that actually
have the attributes of the premise. Rules 114, 135, 144, 157 and 186 indicate:
if the TNF$\alpha$-dependent genes are not induced (ETS1 as mediator), then
simultaneously the expression of TGF$\beta$1-dependent genes is enabled (SMAD7
is off). This suggests that TNF$\alpha$ and TGF$\beta$1 may act as antagonists
in SFB, as described in [84], [98].

The expression of NFKB1, which is also induced by TNF$\alpha$, proceeds
conversely to that of ETS1 and SMAD7 (rules 34, 45, 70, 71, 134, 144, 154, 157
and 173) reflecting the different targets of NF-$\kappa$B and SMAD7. The
antagonistic expression pattern of NFKB1 and SMAD7 appears indirectly in rule
33, where the two genes show up in the premise of a rule with high support:

$<150>(...)\>\text{NFKB1.out.on, SMAD7.out.off}\rightarrow\text{ETS1.out.off}$

Regarding this rule, it is interesting that ETS1 always acts in the same
direction as NF-$\kappa$B, according to the network derived from the
literature (Figure 8.4). In the adapted network (Table 8.8), we assumed a
necessary cooperation (i.e., an AND connective) for the positive regulation of
ETS1, MMP1, MMP3, MMP9, and TNF, as well as for the inhibition of COL1A1 and
COL1A2. Thus, rule 33 further suggests that the coordinated action of
NF-$\kappa$B and ETS1 is turned off in states which are characterised by
supplementary conditions as SMAD7.out.off.

The generated rules adequately reflect the major influence of the TF AP‑1 in
the TNF$\alpha$ system: the expression of prominent targets, such as COL1A1,
MMP1, and MMP3, depends on JUN (rules 211 and 258) and/or FOS (rule 204), with
JUN as the key player. These rules connect input and output states and thus
their semantics is directly related to dynamics, as seen in rule 211:

$<87>\text{TGFB1.in.on, TIMP1.in.on, ETS1.in.on,
JUN.in.on}\rightarrow\text{MMP1.out.on}$

making this strong statement: if ETS1 and JUN are on, MMP1 will always be up-
regulated in the future (at least within the time frame of 12 hours).

Sometimes, MMP1 is expressed simultaneously or before ETS1 and JUN. In the
simulation, MMP1 was always on in the output state and from time point 2 h in
the data. An exception can be found for the experimental results from OA
sample OA3 (Figure 8.3), where MMP1 is off after 12 h. This is the reason for
the computation of the auxiliary conditions TGFB1.in.on and TIMP1.in.on in
rule 211.

Concerning the regulation of target genes, the expression of MMP1, MMP3, and
MMP13 is co-regulated (rules 35, 63, 82, 86 and 176), while MMP9 is expressed
independently (rules 24 and 35). There is a contradiction between the
simulation and the data: in the observed experimental time series, MMP13 is
always off, whereas the Boolean network predicts an up-regulation similar to
MMP1 and MMP3. This unexpected absence of predicted MMP13 expression may be an
indication for a more complex regulation of MMP13 transcription, exceeding the
already known regulatory interrelations. Therefore, the MMP13 promoter and
further enhancer/repressor sequences should be targeted for a more pronounced
structural and functional analysis. For MMP9, the simulation and the
experimental data are in good agreement: the gene is off in most, but not all
states. However, since the expression of MMP9 by (S)FB is discussed
controversially in the literature (see [92] and [114] vs. [42]), the
calculated expression of MMP9 by fibroblasts – at least at a limited number of
time points – supports the majority of studies, reporting detectable MMP9 mRNA
amounts in (S)FB.

Several rules unanimously indicate the co-expression of the ECM-forming genes
COL1A1 and COL1A2 (rules 87, 88 and 95), but contradictory rules occur
concerning their expression profile in comparison to the MMPs. COL1A1 and
COL1A2 seem to be co-expressed with MMP1 (rules 90 and 176), for COL1A2,
however, a certain co-expression with MMP9 is calculated as well (rules 76 and
77), which conflicts with the opposing expression of MMP1 and MMP9 (see
above). Therefore, the expression of collagens does often, but not necessarily
always correlate with the expression of MMPs. This reflects the imbalance
between MMP-dependent destruction and collagen-driven regeneration/fibrosis of
ECM in the joints in inflammatory RA.

The calculated knowledge base also contains a further unexpected correlation.
According to rule 166:

$\displaystyle<94>\quad\>$ FOS.in.off, TIMP1.in.on, SMAD7.out.off
$\displaystyle\quad\rightarrow\>$ TGFB1.in.on, MMP1.out.on, TGFB1.out.on

and rule 188, the expression of MMP1 may also be induced in the absence of FOS
(e.g., by JUN-containing AP-1 complexes), indicating that the regulation of
MMP1 does not predominantly depend on FOS as proposed in the literature [104],
[94]. This result may point to the influence of other TFs, e.g., NF-$\kappa$B,
ETS1, or AP-1 complexes containing JUN, which may indeed be able to induce
target gene expression in the absence of FOS.

##### Stimulation with TGF$\beta$1

For the stimulation with TGF$\beta$1, we had a total number of 341
transitions. The SMADs play a major role for the expression of
TGF$\beta$1-dependent target genes, as reflected by various classes of rules
containing SMAD4 and/or SMAD7 (see combTransTgf.txt or additional file 8). For
example, SMAD4 can be involved in the expression of COL1A1, see rule 15 (and
also rules 21, 26 and 30):

$<239>\text{ETS1.out.off}\rightarrow\text{SMAD4.in.on, COL1A1.out.on,
SMAD4.out.on}$

This also suggests an antagonistic behaviour of ETS1 and SMAD4: if ETS1 was
off, then SMAD4 was on, as well as in all previous states. Rules 52 and 57
suggest a dependency of MMP1 on SMAD4. However, this seems to be one amongst
many other influences (or could be a non-influencing coincidence), since SMAD4
was permanently on during simulation and experimental stimulation with
TGF$\beta$1 (exception: sample RA3 at time point 2h).

The expression of MMP9 is neither induced by SMAD4 (rules 7, 24 and 41) nor by
any other TF, indicating that MMP9 is not influenced by TGF$\beta$1\. The fact
that TGF$\beta$1 obviously does not induce MMP9 (but other MMPs) agrees with
findings reported previously [42] and represents a clear contrast to the MMP
expression profiles following TNF$\alpha$ stimulation.

A further case of an antagonistic expression pattern was calculated for MMPs
and COL1A1 (rules 21, 30, 36, 41, 54, and 60), for example, in rule 54:

$\displaystyle<170>\quad\>$ SMAD4.in.on, MMP3.out.off, MMP9.out.off,
MMP13.out.off, (…) $\displaystyle\quad\rightarrow\>$ COL1A1.out.on

Antagonistic expression profiles also can be observed for SMAD4 and other TFs,
e.g., JUN and JUNB (rules 12, 39) or ETS1 (rule 15, see above). The variety of
TF combinations found, even following the same stimulus, exceeds the
possibilities of conventional TF studies because stimulation experiments are
generally restricted to a selected set of read-out parameters (e.g., the
expression of single TFs or target genes) which are not able to reflect the
multiplicity of different effects in the cell.

Following stimulation with TGF$\beta$1, interestingly COL1A2 appears to be
constitutively expressed since its status is always calculated as on (rule 1).
Therefore, for the formation of collagen I, which contains COL1A1 and COL1A2
chains, COL1A1 expression seems to be the critical switch.

##### TGF$\beta$1 versus TNF$\alpha$ effects

The calculated results impressively illustrate that TGF$\beta$1 and
TNF$\alpha$ stimulation are mediated via separate signal transduction
pathways, leading to the expression and activation of different TFs. In
general, ETS1 and NFKB1 are induced predominantly by TNF$\alpha$, whereas SMAD
expression depends on TGF$\beta$1 (represented by differential expression
profiles of ETS1 and SMAD4). JUN and FOS, however, strikingly respond to both
stimuli. This defined pattern results in the expression of target genes with
opposing roles. TGF$\beta$1 positively regulates the enhanced formation of ECM
components, whereas TNF$\alpha$ is strongly involved in the expression of ECM-
degrading enzymes. This was the main reason for a discriminative revision of
the BF for TNF$\alpha$ and TGF$\beta$1 (Tables 8.7 and 8.8). Six BF were found
to be differently adjusted (BF 1, 2, 3, 8, 12 and 14) which concern either the
key players for ECM destruction (MMP1; BF 8), ECM formation (COL1A1 and
COL1A2; BF 1 and 2) or important regulatory genes (ETS1, NFKB1, SMAD7). This
may indicate that the differential effects on ECM induced by TNF$\alpha$ or
TGF$\beta$1 are mainly mediated via ETS1 (BF 3), NFKB1 (BF 12, especially in
the TNF$\alpha$ pathway), or SMAD7 (BF 14, especially in the TGF$\beta$1
pathway) identifying ETS1- and NFKB1-associated pathways as the major
TNF$\alpha$-induced pro-inflammatory/pro-destructive signalling modules in
rheumatic diseases, whereas TGF$\beta$1-driven and SMAD7-related signalling
appears prominently involved in fibrosis.

####  8.3.8 Querying the knowledge base

The minimal rule set gave many new insights, and further queries can be
addressed by accessing the TNF$\alpha$ and TGF$\beta$1 knowledge bases in one
of two ways: (i) the Excel file containing the transition rules for structured
searches within the rule sets (see additional file 8 containing the top 500
transition rules, impCombTransTgf.txt and impCombTransTnf.txt for complete
lists); and (ii) the stem base in PROLOG format for queries concerning
logically implied rules as in Section 7.4 for the B. subtilis simulations
(impCombTransTgf.P and impCombTransTnf.P).

####  8.3.9 Expert centered attribute exploration

Resuming the presented study published in [109], I investigated in detail four
genes showing strong changes over the time steps of the simulation modelling
TGF$\beta$1 stimulation, by interactive attribute exploration:

  1. 1.

MMP13 is up- and downregulated at one or two time points during the
simulation, but it was never expressed significantly in the microarry
experiments. A human expert can partly solve this contradiction and decide for
each relative implication to which of the two knowledge sources more
plausibility is attributed.

  2. 2.

I was also interested in the interplay of three TF belonging to different
pathways, but connected in the Boolean formula for JUNB (BF 6 of Table 8.7):

JUNB.out = (TGFB1 $\wedge$ NFKB1 $\wedge$ SMAD4 $\wedge\>\neg$SMAD7) $\vee$
(TNF $\wedge$ NFKB1)

JUNB represents the AP1 complex playing an important role in the investigated
biological context.

  3. 3.

NFKB1 is known to activate MMP13.

  4. 4.

Whereas JUNB and NFKB1 generally belong to TNF$\alpha$ pathways, SMAD7
inhibits TGF$\beta$1 signaling via SMAD4. The inhibition of SMAD7 expression
by TNF$\alpha$ connects both pathways.

During attribute exploration of the simulated transitive context, the
following implications were accepted, or an observed transition was introduced
as counterexample, which differed little from a simulated transition.
Counterexamples are indicated as binary numbers designating the values of the
attributes JUNB.in, MMP13.in, NFKB1.in, SMAD7.in, JUNB.out, MMP13.out,
NFKB1.out and SMAD7.out. Important decision criteria were support (number of
transitions with the premise attributes / 72 overall transitions) and
confidence (transitions with conclusion attributes / premise transitions) of
the implication in the observed transitive context. For this purpose, the R
script selectGenes2.1.r was used. In the protocol of the exploration, I omit
background implications expressing dichotomic scaling like “gene.in.on,
gene.in.out $\rightarrow\bot$”. The resulting context is
exploredTransTgf_regulationMMP13.txt, the complete stem base is documented at
exploredTransTgf_regulationMMP13_inf.txt.

  1. 1.

SMAD7.out.off $\rightarrow$ JUNB.out.off, MMP13.out.off, NFKB1.out.on.
The implication was rejected by reason of a week confidence 13/30. The
counterexample 1001 0000 was introduced, i.e. a transition where JUNB.in and
SMAD7.in are on and the other attributes off.

  2. 2.

SMAD7.out.off $\rightarrow$ JUNB.out.off, MMP13.out.off.
Accepted with support 30/72 and confidence 23/30.

  3. 3.

MMP13.out.on $\rightarrow$ SMAD7.out.on.
The implication was accepted, since there is no information in the observed
context: MMP13 is always off, hence the support is 0.

  4. 4.

JUNB.out.on $\rightarrow$ SMAD7.out.on.
Accepted with confidence 29/36. The implication is biologically interesting:
If TNF$\alpha$ signaling via JUNB is enabled, TGF$\beta$1 signaling is
inhibited via SMAD7 – in spite of its reported inhibition, in turn, by
TNF$\alpha$ (BF 14 of Table 8.5). However, TNF$\alpha$ was supposed to have a
minor influence compared to the stimulus TGF$\beta$1 (BF 14 of Table 8.7),
which points at more complex regulations.

  5. 5.

JUNB.out.on, SMAD7.out.on, NFKB1.out.off $\rightarrow$ NFKB1.in.on,
JUNB.in.off, MMP13.in.off, SMAD7.in.off.
Despite a confidence 0/4, the complicated, little expressive implication has
been accepted. The latter fact is reflected in the small support of 4/72.

  6. 6.

JUNB.out.off, MMP13.out.off, NFKB1.out.off, SMAD7.out.off $\rightarrow$