# Formalism-Driven Development: Concepts, Taxonomy, and Practice +
## 2 Preliminaries
### Basic Structures  
Firstly, let us recall the Kripke structure, which is one of the commonly used models for formal specification. **Definition 1** (Kripke structure). : _Let \(P\) be a set of atomic propositions. A Kripke structure \(\mathfrak{K}\) is a quintuple_  
\[\mathfrak{K}\triangleq\langle S,R,I,P,\mathcal{L}\rangle\]  
_where_  
* \(S\) _is a set of states,_
* \(R\subseteq S\times S\) _is a transition relation;_
* \(I\subseteq S\) _is a set of initial states;_
* \(P\) _is a set of atomic propositions; and_
* \(\mathcal{L}:S\mapsto\wp(P)\) _is a labeling function._  
_Relation \(R\) is left-total, i.e., \(\forall s\in S(\exists s^{\prime}\in S:(s,s^{\prime})\in R)\). An atomic proposition is an indecomposable proposition defined in propositional logic. The labeling function \(\mathcal{L}\) relates a set \(\mathcal{L}(s)\in\wp(P)\) of atomic propositions to any state \(s\)._  
Notably, a Kripke structure is an unlabeled transition system. Therefore, it is preferred in state-based approaches for formal specification. For action-based approaches that assume only the executed actions are observable from outside, a labeled transition system plays a pivotal role. In this paper, we define a variant of labeled transition system as below. **Definition 2** (Labeled Transition System). : _A labeled transition system \(\mathfrak{T}\) over set Var of typed state variables is a tuple_  
\[\mathfrak{T}\triangleq\langle S,A,\rightarrow,I,P,\mathcal{L}\rangle\]  
_where_  
* \(S=[\text{Var}]\) _is a set of states;_
* \(A\) _is a set of actions;_* \(\rightarrow\subseteq S\times A\times S\) _is a transition relation;_
* \(I\subseteq S\) _is a set of initial states;_
* \(P\) _is a set of atomic propositions; and_
* \(\mathcal{L}:S\mapsto\wp(P)\) _is a labeling function._  
_The state space_ \(S\) _is determined by_ \([\text{Var}]\)_, which is the set of evaluations of state variables_ _Var. State_ \(s\in S\) _is called a terminal state if it does not have any outgoing transitions, i.e.,_ \(\bigcup\limits_{a\in A}\{s^{\prime}\in S\mid s\xrightarrow{a}s^{\prime}\}=\emptyset\)_. The notation_ \(s\xrightarrow{a}s^{\prime}\) _is used as shorthand for_ \((s,a,s^{\prime})\in\rightarrow\)_. In this paper, we assume that_ \(S\)_,_ \(A\)_, and_ \(P\) _are finite sets._  
In fact, a labeled transition system can be transformed into a Kripke structure and vice versa [20; 21]. In this manner, we can formalize a system from either a state-based view or an action-based view according to concrete contexts. In the remainder of this paper, we abbreviate _labeled transition system_ to _transition system_. Conditional branching is commonly used in modeling systems. By using conditional branching, it is possible to put constraints on actions. An action can only be triggered while the current evaluation of variables satisfies some conditions. We denote a set of Boolean conditions (propositional formulae) over _Var_ as \(\|\text{Var}\|\). In the interest of modeling conditional branching, we introduce conditional transitions. **Definition 3** (Conditional Transition). : _A transition system \(\mathfrak{T}\) with conditional transitions over set Var of typed state variables is a tuple_  
\[\mathfrak{T}\triangleq\langle S,A,\hookrightarrow,I,g_{0},P,\mathcal{L}\rangle\]  
_according to Definition 2 with differences that_  
* \(\hookrightarrow\subseteq S\times\|\text{Var}\|\times A\times S\) _is the conditional transition relation; and_
* \(g_{0}\in\|\text{Var}\|\) _is the initial guard (condition)._  
_For convenience, we use the notation_ \(s\stackrel{{ g\downarrow a}}{{\longrightarrow}}s^{\prime}\) _as shorthand for_ \((s,g,a,s^{\prime})\in\hookrightarrow\)_. If the guard is a tautology, we can omit it, i.e.,_ \(s\stackrel{{ a}}{{\hookrightarrow}}s^{\prime}\)_._  
_The behavior in state_ \(s\in S\) _depends on the current state variable evaluation_ \(\mathcal{V}\in[\text{Var}]\)_. The value of state variable_ \(x\in\text{Var}\) _is accessible through_ \(\mathcal{V}(x)\)_.