Variability Abstraction and Refinement for GameBased Lifted Model Checking of Full CTL
Abstract
Variability models allow effective building of many custom model variants for various configurations. Lifted model checking for a variability model is capable of verifying all its variants simultaneously in a single run by exploiting the similarities between the variants. The computational cost of lifted model checking still greatly depends on the number of variants (the size of configuration space), which is often huge. One of the most promising approaches to fighting the configuration space explosion problem in lifted model checking are variability abstractions. In this work, we define a novel gamebased approach for variabilityspecific abstraction and refinement for lifted model checking of the full CTL, interpreted over 3valued semantics. We propose a direct algorithm for solving a 3valued (abstract) lifted model checking game. In case the result of model checking an abstract variability model is indefinite, we suggest a new notion of refinement, which eliminates indefinite results. This provides an iterative incremental variabilityspecific abstraction and refinement framework, where refinement is applied only where indefinite results exist and definite results from previous iterations are reused.
1 Introduction
Software Product Line (SPL) [6] is an efficient method for systematic development of a family of related models, known as variants (valid products), from a common code base. Each variant is specified in terms of features (static configuration options) selected for that particular variant. SPLs are particularly popular in the embedded and critical system domains (e.g. cars, phones, avionics, healthcare).
Lifted model checking [4, 5] is a useful approach for verifying properties of variability models (SPLs). Given a variability model and a specification, the lifted model checking algorithm, unlike the standard nonlifted one, returns precise conclusive results for all individual variants, that is, for each variant it reports whether it satisfies or violates the specification. The main disadvantage of lifted model checking is the configuration space explosion problem, which refers to the high number of variants in the variability model. In fact, exponentially many variants can be derived from only few configuration options (features). One of the most successful approaches to fighting the configuration space explosion are socalled variability abstractions [12, 14, 15, 17]. They hide some of the configuration details, so that many of the concrete configurations become indistinguishable and can be collapsed into a single abstract configuration (variant). This results in smaller abstract variability models with a smaller number of abstract configurations. In order to be conservative w.r.t. the full CTL temporal logic, abstract variability models have two types of transitions: maytransitions which represent possible transitions in the concrete model, and musttransitions which represent the definite transitions in the concrete model. May and must transitions correspond to over and under approximations, and are needed in order to preserve universal and existential CTL properties, respectively.
Here we consider the 3valued semantics for interpreting CTL formulae over abstract variability models. This semantics evaluates a formula on an abstract model to either true, false, or indefinite. Abstract variability models are designed to be conservative for both true and false. However, the indefinite answer gives no information on the value of the formula on the concrete model. In this case, a refinement is needed in order to make the abstract models more precise.
The technique proposed here significantly extends the scope of existing automatic variabilityspecific abstraction refinement procedures [8, 18], which currently support the verification of universal LTL properties only. They use conservative variability abstractions to construct overapproximated abstract variability models, which preserve LTL properties. If a spurious counterexample (introduced due to the abstraction) is found in the abstract model, the procedures [8, 18] use Craig interpolation to extract relevant information from it in order to define the refinement of abstract models. Variability abstractions that preserve all (universal and existential) CTL properties have been previously introduced [12], but without an automatic mechanism for constructing them and no notion of refinement. The abstractions [12] has to be constructed manually by an engineer before verification. In order to make the entire verification procedure automatic, we need to develop an abstraction and refinement framework for CTL properties.
In this work, we propose the first variabilityspecific abstraction refinement procedure for automatically verifying arbitrary formulae of CTL. To achieve this aim, model checking games [24, 25, 26] represent the most suitable framework for defining the refinement. In this way, we establish a brand new connection between games and familybased (SPL) model checking. The refinement is defined by finding the reason for the indefinite result of an algorithm that solves the corresponding model checking game, which is played by two players: Player\(\, \forall \) (trying to refute the formula \(\varPhi \) on an abstract model \(\mathcal {M}\)) and Player\(\, \exists \) (trying to verify \(\varPhi \) on \(\mathcal {M}\)). The game is played on a game board, which consists of configurations of the form \((s,\varPhi ')\) where s is a state of the abstract model \(\mathcal {M}\) and \(\varPhi '\) is a subformula of \(\varPhi \), such that the value of \(\varPhi '\) in s is relevant for determining the final model checking result. The players make moves between configurations in which they try to verify or refute \(\varPhi '\) in s. All possible plays of a game are captured in the gamegraph, whose nodes are the elements of the game board and whose edges are the possible moves of the players. The model checking game is solved via a coloring algorithm which colors each node \((s,\varPhi ')\) in the gamegraph by T, F, or ? iff the value of \(\varPhi '\) in s is true, false, or indefinite, respectively. Player\(\, \forall \) has a winning strategy at the node \((s,\varPhi ')\) iff the node is colored by F iff \(\varPhi '\) does not hold in s, and Player\(\, \exists \) has a winning strategy at \((s,\varPhi ')\) iff the node is colored by T iff \(\varPhi '\) holds in s. In addition, it is also possible that neither of players has a winning strategy, in which case the node is colored by ? and the value of \(\varPhi '\) in s is indefinite. In this case, we want to refine the abstract model. We can find the reason for the tie by examining the gamegraph. We choose a refinement criterion, which splits abstract configurations so that the new, refined abstract configurations represent smaller subsets of concrete configurations.
2 Background
Variability Models. Let Open image in new window be a finite set of Boolean variables representing the features available in a variability model. A specific subset of features, Open image in new window , known as configuration, specifies a variant (valid product) of a variability model. We assume that only a subset Open image in new window of configurations are valid. An alternative representation of configurations is based upon propositional formulae. Each configuration \(k \in \mathbb {K}\) can be represented by a formula: \(k(A_1) \wedge \ldots \wedge k(A_n)\), where \(k(A_i) = A_i\) if \(A_i \in k\), and \(k(A_i) = \lnot A_i\) if \(A_i \notin k\) for \(1 \le i \le n\).
We use transition systems (TS) to describe behaviors of singlesystems.
Definition 1
A transition system (TS) is a tuple \(\mathcal {T}=(S,Act,trans,I,AP,L)\), where S is a set of states; Act is a set of actions; \(trans \subseteq S \times Act \times S\) is a transition relation which is total, so that for each state there is an outgoing transition; \(I \subseteq S\) is a set of initial states; AP is a set of atomic propositions; and \(L : S \rightarrow 2^{AP}\) is a labelling function specifying which propositions hold in a state. We write Open image in new window whenever \((s_1,\lambda ,s_2) \in \textit{trans} \).
An execution (behaviour) of a TS \(\mathcal {T}\) is an infinite sequence \(\rho = s_0 \lambda _1 s_1 \lambda _2 \ldots \) with \(s_0 \in I\) such that \(s_i {\mathop {\longrightarrow }\limits ^{\lambda _{i+1}}} s_{i+1}\) for all \(i \ge 0\). The semantics of the TS \(\mathcal {T}\), denoted as \([\! [\mathcal {T} ]\! ]_{TS}\), is the set of its executions.
A featured transition system (FTS) is a particular instance of a variability model, which describes the behavior of a whole family of systems in a single monolithic description, where the transitions are guarded by a presence condition that identifies the variants they belong to. The presence conditions \(\psi \) are drawn from the set of feature expressions, Open image in new window , which are propositional logic formulae over Open image in new window : Open image in new window . We write \([\! [\psi ]\! ]\) to denote the set of configurations from \(\mathbb {K}\) that satisfy \(\psi \), i.e. \(k \in [\! [\psi ]\! ]\) iff \(k \models \psi \).
Definition 2
A featured transition system (FTS) represents a tuple Open image in new window , where S, Act, trans, I, AP, and L form a TS; Open image in new window is the set of available features; \(\mathbb {K}\) is a set of valid configurations; and Open image in new window is a total function decorating transitions with presence conditions.
The projection of an FTS \(\mathcal {F}\) to a configuration \(k \in \mathbb {K}\), denoted as \(\pi _k(\mathcal {F})\), is the TS \((S,Act,trans',I,AP,L)\), where \(trans'=\{ t \in trans \mid k \models \delta (t) \}\). We lift the definition of projection to sets of configurations \(\mathbb {K}' \!\subseteq \! \mathbb {K}\), denoted as \(\pi _{\mathbb {K}'}(\mathcal {F})\), by keeping the transitions admitted by at least one of the configurations in \(\mathbb {K}'\). That is, \(\pi _{\mathbb {K}'}(\mathcal {F})\), is the FTS Open image in new window , where \(trans'=\{ t \in trans \mid \exists k \in \mathbb {K}'. k \models \delta (t) \}\) and \(\delta ' = \left. \delta \right _{trans'}\) is the restriction of \(\delta \) to \(trans'\). The semantics of an FTS \(\mathcal {F}\), denoted as \([\! [\mathcal {F} ]\! ]_{FTS}\), is the union of behaviours of the projections on all valid variants \(k \in \mathbb {K}\), i.e. \([\! [\mathcal {F} ]\! ]_{FTS} = \cup _{k \in \mathbb {K}} [\! [\pi _k(\mathcal {F}) ]\! ]_{TS}\).
Modal transition systems (MTSs) [22] are a generalization of transition systems equipped with two transition relations: must and may. The former (must) is used to specify the required behavior, while the latter (may) to specify the allowed behavior of a system. We will use MTSs for representing abstractions of FTSs.
Definition 3
A modal transition system (MTS) is represented by a tuple \(\mathcal {M}=(S,Act,trans^{\text {may}},trans^{\text {must}},I,AP,L)\), where \(trans^{\text {may}} \subseteq S \times Act \times S\) describe may transitions of \(\mathcal {M}\); \(trans^{\text {must}} \subseteq S \times Act \times S\) describe must transitions of \(\mathcal {M}\), such that \(trans^{\text {may}}\) is total and \(trans^{\text {must}} \subseteq trans^{\text {may}}\).
A mayexecution in \(\mathcal {M}\) is an execution (infinite sequence) with all its transitions in \(trans^{\text {may}}\); whereas a mustexecution in \(\mathcal {M}\) is a maximal sequence with all its transitions in \(trans^{\text {must}}\), which cannot be extended with any other transition from \(trans^{\text {must}}\). Note that since \(trans^{\text {must}}\) is not necessarily total, mustexecutions can be finite. We use \([\! [\mathcal {M} ]\! ]_{MTS}^{\text {may}}\) (resp., \([\! [\mathcal {M} ]\! ]_{MTS}^{\text {must}}\)) to denote the set of all mayexecutions (resp., mustexecutions) in \(\mathcal {M}\) starting in an initial state.
Example 1
Throughout this paper, we will use a beverage vending machine as a running example [4]. Figure 1 shows the FTS of a VendMach family. It has two features, and each of them is assigned an identifying letter and a color. The features are: CancelPurchase ( Open image in new window ), for canceling a purchase after a coin is entered; and FreeDrinks ( Open image in new window ) for offering free drinks. Each transition is labeled by an action followed by a feature expression. For instance, the transition Open image in new window is included in variants where the feature Open image in new window is enabled. For clarity, we omit to write the presence condition true in transitions. There is only one atomic proposition \(\texttt {served} \in AP\), which is abbreviated as \(\textit{r}\). Note that \(\textit{r} \in L(s_2)\), whereas \(\textit{r} \not \in L(s_0)\) and \(\textit{r} \not \in L(s_1)\).
By combining various features, a number of variants of this VendMach can be obtained. The set of valid configurations is:
Open image in new window (or, equivalently Open image in new window ). Figure 2 shows a basic version of VendMach that only serves a drink, described by the configuration: \(\emptyset \) (or, as formula Open image in new window ). It takes a coin, serves a drink, opens a compartment so the customer can take the drink. Figure 3 shows an MTS, where must transitions are denoted by solid lines, while may transitions by dashed lines. \(\square \)
We assume the standard CTL semantics over TSs is given [1] (see also [16, Appendix A]). We write \([\mathcal {T}\models \varPhi ]=\textit{tt}\) to denote that \(\mathcal {T}\) satisfies the formula \(\varPhi \), whereas \([\mathcal {T}\models \varPhi ]=\textit{ff}\) to denote that \(\mathcal {T}\) does not satisfy \(\varPhi \).
We say that an FTS \(\mathcal {F}\) satisfies a CTL formula \(\varPhi \), written \([\mathcal {F}\models \varPhi ]=\textit{tt}\), iff all its valid variants satisfy the formula, i.e. \( \forall k\!\in \!\mathbb {K}. \, [\pi _k(\mathcal {F}) \models \varPhi ]=\textit{tt}\). Otherwise, we say \(\mathcal {F}\) does not satisfy \(\varPhi \), written \([\mathcal {F}\models \varPhi ]=\textit{ff}\). In this case, we also want to determine a nonempty set of violating variants \(\mathbb {K}' \subseteq \mathbb {K}\), such that \(\forall k'\!\in \!\mathbb {K}'. \,[\pi _{k'}(\mathcal {F}) \models \varPhi ]=\textit{ff}\) and \(\forall k\!\in \!\mathbb {K}\backslash \mathbb {K}'. \,[\pi _k(\mathcal {F}) \models \varPhi ]=\textit{tt}\).
 (1)
\([s \models ^3 a] = \left. {\left\{ \begin{array}{ll} \textit{tt}, &{} \text {if } a \in L(s) \\ \textit{ff}, &{} \text {if } a \not \in L(s) \end{array}\right. }\right. \), \([s \models ^3 \lnot a] = \left. {\left\{ \begin{array}{ll} \textit{tt}, &{} \text {if } a \not \in L(s) \\ \textit{ff}, &{} \text {if } a \in L(s) \end{array}\right. }\right. \)
 (2)
\([s \models ^3 \varPhi _1 \wedge \varPhi _2] = \left. {\left\{ \begin{array}{ll} \textit{tt}, &{} \text {if } [s \models ^3 \varPhi _1]=\textit{tt}\text { and } [s \models ^3 \varPhi _2]=\textit{tt}\\ \textit{ff}, &{} \text {if } [s \models ^3 \varPhi _1]=\textit{ff}\text { or } [s \models ^3 \varPhi _2]=\textit{ff}\\ \bot , &{} \text {otherwise} \end{array}\right. }\right. \)
 (3)
\([s \models ^3 A \phi ] = \left. {\left\{ \begin{array}{ll} \textit{tt}, &{} \text {if } \forall \rho \in [\! [\mathcal {M} ]\! ]^{\text {may},s}_{MTS}. \, [\rho \models ^3 \phi ] = \textit{tt}\\ \textit{ff}, &{} \text {if } \exists \rho \in [\! [\mathcal {M} ]\! ]^{\text {must},s}_{MTS}. \, [\rho \models ^3 \phi ] = \textit{ff}\\ \bot , &{} \text {otherwise} \end{array}\right. }\right. \) \([s \models ^3 E \phi ] = \left. {\left\{ \begin{array}{ll} tt, &{} \text {if } \exists \rho \in [\! [\mathcal {M} ]\! ]^{\text {must},s}_{MTS}. \, [\rho \models ^3 \phi ] = \textit{tt}\\ \textit{ff}, &{} \text {if } \forall \rho \in [\! [\mathcal {M} ]\! ]^{\text {may},s}_{MTS}. \, [\rho \models ^3 \phi ] = \textit{ff}\\ \bot , &{} \text {otherwise} \end{array}\right. }\right. \)
 (4)
\([\rho \models ^3 \! (\varPhi _1 \textsf {U}\varPhi _2)] \!=\! \left. {\left\{ \begin{array}{ll} \textit{tt}, &{} \!\!\text {if } \exists 0 \!\le \! i \!\le \! \rho . \big ( [\rho _i \!\models ^3 \! \varPhi _2]\!=\!\textit{tt}\wedge (\forall j \!<\! i. [\rho _j \!\models ^3 \varPhi _1]\!=\!\textit{tt}) \big ) \\ \textit{ff}, &{} \!\!\text {if } \begin{array}{@{} l @{}} \forall 0 \!\le \! i \!\le \! \rho . \big ( \forall j \!<\! i. [\rho _j \!\models ^3 \! \varPhi _1] \!\ne \! \textit{ff}\!\!\implies \!\! [\rho _i \! \models ^3 \! \varPhi _2]\!=\!\textit{ff}\big ) \\ \wedge \ \forall i \!\ge \! 0. [\rho _i \!\models ^3 \! \varPhi _1] \!\ne \! \textit{ff}\!\implies \!\! \rho =\infty \end{array} \\ \bot , &{} \!\!\text {otherwise} \end{array}\right. }\right. \)
A MTS \(\mathcal {M}\) satisfies a formula \(\varPhi \), written \([\mathcal {M}\models ^3 \varPhi ]=\textit{tt}\), iff \(\forall s_0 \in I. \, [s_0 \models ^3 \varPhi ]=\textit{tt}\). We say that \([\mathcal {M}\models ^3 \varPhi ]=\textit{ff}\) if \(\exists s_0 \in I. \, [s_0 \models ^3 \varPhi ]=\textit{ff}\). Otherwise, \([\mathcal {M}\models ^3 \varPhi ]=\bot \).
Example 2
Consider the FTS VendMach and MTS \(\varvec{\alpha }^{ \text {join} }(\textsc {VendMach})\) in Figs. 1 and 3. The property \(\varPhi _1=A (\lnot \textit{r} \textsf {U}\textit{r})\) states that in the initial state along every execution will eventually reach the state where \(\textit{r}\) holds. Note that \([\textsc {VendMach}\models \varPhi _1]=\textit{ff}\). E.g., if the feature Open image in new window is enabled, a counterexample where the state \(s_2\) that satisfies r is never reached is: \(s_0 \rightarrow s_1 \rightarrow s_0 \rightarrow \ldots \). The set of violating products is Open image in new window .However, Open image in new window . We also have that \([\varvec{\alpha }^{ \text {join} }(\textsc {VendMach}) \models ^3 \varPhi _1]=\bot \), since (1) there is a mayexecution in \(\varvec{\alpha }^{ \text {join} }(\textsc {VendMach})\) where \(s_2\) is never reached: \(s_0 \rightarrow s_1 \rightarrow s_0 \rightarrow \ldots \), and (2) there is no mustexecution that violates \(\varPhi _1\).
Consider the property \(\varPhi _2=E (\lnot \textit{r} \textsf {U}\textit{r})\), which describes a situation where in the initial state there exists an execution that will eventually reach \(s_2\) that satisfies r. Note that \([\textsc {VendMach}\models \varPhi _2]=\textit{tt}\), since even for variants with the feature Open image in new window there is a continuation from the state \(s_1\) to \(s_2\). But, \([\varvec{\alpha }^{ \text {join} }(\textsc {VendMach}) \models \varPhi _2] = \bot \) since (1) there is no a mustexecution in \(\varvec{\alpha }^{ \text {join} }(\textsc {VendMach})\) that reaches \(s_2\) from \(s_0\), and (2) there is a mayexecution that satisfies \(\varPhi _2\). \(\square \)
3 Abstraction of FTSs
We now introduce the variability abstractions [12] which preserve full CTL. We start working with Galois connections^{2} between Boolean complete lattices of feature expressions, and then induce a notion of abstraction of FTSs.
The Boolean complete lattice of feature expressions (propositional formulae over \(\mathbb {F}\)) is: \((\textit{FeatExp}(\mathbb {F})_{/\equiv },\models ,\vee ,\wedge ,\textit{true},\textit{false},\lnot )\). The elements of the domain \(\textit{FeatExp}(\mathbb {F})_{/\equiv }\) are equivalence classes of propositional formulae \(\psi \!\in \! \textit{FeatExp}(\mathbb {F})\) obtained by quotienting by the semantic equivalence \(\equiv \). The ordering \(\models \) is the standard entailment between propositional logics formulae, whereas the least upper bound and the greatest lower bound are just logical disjunction and conjunction respectively. Finally, the constant false is the least, true is the greatest element, and negation is the complement operator.
Abstract MTS and Preservation of CTL. Given a Galois connection \((\varvec{\alpha }^{ \text {join} },\varvec{\gamma }^{ \text {join} })\) defined on the level of feature expressions, we now define the abstraction of an FTS as an MTS with two transition relations: one (may) preserving universal properties, and the other (must) preserving existential properties. The may transitions describe the behaviour that is possible in some variant of the concrete FTS, but not need be realized in the other variants; whereas the must transitions describe behaviour that has to be present in all variants of the FTS.
Definition 4
Given the FTS \(\mathcal {F}=(S,Act,trans,I,AP,L,\mathbb {F},\mathbb {K},\delta )\), define MTS \(\varvec{\alpha }^{ \text {join} }(\mathcal {F})=(S,Act,trans^{\text {may}},trans^{\text {must}},I,AP,L)\) to be its abstraction, where \(trans^{\text {may}} \!=\! \{ t \!\in \! trans \mid \varvec{\alpha }^{ \text {join} }(\delta (t)) \!=\! \textit{true}\}\), and \(trans^{\text {must}} \!=\! \{ t \!\in \! trans \mid \widetilde{\varvec{\alpha }^{ \text {join} }}(\delta (t)) \!=\! \textit{true}\}\).
Note that the abstract model \(\varvec{\alpha }^{ \text {join} }(\mathcal {F})\) has no variability in it, i.e. it contains only one abstract configuration. We now show that the 3valued semantics of the MTS \(\varvec{\alpha }^{ \text {join} }(\mathcal {F})\) is designed to be sound in the sense that it preserves both satisfaction (\(\textit{tt}\)) and refutation (\(\textit{ff}\)) of a formula from the abstract model to the concrete one. However, if the truth value of a formula in the abstract model is \(\bot \), then its value over the concrete model is not known. We prove [16, Appendix B]:
Theorem 1

(1) \([\varvec{\alpha }^{ \text {join} }(\mathcal {F}) \models ^3 \varPhi ]\!=\!\textit{tt}\, \implies \, [\mathcal {F}\models \varPhi ]\!=\!\textit{tt}\).

(2) \([\varvec{\alpha }^{ \text {join} }(\mathcal {F}) \models ^3 \varPhi ]\!=\!\textit{ff}\, \implies \, [\mathcal {F}\models \varPhi ]\!=\!\textit{ff}\) and \([\pi _k(\mathcal {F}) \models \varPhi ]\!=\!\textit{ff}\) for all \(k \in \mathbb {K}\).
Divideandconquer strategy. The problem of evaluating \([\mathcal {F}\models \varPhi ]\) can be reduced to a number of smaller problems by partitioning the configuration space \(\mathbb {K}\). Let the subsets \(\mathbb {K}_1, \mathbb {K}_2, \ldots , \mathbb {K}_n\) form a partition of the set \(\mathbb {K}\). Then, \([\mathcal {F}\models \varPhi ]=\textit{tt}\) iff \([\pi _{\mathbb {K}_i}(\mathcal {F}) \models \varPhi ]=\textit{tt}\) for all \(i=1,\ldots ,n\). Also, \([\mathcal {F}\models \varPhi ]=\textit{ff}\) iff \([\pi _{\mathbb {K}_j}(\mathcal {F}) \models \varPhi ]=\textit{ff}\) for some \(1 \le j \le n\). By using Theorem 1, we obtain the following result.
Corollary 1
Let \(\mathbb {K}_1, \mathbb {K}_2, \ldots , \mathbb {K}_n\) form a partition of \(\mathbb {K}\).

(1) If \([\varvec{\alpha }^{ \text {join} }(\pi _{\mathbb {K}_1}(\mathcal {F})) \models \varPhi ]\!=\!\textit{tt}\, \wedge \ldots \wedge \, [\varvec{\alpha }^{ \text {join} }(\pi _{\mathbb {K}_n}(\mathcal {F})) \models \varPhi ]\!=\!\textit{tt}\), then \([\mathcal {F}\models \varPhi ]\!=\!\textit{tt}\).

(2) If \([\varvec{\alpha }^{ \text {join} }(\pi _{\mathbb {K}_j}(\mathcal {F})) \models \varPhi ]\!=\!\textit{ff}\) for some \(1 \!\le \! j \le n\), then \([\mathcal {F}\models \varPhi ]\!=\!\textit{ff}\) and \([\pi _{k}(\mathcal {F}) \models \varPhi ]\!=\!\textit{ff}\) for all \(k \in \mathbb {K}_j\).
Example 3
Recall the FTS \(\textsc {VendMach}\) of Fig. 1. Figure 3 shows the MTS \(\varvec{\alpha }^{ \text {join} }({\textsc {VendMach}})\), where the allowed (may) part of the behavior includes the transitions that are associated with the optional features Open image in new window and Open image in new window in VendMach, and the required (must) part includes transitions with the presence condition true. Consider the properties introduced in Example 2. We have \([\varvec{\alpha }^{ \text {join} }(\textsc {VendMach}) \models ^3 \varPhi _1]=\bot \) and \([\varvec{\alpha }^{ \text {join} }(\textsc {VendMach}) \models ^3 \varPhi _2]=\bot \), so we cannot conclude whether \(\varPhi _1\) and \(\varPhi _2\) are satisfied by VendMach or not. \(\square \)
4 GameBased Abstract Lifted Model Checking

(1) \(C_i=(s,\textit{false})\), \(C_i=(s,\textit{true})\), \(C_i=(s,l)\): the play is finished. Such configurations are called terminal.

(2) if \(C_i=(s,A \bigcirc \varPhi )\), Player \(\forall \) chooses a musttransition Open image in new window (for refutation) or a maytransition Open image in new window of \(\mathcal {M}\) (to prevent satisfaction), and \(C_{i+1}=(s',\varPhi )\).

(3) if \(C_i=(s,E \bigcirc \varPhi )\), Player \(\exists \) chooses a musttransition Open image in new window (for satisfaction) or a maytransition Open image in new window of \(\mathcal {M}\) (to prevent refutation), and \(C_{i+1}=(s',\varPhi )\).

(4) if \(C_i=(s,\varPhi _1 \wedge \varPhi _2)\), then Player \(\forall \) chooses \(j \in \{1,2\}\) and \(C_{i+1}=(s,\varPhi _j)\).

(5) if \(C_i=(s,\varPhi _1 \vee \varPhi _2)\), then Player \(\exists \) chooses \(j \in \{1,2\}\) and \(C_{i+1}=(s,\varPhi _j)\).

(6), (7) if Open image in new window , then Open image in new window .

(8), (9) if Open image in new window , then Open image in new window .
The moves (6)–(9) are deterministic, thus any player can make them.

Player \(\forall \) wins a (maximal) play iff in each configuration of the form \(C_i=(s,A \bigcirc \varPhi )\), Player \(\forall \) chooses a move based on musttransitions and one of the following holds: (1) the play is finite and ends in a terminal configuration of the form \(C_i=(s,\textit{false})\) or \(C_i=(s,a)\) where \(a \not \in L(s)\) or \(C_i=(s,\lnot a)\) where \(a \in L(s)\); (2) the play is infinite and the witness is of the form \(A\textsf {U}\) or \(E\textsf {U}\).

Player \(\exists \) wins a (maximal) play iff in each configuration of the form \(C_i=(s,E \bigcirc \varPhi )\), Player \(\exists \) chooses a move based on musttransitions and one of the following holds: (1) the play is finite and ends in a terminal configuration of the form \(C_i=(s,\textit{true})\) or \(C_i=(s,a)\) where \(a \in L(s)\) or \(C_i=(s,\lnot a)\) where \(a \not \in L(s)\); (2) the play is infinite and the witness is of the form \(A\textsf {V}\) or \(E\textsf {V}\).

Otherwise, the play ends in a tie.
A strategy is a set of rules for a player, telling the player which move to choose in the current configuration. A winning strategy from \((s,\varPhi )\) is a set of rules allowing the player to win every play that starts at \((s,\varPhi )\) if he plays by the rules. It was shown in [24, 25] that the model checking problem of evaluating \([\mathcal {M}, s \models ^3 \varPhi ]\) can be reduced to the problem of finding which player has a winning strategy from \((s,\varPhi )\) (i.e. to solving the given 3valued model checking game).
The algorithm proposed in [24, 25] for solving the given 3valued model checking game consists of two parts. First, it constructs a gamegraph, then it runs an algorithm for coloring the gamegraph. The gamegraph is \(G_{\mathcal {M}\times \varPhi } = (N,E)\) where \(N \subseteq S \times sub(\varPhi )\) is the set of nodes and \(E \subseteq N \times N\) is the set of edges. N contains a node for each configuration that was reached during the construction of the gamegraph that starts from initial configurations \(I \times \{\varPhi \}\) in a BFS manner, and E contains an edge for each possible move that was applied. The nodes of the gamegraph can be classified as: terminal nodes, \(\wedge \)nodes, \(\vee \)nodes, \(A\bigcirc \)nodes, and \(E\bigcirc \)nodes. Similarly, the edges can be classified as: progress edges, which originate in \(A\bigcirc \) or \(E\bigcirc \) nodes and reflect real transitions of the MTS \(\mathcal {M}\), and auxiliary nodes, which are all other edges. We distinguish two types of progress edges, two types of children, and two types of SCCs (Strongly Connected Components). Mustedges (mayedges) are edges based on musttransitions (maytransitions) of MTSs. A node \(n'\) is a mustchild (maychild) of the node n if there exists a mustedge (mayedge) \((n,n')\). A mustSCC (maySCC) is an SCC in which all progress edges are mustedges (mayedges).
The gamegraph is partitioned into its mayMaximal SCCs (mayMSCCs), denoted \(Q_i\)’s. This partition induces a partial order \(\le \) on the \(Q_i\)’s, such that edges go out of a set \(Q_i\) only to itself or to a smaller set \(Q_j\). The partial order is extended to a total order \(\le \) arbitrarily. The coloring algorithm processes the \(Q_i\)’s according to \(\le \), bottomup. Let \(Q_i\) be the smallest set that is not fully colored. The nodes of \(Q_i\) are colored in two phases, as follows.
Phase 1. Apply these rules to all nodes in \(Q_i\) until none of them is applicable.

A terminal node C is colored: by T if Player \(\exists \) wins in it (when \(C=(s,\textit{true})\) or \(C=(s,a)\) with \(a \in L(s)\) or \(C=(s,\lnot a)\) with \(a \not \in L(s)\)); and by F if Player \(\forall \) wins in it (when \(C=(s,\textit{false})\) or \(C=(s,a)\) with \(a \not \in L(s)\) or \(C=(s,\lnot a)\) with \(a \in L(s)\)).

An \(A \bigcirc \) node is colored: by T if all its maychildren are colored by T; by F if it has a mustchild colored by F; by ? if all its mustchildren are colored by T or ?, and it has a maychild colored by F or ?.

An \(E \bigcirc \) node is colored: by T if it has a mustchild colored by T; by F if all its maychildren are colored by F; by ? if it has a maychild colored by T or ?, and all its mustchildren are colored by F or ?.

An \(\wedge \)node (\(\vee \)node) is colored: by T (F) if both its children are colored by T (F); by F (T) if it has a child that is colored by F (T); by ? if it has a child colored by ? and the other child is colored by ? or T (F).

Case U. The witness is of the form \(A(\varPhi _1 \textsf {U}\varPhi _2)\) or \(E(\varPhi _1 \textsf {U}\varPhi _2)\).
Phase 2a. Repeatedly color by ? each node in \(Q_i\) that satisfies one of the following conditions, until there is no change:
(1) An \(A \bigcirc \) node that all its mustchildren are colored by T or ?; (2) An \(E \bigcirc \) node that has a maychild colored by T or ?; (3) An \(\wedge \) node that both its children are colored T or ?; (4) An \(\vee \) node that has a child colored by T or ?.
In fact, each node for which the F option is no longer possible according to the rules of Phase 1 is colored by ?.
Phase 2b. Color the remaining nodes in \(Q_i\) by F.

Case V. The witness is of the form \(A(\varPhi _1 \textsf {V}\varPhi _2)\) or \(E(\varPhi _1 \textsf {V}\varPhi _2)\) (see [16, Appendix B]).
The result of the coloring is a 3valued coloring function \(\chi : N \rightarrow \{ T, F, ? \}\).
Theorem 2

(1) \([(\mathcal {M},s) \models ^3 \varPhi ']=\textit{tt}\) iff \(\chi (n)=T\) iff Player \(\exists \) has a winning strategy at n.

(2) \([(\mathcal {M},s) \models ^3 \varPhi ']=\textit{ff}\) iff \(\chi (n)=F\) iff Player \(\forall \) has a winning strategy at n.

(3) \([(\mathcal {M},s) \!\models ^3\! \varPhi ']\!=\!\!\bot \) iff \(\chi (n)\!=?\) iff none of players has a winning strategy at n.
Using Theorems 1 and 2, given the colored gamegraph of the MTS \(\varvec{\alpha }^{ \text {join} }(\mathcal {F})\), if all its initial nodes are colored by T then \([\mathcal {F}\models \varPhi ] = \textit{tt}\), if at least one of them is colored by F then \([\mathcal {F}\models \varPhi ] = \textit{ff}\). Otherwise, we do not know.
Example 4
The colored gamegraph for the MTS \(\varvec{\alpha }^{ \text {join} }({\textsc {VendMach}})\) and \(\varPhi _1=A (\lnot \textit{r} \textsf {U}\textit{r})\) is shown in Fig. 4. Green, red (with dashed borders), and white nodes denote nodes colored by T, F, and ?, respectively. The partitions from \(Q_1\) to \(Q_6\) consist of a single node shown in Fig. 4, while \(Q_7\) contains all the other nodes. The initial node \((s_0,\varPhi _1)\) is colored by ?, so we obtain an indefinite answer. \(\square \)
5 Incremental Refinement Framework
Given an FTS \(\pi _{\mathbb {K}'}(\mathcal {F})\) with a configuration set \(\mathbb {K}' \subseteq \mathbb {K}\), we show how to exploit the gamegraph of the abstract MTS \(\mathcal {M}= \varvec{\alpha }^{ \text {join} }(\pi _{\mathbb {K}'}(\mathcal {F}))\) in order to do refinement in case that the model checking resulted in an indefinite answer. The refinement consists of two parts. First, we use the information gained by the coloring algorithm of \(G_{\mathcal {M}\times \varPhi }\) in order to split the single abstract configuration \(\textit{true}\in \varvec{\alpha }^{ \text {join} }(\mathbb {K}')\) that represents the whole concrete configuration set \(\mathbb {K}'\). We then construct the refined abstract models, using the refined abstract configurations.
There are a failure node and a failure reason associated with an indefinite answer. The goal in the refinement is to find and eliminate at least one of the failure reasons.
Definition 5
A node n is a failure node if it is colored by ?, whereas none of its children was colored by ? at the time n got colored by the coloring algorithm.
Lemma 1
([24]). A failure node is one of the following.

An \(A \bigcirc \)node (\(E \bigcirc \)node) that has a maychild colored by F (T).

An \(A \bigcirc \)node (\(E \bigcirc \)node) that was colored during Phase 2a based on an \(A\textsf {U}\) (\(A\textsf {V}\)) witness, and has a maychild colored by ?.
Given a failure node \(n=(s,\varPhi )\), suppose that its maychild is \(n'=(s',\varPhi _1')\) as identified in Lemma 1. Then the mayedge from n to \(n'\) is considered as the failure reason. Since the failure reason is a maytransition in the abstract MTS \(\varvec{\alpha }^{ \text {join} }(\pi _{\mathbb {K}'}(\mathcal {F}))\), it needs to be refined in order to result either in a must transition or no transition at all. Let Open image in new window be the transition in the concrete model \(\pi _{\mathbb {K}'}(\mathcal {F})\) corresponding to the above (failure) maytransition. We split the configuration space \(\mathbb {K}'\) into \([\! [\psi ]\! ]\) and \([\! [\lnot \psi ]\! ]\) subsets, and we partition \(\pi _{\mathbb {K}'}(\mathcal {F})\) in \(\pi _{[\! [\psi ]\! ] \cap \mathbb {K}'}(\mathcal {F})\) and \(\pi _{[\! [\lnot \psi ]\! ] \cap \mathbb {K}'}(\mathcal {F})\). Then, we repeat the verification process based on abstract models \(\varvec{\alpha }^{ \text {join} }(\pi _{[\! [\psi ]\! ] \cap \mathbb {K}'}(\mathcal {F}))\) and \(\varvec{\alpha }^{ \text {join} }(\pi _{[\! [\lnot \psi ]\! ] \cap \mathbb {K}'}(\mathcal {F}))\). Note that, in the former, \(\varvec{\alpha }^{ \text {join} }(\pi _{[\! [\psi ]\! ] \cap \mathbb {K}'}(\mathcal {F}))\), Open image in new window becomes a musttransition, while in the latter, \(\varvec{\alpha }^{ \text {join} }(\pi _{[\! [\lnot \psi ]\! ] \cap \mathbb {K}'}(\mathcal {F}))\), Open image in new window is removed. The complete refinement procedure is shown in Fig. 5. We prove that (see [16, Appendix A]):
Theorem 3
The procedure Open image in new window terminates and is correct.
Example 5
We can do a failure analysis on the gamegraph of \(\varvec{\alpha }^{ \text {join} }(\textsc {VendMach})\) in Fig. 4. The failure node is \((s_1,A \bigcirc A (\lnot \textit{r} \textsf {U}\textit{r}))\) and the reason is the mayedge Open image in new window . The corresponding concrete transition in VendMach is Open image in new window . So, we partition the configuration space \(\displaystyle \mathbb {K}^{\textsc {VM}}\) into subsets Open image in new window and Open image in new window , and in the next second iteration we consider FTSs Open image in new window and Open image in new window . \(\square \)
The gamebased model checking algorithm provides us with a convenient framework to use results from previous iterations and avoid unnecessary calculations. At the end of the ith iteration of abstractionrefinement, we remember those nodes that were colored by definite colors. Let D denote the set of such nodes. Let \(\chi _D: D \rightarrow \{ T, F \}\) be the coloring function that maps each node in D to its definite color. The incremental approach uses this information both in the construction of the gamegraph and its coloring. During the construction of a new refined gamegraph performed in a BFS manner in the next \(i+1\)th iteration, we prune the gamegraph in nodes that are from D. When a node \(n \in D\) is encountered, we add n to the gamegraph and do not continue to construct the gamegraph from n onwards. That is, \(n \in D\) is considered as terminal node and colored by its previous color. As a result of this pruning, only the reachable subgraph that was previously colored by ? is refined.
Example 6
The property \(\varPhi _1\) holds for Open image in new window . The initial node of the gamegraph Open image in new window (see [16, Fig. 13, Appendix C]), is colored by T. On the other hand, we obtain an indefinite answer for Open image in new window . The model Open image in new window is shown in Fig. 7, whereas the final colored gamegraph Open image in new window is given in Fig. 6. The failure node is \((s_0,A \bigcirc A (\lnot \textit{r} \textsf {U}\textit{r}))\), and the reason is the mayedge Open image in new window . The corresponding concrete transition in Open image in new window is Open image in new window . So, in the next third iteration we consider FTSs Open image in new window and Open image in new window .
The initial node of the graph Open image in new window (see [16, Fig. 16, Appendix C]) is colored by F in Phase 2b. The initial node of Open image in new window (see [16, Fig. 17, Appendix C]) is colored by T.
In the end, we conclude that \(\varPhi _1\) is satisfied by the variants Open image in new window , and \(\varPhi \) is violated by the variant Open image in new window .
On the other hand, we need two iterations to conclude that \(\varPhi _2=E (\lnot \textit{r} \textsf {U}\textit{r})\) is satisfied by all variants in \(\displaystyle \mathbb {K}^{\textsc {VM}}\) (see [16, Appendix D] for details). \(\square \)
6 Evaluation
To evaluate our approach, we use a synthetic example to demonstrate specific characteristics of our approach, and the Elevator model which is often used as benchmark in SPL community [4, 12, 15, 20, 23]. We compare (1) our abstractionrefinement procedure Verify with the gamebased model checking algorithm implemented in Java from scratch vs. (2) familybased version of the NuSMVmodel checker, denoted fNuSMV, which implements the standard lifted model checking algorithm [5]. For each experiment, we measure T(ime) to perform an analysis task, and Call which is the number of times an approach calls the model checking engine. All experiments were executed on a 64bit Intel\(^\circledR \)Core\(^{TM}\) i53337U CPU running at 1.80 GHz with 8 GB memory. All experimental data is available from: https://aleksdimovski.github.io/automaticctl.html.
Synthetic example. The FTS \(M_n\) (where \(n>0\)) consists of n features \(A_1, \ldots , A_n\) and an integer data variable x, such that the set AP consists of all evaluations of x which assign nonnegative integer values to x. The set of valid configurations is \(\mathbb {K}_{n} = 2^{\{A_1, \ldots , A_n\}}\). \(M_n\) has a treelike structure, where in the root is the initial state with \(x=0\). In each level k (\(k \ge 1\)), there are two states that can be reached with two transitions leading from a state from a previous level. One transition is allowable for variants with the feature \(A_k\) enabled, so that in the target state the variable’s value is \(x+2^{k1}\) where x is its value in the source state, whereas the other transition is allowable for variants with \(A_k\) disabled, so that the value of x does not change. For example, \(M_2\) is shown in Fig. 8, where in each state we show the current value of x and all transitions have the silent action \(\tau \).
We consider two properties: \(\varPhi = A (\textit{true}\,\textsf {U}(x \!\ge \! 0))\) and \(\varPhi ' = A (\textit{true}\,\textsf {U}(x \!\ge \! 1))\). The property \(\varPhi \) is satisfied by all variants in \(\mathbb {K}\), whereas \(\varPhi '\) is violated only by one configuration \(\lnot A_1 \!\wedge \! \ldots \!\wedge \! \lnot A_n\) (where all features are disabled). We have verified \(M_n\) against \(\varPhi \) and \(\varPhi '\) using fNuSMV (e.g. see fNuSMVmodels for \(M_1\) and \(M_2\) in [16, Fig. 23, Appendix E]). We have also checked \(M_n\) using our Verify procedure. For \(\varPhi \), Verify terminates in one iteration since \(\varvec{\alpha }^{ \text {join} }(M_n)\) satisfies \(\varPhi \) (see \(G_{\varvec{\alpha }^{ \text {join} }(M_1) \times \varPhi }\) in [16, Fig. 24, Appendix E]). For \(\varPhi '\), Verify needs \(n+1\) iterations. First, an indefinite result is reported for \(\varvec{\alpha }^{ \text {join} }(M_n)\) (e.g. see \(G_{\varvec{\alpha }^{ \text {join} }(M_1) \times \varPhi '}\) in [16, Fig. 27, Appendix E]), and the configuration space is split into \([\! [\lnot A_1 ]\! ]\) and \([\! [A_1 ]\! ]\) subsets. The refinement procedure proceeds in this way until we obtain definite results for all variants. The performance results are shown in Fig. 9. Notice that, fNuSMV reports all results in only one iteration. As n grows, Verify becomes faster than fNuSMV. For \(n=11\) (\(\mathbb {K}=2^{11}\)), fNuSMV timeouts after 2 h. In contrast, Verify is feasible even for large values of n.
7 Related Work and Conclusion
There are different formalisms for representing variability models [2, 21]. Classen et al. [4] present Featured Transition Systems (FTSs). They show how specifically designed lifted model checking algorithms [5, 7] can be used for verifying FTSs against LTL and CTL properties. The variability abstractions that preserve LTL are introduced in [14, 15, 17], and subsequently automatic abstraction refinement procedures [8, 18] for lifted model checking of LTL are proposed, by using Craig interpolation to define the refinement. The variability abstractions that preserve the full CTL are introduced in [12], but they are constructed manually and no notion of refinement is defined there. In this paper, we define an automatic abstraction refinement procedure for lifted model checking of full CTL by using games to define the refinement. To the best of our knowledge, this is the first such procedure in lifted model checking.
One of the earliest attempts for using games for CTL model checking has been proposed by Stirling [26]. Shoham and Grumberg [3, 19, 24, 25] have extended this gamebased approach for CTL over 3valued semantics. In this work, we exploit and apply the gamebased approach in a completely new direction, for automatic CTL verification of variability models.
The works [11, 13] present an approach for software lifted model checking of #ifdefbased program families using symbolic game semantics models [10].
To conclude, in this work we present a gamebased lifted model checking for abstract variability models with respect to the full CTL. We also suggest an automatic refinement procedure, in case the model checking result is indefinite.
Footnotes
 1.
See [16, Appendix A] for definitions of \([s \models ^3 \varPhi _1 \vee \varPhi _2]\), \([\rho \models ^3 \bigcirc \varPhi ]\), and \([\rho \models ^3 \!(\varPhi _1 \textsf {V}\varPhi _2)]\).
 2.
Open image in new window is a Galois connection between complete lattices L (concrete domain) and M (abstract domain) iff \(\alpha :L\rightarrow M\) and \(\gamma :M \rightarrow L\) are total functions that satisfy: \(\alpha (l) \le _M m \iff l \le _L \gamma (m)\), for all \(l \in L, m \in M\).
References
 1.Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)zbMATHGoogle Scholar
 2.ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints. J. Log. Algebr. Methods Program. 85(2), 287–315 (2016). https://doi.org/10.1016/j.jlamp.2015.09.004MathSciNetCrossRefzbMATHGoogle Scholar
 3.Campetelli, A., Gruler, A., Leucker, M., Thoma, D.: Don’t Know for multivalued systems. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 289–305. Springer, Heidelberg (2009). https://doi.org/10.1007/9783642047619_22CrossRefzbMATHGoogle Scholar
 4.Classen, A., Cordy, M., Schobbens, P., Heymans, P., Legay, A., Raskin, J.: Featured transition systems: foundations for verifying variabilityintensive systems and their application to LTL model checking. IEEE Trans. Softw. Eng. 39(8), 1069–1089 (2013). http://doi.ieeecomputersociety.org/10.1109/TSE.2012.86CrossRefGoogle Scholar
 5.Classen, A., Heymans, P., Schobbens, P.Y., Legay, A.: Symbolic model checking of software product lines. In: Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, pp. 321–330. ACM (2011). http://doi.acm.org/10.1145/1985793.1985838
 6.Clements, P., Northrop, L.: Software Product Lines: Practices and Patterns. AddisonWesley, Boston (2001)Google Scholar
 7.Cordy, M., Classen, A., Heymans, P., Schobbens, P., Legay, A.: Provelines: a product line of verifiers for software product lines. In: 17th International SPLC 2013 Workshops, pp. 141–146. ACM (2013). http://doi.acm.org/10.1145/2499777.2499781
 8.Cordy, M., Heymans, P., Legay, A., Schobbens, P., Dawagne, B., Leucker, M.: Counterexample guided abstraction refinement of productline behavioural models. In: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, (FSE22), pp. 190–201. ACM (2014). http://doi.acm.org/10.1145/2635868.2635919
 9.Cousot, P.: Partial completeness of abstract fixpoint checking. In: Choueiry, B.Y., Walsh, T. (eds.) SARA 2000. LNCS (LNAI), vol. 1864, pp. 1–25. Springer, Heidelberg (2000). https://doi.org/10.1007/3540449140_1CrossRefGoogle Scholar
 10.Dimovski, A.S.: Program verification using symbolic game semantics. Theor. Comput. Sci. 560, 364–379 (2014). https://doi.org/10.1016/j.tcs.2014.01.016MathSciNetCrossRefzbMATHGoogle Scholar
 11.Dimovski, A.S.: Symbolic game semantics for model checking program families. In: Bošnački, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 19–37. Springer, Cham (2016). https://doi.org/10.1007/9783319325828_2CrossRefGoogle Scholar
 12.Dimovski, A.S.: Abstract familybased model checking using modal featured transition systems: preservation of CTL\(^{\star }\). In: Russo, A., Schürr, A. (eds.) FASE 2018. LNCS, vol. 10802, pp. 301–318. Springer, Cham (2018). https://doi.org/10.1007/9783319893631_17CrossRefGoogle Scholar
 13.Dimovski, A.S.: Verifying annotated program families using symbolic game semantics. Theor. Comput. Sci. 706, 35–53 (2018). https://doi.org/10.1016/j.tcs.2017.09.029MathSciNetCrossRefzbMATHGoogle Scholar
 14.Dimovski, A.S., AlSibahi, A.S., Brabrand, C., Wąsowski, A.: Familybased model checking without a familybased model checker. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 282–299. Springer, Cham (2015). https://doi.org/10.1007/9783319234045_18CrossRefGoogle Scholar
 15.Dimovski, A.S., AlSibahi, A.S., Brabrand, C., Wasowski, A.: Efficient familybased model checking via variability abstractions. STTT 19(5), 585–603 (2017). https://doi.org/10.1007/s1000901604252CrossRefGoogle Scholar
 16.Dimovski, A.S., Legay, A., Wasowski, A.: Variability abstraction and refinement for gamebased lifted model checking of full CTL (extended version). CoRR (2019). http://arxiv.org/
 17.Dimovski, A.S., Wąsowski, A.: From transition systems to variability models and from lifted model checking back to UPPAAL. In: Aceto, L., Bacci, G., Bacci, G., Ingólfsdóttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 249–268. Springer, Cham (2017). https://doi.org/10.1007/9783319631219_13CrossRefGoogle Scholar
 18.Dimovski, A.S., Wąsowski, A.: Variabilityspecific abstraction refinement for familybased model checking. In: Huisman, M., Rubin, J. (eds.) FASE 2017. LNCS, vol. 10202, pp. 406–423. Springer, Heidelberg (2017). https://doi.org/10.1007/9783662544945_24CrossRefGoogle Scholar
 19.Grumberg, O., Lange, M., Leucker, M., Shoham, S.: When not losing is better than winning: abstraction and refinement for the full mucalculus. Inf. Comput. 205(8), 1130–1148 (2007). https://doi.org/10.1016/j.ic.2006.10.009CrossRefzbMATHGoogle Scholar
 20.IosifLazar, A.F., Melo, J., Dimovski, A.S., Brabrand, C., Wasowski, A.: Effective analysis of c programs by rewriting variability. Program. J. 1(1), 1 (2017). https://doi.org/10.22152/programmingjournal.org/2017/1/1CrossRefGoogle Scholar
 21.Larsen, K.G., Nyman, U., Wąsowski, A.: Modal I/O automata for interface and product line theories. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 64–79. Springer, Heidelberg (2007). https://doi.org/10.1007/9783540713166_6CrossRefzbMATHGoogle Scholar
 22.Larsen, K.G., Thomsen, B.: A modal process logic. In: Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS 1988), pp. 203–210. IEEE Computer Society (1988). http://dx.doi.org/10.1109/LICS.1988.5119
 23.Plath, M., Ryan, M.: Feature integration using a feature construct. Sci. Comput. Program. 41(1), 53–84 (2001). https://doi.org/10.1016/S01676423(00)000186CrossRefzbMATHGoogle Scholar
 24.Shoham, S., Grumberg, O.: A gamebased framework for CTL counterexamples and 3valued abstractionrefinement. ACM Trans. Comput. Log. 9(1), 1 (2007). https://doi.org/10.1145/1297658.1297659MathSciNetCrossRefzbMATHGoogle Scholar
 25.Shoham, S., Grumberg, O.: Compositional verification and 3valued abstractions join forces. Inf. Comput. 208(2), 178–202 (2010). https://doi.org/10.1016/j.ic.2009.10.002MathSciNetCrossRefzbMATHGoogle Scholar
 26.Stirling, C.: Modal and Temporal Properties of Processes. Texts in Computer Science. Springer, New York (2001). https://doi.org/10.1007/9781475735505CrossRefzbMATHGoogle Scholar
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.