=Paper=
{{Paper
|id=Vol-1770/ARQNL2016_paper3
|storemode=property
|title=A Dynamic Logic for Configuration
|pdfUrl=https://ceur-ws.org/Vol-1770/ARQNL2016_paper3.pdf
|volume=Vol-1770
|authors=Ching Hoo Tang,Christoph Weidenbach
}}
==A Dynamic Logic for Configuration==
https://ceur-ws.org/Vol-1770/ARQNL2016_paper3.pdf
A Dynamic Logic for Configuration
Ching Hoo Tang and Christoph Weidenbach
Max Planck Institute for Informatics, Saarbrücken, Germany
{chtang, weidenbach}@mpi-inf.mpg.de
Abstract
We define the new dynamic logic PIDL+ that extends our previously developed logic PIDL (Propo-
sitional Interactive Dynamic Logic) with arithmetic constraints. The language of PIDL+ is motivated
by real world configuration systems, in particular, configuration systems for power plants. A PIDL+
specification consists of the description of an initial state, global constraints, and actions. Its semantics
are the possible worlds starting from the initial state, spanned by the actions and restricted by the
constraints. It distinguishes user actions from rule actions. Any user action is followed by a unique
fixed point, called rule-terminal state, generated through exhaustive application of rule actions from the
specification. The built in rule action fixpoint semantics and arithmetic constraints distinguish PIDL+
from known dynamic or action logics. Correctness of a PIDL+ specification as well as reachability of
a particular state are decidable. We provide sound and complete algorithms.
1 Introduction
The dynamic logic PIDL+ is motivated by real-world configuration systems, e.g., configuration
systems for steel or power plants as they are productive at Siemens [8]. A run of such a
configuration system is a dialog between its user picking components or setting parameters
inside certain bounds and the system reacting by adjusting the current configuration such that
eventually a buildable product is the result. Today’s implementations of such configuration
systems are not based on formal specifications but are typically built on top of general-purpose
programming languages. Hence, overall soundness or completeness of the configuration system
cannot be automatically shown.
PIDL+ copes with the needed expressiveness of real-world configuration systems on one side
and on the other side enables automatic verification of relevant system properties. The above
form of dialog between the system and the user needs to distinguish variables controlled by the
user and variables controlled by the system. Soundness is defined by one quantifier alternation:
for all inputs to variables controlled by the user, the system can react by adjusting variables
under its control such that eventually a buildable product is the result. If for any final product
there is a sequence of user inputs reaching a state representing this product, the configuration
system is complete.
From the user perspective, the system should terminate after each input and always produce
the same result on the same inputs. In PIDL+ the user and the system are modeled by rules,
called transitions (Definition 1). A user or system transition comes in a “precondition ;
update” form: if the precondition of a transition is implied by the current state, its update is
applied to the current state and yields the next state. After the application of a user transition,
the system transitions, later called rules, are exhaustively applied until a unique state is reached
that is a fixpoint with respect to the system transitions. We call such a state a rule-terminal
state. The system is sound if whatever the user does inside the bounds specified eventually a
rule-terminal state representing a product can be reached. Overall requirements to products
are represented by constraint formulas in PIDL+. They have to be satisfied by any state and,
in particular, by states representing a final product (Definition 17).
ARQNL 2016 36 CEUR-WS.org/Vol-1770
A Dynamic Logic for Configuration Tang and Weidenbach
In real-world applications it is necessary that the set of variables controlled by the user
dynamically changes. For example, if the user picks a certain component but subsequent user
choices require an update to the component by the system, the user decision is overwritten and
hence the component is no longer under the control of the user. In PIDL+ this is represented
by a set of user controlled variables attached to each state (Definition 4). Eventually a state is
represented by a set of literals and a set of user controlled variables.
Components are presented in PIDL+ by propositional variables and parameters by inte-
ger variables. For an admissible PIDL+ specification (Definition 3) all integer variables are
finitely bounded. Therefore, the number of all reachable states is finite and properties of the
specification become decidable. A priori bounded integer variables are typical for a real-world
configuration system, e.g., out of a component box no car company is able to build an engine
with arbitrarily high throughput. Still, result variables that are needed to represent the even-
tual product may be of type real in PIDL+ and computed by complex expressions. In order to
preserve decidability, they must not occur in any transition (Definition 3).
Semantically, a system state is a possible world where all propositional and integer variables
have fixed values. Then a user or system transition leads to the next world. We call this
semantics the small step semantics. It is easy to understand but not well-suited for computing
properties as the number of possible worlds becomes the product over the combination of all
variable ranges. In this paper we present a big step semantics where a state of the big step
semantics represents up to exponentially many states of the small step semantics. In any state
the integer variables are bounded, but do not need to have a fixed single value. The semantics
is existential for user and universal for all other variables: the precondition of a transition
is satisfied in a state, if for some instance of the user variables satisfying the bounds of a
state and all instances of all other variables satisfying the bounds of a state the precondition is
implied. The bounds either come from the initial state or are updated by transition applications.
With respect to the above semantics, a transition depending on a user variable might only be
applicable to some of the potential values of the variable, but not to all. This makes it necessary
to partition the values of variables in states with respect to a transition in order to compute
the next state of the big step semantics. We call such partitions meeting the precondition of
a transition with respect to a state a selection (Definition 5). Finite selections always exist
because the applicability of transitions only depends on bounded integer variables.
PIDL+ is the extension of PIDL [9] with arithmetic constraints. Similar approaches that
deal with logics formalizing change naturally arise from modal logics, originally introduced to
describe the behavior of programs, prominently represented by Propositional Dynamic Logic
[10] and its variants [2]. Boolean games [12] and variants thereof [17] are another mechanism
to model a changing system, in this case by considering situations as they appear in game
theory [14], where players play games by setting assignments of Boolean variables. These
approaches are different from PIDL+ insofar that they do not have the inherent features to
describe the characteristic user-rule relationship with rule-terminal states of the configuration
system as mentioned earlier, or that they, in the case of Boolean games, focus on equilibria
depending on certain strategies, as opposed to an exhaustive unfolding of user and rule actions
in PIDL+. Also, our logic supports arithmetic constraints through selections. The same holds
for approaches based on temporal logic [15, 4] and model checking [5], where solutions, for
example, deal with the verification of configuration product variants [6] modeled as feature
models [13], whose logics have been studied extensively [7]. Further work that explicitly centers
on the analysis of configuration systems usually provides stage-wise verification, that is, it aims
to analyze the configuration after each user input and guide the user through the configuration
process, often through constraint satisfaction [1, 16, 3].
2
37
A Dynamic Logic for Configuration Tang and Weidenbach
In Section 2 we introduce the above described syntax and semantics of PIDL+ in full
detail. The section ends with an example specification illustrating the features of the logic
(Example 20). Section 3 presents algorithms checking soundness and completeness and we end
with a short conclusion, Section 4.
2 The Logic PIDL+
We give a detailed description of our logic PIDL+ in this section. Its design is geared towards
modeling the dynamics of an interactive configuration system with the help of a states-and-
transitions semantics. The states describes the possible worlds reachable from the initial state
via defined sets of user and rule transitions. The base logic underlying the formulas used to
express single states and transitions is propositional logic in combination with the theory of
arithmetic over the reals. Relevant concepts connected with the base logic and general notions
essential for the design of PIDL+ are given in the preliminaries subsection, which is followed
by the definition of the actual syntax of PIDL+. Its semantics of states and transitions is
contained in the final part of this section.
2.1 Preliminaries
The basic units of PIDL+ are terms and formulas derived from the fragment of first-order logic
that is composed of propositional variables and the theory of reals. We provide the central
notions needed in this paper.
We fix the order-sorted signature Σ := ({R, Z}, R ∪ {+, −, ·, <, ≤, >, ≥, ≈, 6≈}). It has sorts
R and Z, where Z is a subsort of R, Z ⊂ R, constants R, where the sort of each c ∈ R
is R, written as sort(c) = R, function symbols +, −, and ·, where it holds that sort(f ) =
R × R → R, f ∈ {+, −, ·}, and predicate symbols <, ≤, >, ≥, ≈, and 6≈, where it holds that
sort(◦) = R × R, ◦ ∈ {<, ≤, >, ≥, ≈, 6≈}.
We say that a set of variables X is Σ-sorted if the sort of each variable x ∈ X is one of the
sorts specified in Σ: sort(x) ∈ {R, Z}. We choose to have two sorts R and Z, to be interpreted
as the sets R and Z, because, as is delineated later in the section, we want to interpret numerical
expressions that have an effect on the action dynamics as bounded integers, which is a crucial
requirement for achieving decidability of the logic. Additionally, we allow those expressions
which do not affect the action flow to be over the reals. They represent results that are purely
restricted to the single worlds, holding information values of the configurations.
A term t over the signature Σ and a Σ-sorted variable X is called Σ-term and is defined by
the usual rules known from first-order logic using variables, constants and function symbols.
TΣ (X) denotes the set of all terms over the signature Σ and the variable set X. We use the
customary infix notation when writing Σ-terms. For example, we write x + 9 instead of +(x, 9).
An atom over Σ is an expression of the form t◦t0 , a simple atom over Σ is an atom of the form
x ◦ t, and a simple bound over Σ is a simple atom of the form x ◦ c, where x ∈ X, t, t0 ∈ TΣ (X),
c ∈ Z and ◦ ∈ {<, ≤, >, ≥, ≈, 6≈}.
A formula over Σ, a Σ-sorted variable set X and a set of propositional variables Π, also
called Σ-formula, is a first-order formula constructed in the usual way using the terms from
TΣ (X), the variables from Π, the atoms over Σ, the usual Boolean connectives ¬, ∧, ∨, → and
↔, and the quantifier symbols ∀ and ∃. We write FΣ (X, Π) to denote the set of all formulas
over Σ, X and Π.
Let var (F ) denote the set of variables that occur in a formula F . Analogously, var (N )
denotes the set of variables that occurs in a set N of formulas. Also, varl (x ◦ t) denotes the
3
38
A Dynamic Logic for Configuration Tang and Weidenbach
variable that is the left operand of the atom x◦t, that is, varl (x◦t) = x. If N is a set containing
atoms over Σ, then varl (N ) denotes the set of variables that are the left operands of the atoms
in N : varl (N ) = {x|x ◦ t ∈ N }. We use varl because the relevant terms in the semantics
take the form of simple atoms x ◦ t in which the relevant variables are always on the left side
of the operation by design. Likewise, we define the intersection N |M of a set N of formulas
with a set M of variables as the set N |M := {F ∈ N |varl (F ) ∩ varl (M ) 6= ∅}. For example,
{x ≥ w + 4, y ≈ 23, z < y, C}|{x,z} = {x ≥ w + 4, z < y}.
The objects of the signature Σ are interpreted in the usual way as done in the theory of
reals: The sorts R and Z are interpreted as R and Z, respectively, the symbols are interpreted
as the usual operations and comparisons in R. We use IΣ , called Σ-interpretation, to denote
both the valuation of a term from TΣ (X) and the truth value of a formula from FΣ (X, Π).
Again, valuations and truth values are defined as one expects from the first-order logic theory
of reals.
We say that a Σ-interpretation satisfies a Σ-formula F , written as IΣ |= F, if IΣ (F ) = 1.
A formula F is satisfiable if there is a Σ-interpretation IΣ with IΣ |= F , and F is valid if
IΣ |= F for all Σ-interpretations IΣ . Formula F entails formula F 0 , written as F |= F 0 , if the
following holds: If IΣ is a Σ-interpretation and satisfies F , then IΣ also satisfies F 0 . A set of
N of Σ-formulas entails a Σ-formula F 0 , written as N |= F 0 , if the following holds: If IΣ is a
Σ-interpretation and satisfies each F ∈ N , then IΣ also satisfies F 0 .
We consider tuples of integer intervals, which appear in the semantics of PIDL+. As ex-
pected, intersection of a tuple t = (I1 , . . . , In ) with another t0 = (I10 , . . . , In0 ) is defined compo-
nentwise: t ∩ t0 := (I1 ∩ I10 , . . . , In ∩ In0 ). An intersection is empty, written t ∩ t0 = ∅, if Ii ∩ Ii0 = ∅
for some i. For an interval I = [v1 , v2 ], the atomic representation at(I, x) of I with respect to
a variable x is the set of arithmetic atoms at(I, x) := {x ≥ v1 , x ≤ v2 }.
2.2 Syntax
We now define the syntax of PIDL+. It takes the form of a specification tuple whose components
comprehensively describe a configuration system including its variables, rules and possible user
actions.
Definition 1. A PIDL+ specification is a tuple S+ = (Π, X, SI , UI , C, TU , TR ), where the
components are as follows: Π is a finite set of propositional variables, X is a finite set of Σ-
sorted variables, (SI , UI ) is called the initial state, C is a finite set of Σ-formulas in FΣ (X, Π),
called the constraints, and TU and TR are finite sets of user and rule transitions Λ ∧ F ; E,
respectively, where (1) SI is a finite set of simple bounds x ◦ c in FΣ (X, Π) and propositional
literals over Π with
∀~xu ∃~y SI |UI → (SI \ SI |UI ) ∪ C
being satisfiable, ~xu = x1 . . . xk being all the variables in UI and ~y = y1 . . . yl being all the
variables in X \ UI , (2) UI ⊆ X, called the set of initial user variables, (3) Λ is a conjunction
of simple atoms x ◦ t over Σ, called the arithmetic condition, (4) F is a conjunction of literals
over Π, called the propositional condition, (5) E is called the update set and is a satisfiable set
of simple bounds x ◦ c over Σ and propositional literals over Π for user transitions and is a
satisfiable set of simple atoms x ◦ t over Σ and propositional literals over Π for rule transitions.
The set Π provides the propositional variables needed to describe all the Boolean statements
about the worlds occurring in a configuration process, such as “part A is active”, whereas the
set X represents the numerical variables of the configuration, such as the weight of a component
in kg. The initial state describes the starting world of the modeled system. The set SI contains
4
39
A Dynamic Logic for Configuration Tang and Weidenbach
simple bounds and propositional literals that represent the initial configuration state, together
with UI which indicates which of the system’s variables are set by the user. The models of
the specification, as explained in the next subsection, consider further states that arise from
this initial state. The requirement that ∀~xu ∃~y SI |UI → (SI \ SI |UI ) ∪ C must be satisfiable
basically says that the world is consistent: The simple bounds x ◦ c in SI |UI represents the
range of user input with respect to that state, and they are consistent with the other simple
bounds and the formulas in C, the constraints. This consistency requirement is used for all
the other states induced by the system, as can be seen in the semantics section. The general
and domain-specific constraints of the configuration system are encoded in C. For example,
it typically contains formulas that express “option A and option B cannot be simultaneously
active”. Finally, we have two different sets of of transitions, namely user transitions TU and
rule transitions TR , whose elements are constructs Λ ∧ F ; E. The conjunction Λ ∧ F form
the condition part of a transition and express what must be met in the current state in order to
have a transition from it to another state. There is a clear separation between the arithmetic
conditions Λ and the propositional conditions F . The set E determines how the next state is
defined by updating the current state with the atoms and literals in E if a transition is indeed
possible. It expresses user actions in the case of TU and rule actions in the case of TR . User
actions can set simple bounds while rules can update with simple atoms, which is a natural
representation of a configuration system.
Definition 1 defines specifications in a broad sense. We work with a restricted class of
specifications that have certain properties that, in particular, enables us to achieve finiteness of
the system and thus decidability. First, we identify the set of all variables involved in transitions,
which plays an important role in this.
Definition 2. The transition variables XT of a specification S+ are the set
XT := {x|x ∈ var (Λ ∧ F ; E), Λ ∧ F ; E ∈ (TU ∪ TR )}.
Now the desired kind of specification, which we call admissible specifications, is defined as
follows:
Definition 3. A specification S+ is admissible if the following holds. (1) For each x ∈ XT ,
sort(x) = Z, (2) the constraints set C has the form
! !
V V
x ≥ cx1 ∧ x ≤ cx2 ∧ x ≈ tx ∧ Φ,
x∈XT x∈Xr
where cx1 , cx2 ∈ Z for all x ∈ XT , Xr ⊆ X \ XT , tx ∈ TΣ (XT ) for all x ∈ Xr , and Φ is a
propositional formula over Π, and (3) for each Λ ∧ F ; E ∈ (TU ∪ TR ), it holds that if x ◦ t ∈ E,
then x 6∈ var (t).
The composition of the constraints C in admissible specifications is fixed. There, variables
occurring in transitions are set to be over the integers and bounded by integer constants. They
do not appear anywhere else in the constraints. As is explained later in the semantics, the
atoms x ◦ c in a state with x ∈ U of a state stand for the possible instances of the state modulo
user choices. By bounding the variables relevant to the transition flow we achieve decidability
of the transition system of PIDL+. Variables not in XT do not affect transitions and function
only as holders of result values specific to the current state. Their valuations are derived from
the values of terms over the transition variables. Moreover, admissible specifications may have
constraints that are purely propositional, which are encoded in the formula Φ.
5
40
A Dynamic Logic for Configuration Tang and Weidenbach
2.3 Semantics
Given a PIDL+ specification, the semantics is a possible-worlds semantics with states and
transitions between them, starting from the initial state and adhering to the constraints and
transition conditions of the specification. For the rest of the paper, we assume that we only
work with admissible specifications. While the meaning of the initial state is briefly given in
the syntax section because the initial state is part of the specification, we now define states
generally.
Definition 4. A state is a pair (S, U ) of a set of user variables U ⊆ X, and a set of literals S
containing simple atoms over Σ and propositional literals over Π. The subset S|U is always a
set of simple bounds over Σ.
A state in PIDL+ contains the description of a corresponding state in the configuration
system. As mentioned in the syntax section, propositional literals and arithmetic atoms fulfill
this task. The user variables U tell us what variable has been set by the user during the
configuration process so far. The simple bounds x ◦ c with x ∈ U describe the range of user
choices in that state. For example, the state ({x > 4, x ≤ 21, A}, {x}) implicitly corresponds
to a set of worlds. It includes an instance in which A holds and the user has chosen x ≈ 5,
another instance in which A holds and the user has set x ≈ 6, or one where A holds and x ≈ 18
by a user decision.
We adopt the following convention. Let (S, U ) be a state. We write ~xu to mean all the
variables of U and ~y to mean all the variables in X \ U . If we use this notation, it should be
clear from the context that we refer to the U of a certain state.
The view that a state is an aggregation of all the possible instances modulo the user decisions,
embodied by the simple bounds in S|U , has far-reaching implications for our semantics. We
define transitions later, but we already want to say at this point that different instances of the
user variable valuations can imply different behaviors concerning transitions. Consequently,
it is necessary to divide a state with respect to its user choices. We do this by considering
selections.
Definition 5. Let (S, U ) be a state. Furthermore, let Λ ∧ F ; E ∈ (TU ∪ TR ) be a transition.
Then, a selection γ with respect to (S, U ) and Λ ∧ F ; E is defined as follows: (1) If U is a
non-empty set and U = {x1 , . . . , xn }, then γ is a tuple of interval integers (I1 , . . . , In ), where
∀~y (S|U ∧ (S \ S|U ∪ C → Λ ∧ F ))σ
is valid for all σ = {x1 7→ v1 , . . . , xn 7→ vn } with vi ∈ Ii and i = 1, . . . , n, and (2) if U = ∅, then
γ is the empty tuple () and ∀~y S ∪ C → Λ ∧ F is valid.
We write γ(i) to denote the i-th component Ii of γ = (I1 , . . . , In ). The intervals I1 , I2 , . . . , In
of a selection contain values of the user variables x1 , x2 , . . . , xn for which ∀~y (S|U ∧(S \S|U ∪C →
Λ∧F )) is valid, expressed by all substitutions that map the variables from U to the values of the
intervals. These intervals exist if there is at least one valuation of the user variables that makes
the above statement true. If this is the case, we consider the condition of the corresponding
transition Λ ∧ F ; E to be fulfilled. It can be read as “all assignments done by the user that
are based on the values occurring in the selection and that are consistent with the simple atoms
of S|U entail the transition condition Λ ∧ F , thus that transition is possible”. As is defined later
in this section, all transitions are with respect to some selections. If the set of user variables
is empty, the criterion for allowing a transition reduces to essentially checking the validity of
S ∪ C → Λ ∧ F.
In our setting, considering subsets of user choices and their properties makes sense. We then
talk about subselections.
6
41
A Dynamic Logic for Configuration Tang and Weidenbach
Definition 6. Let γ and γ 0 be two selections of the same length. We say that γ 0 is a subselection
of γ, written as γ 0 ⊆ γ, if γ 0 (i) ⊆ γ(i) for all i = 1, . . . , n. We say that γ 0 is a proper subselection
of γ, written as γ 0 ⊂ γ, if γ 0 ⊆ γ and γ 0 (i) ⊂ γ(i) for an i ∈ {1, . . . , n}.
In general, there can be more than one possible selection with respect to a transition. In our
semantics, we restrict the possibilities to consider to maximal selections. Maximal selections
are defined with the help of subselections.
Definition 7. A selection γ with respect to (S, U ) and Λ ∧ F ; E is maximal if either γ = ()
or there is no selection γ 0 with respect to (S, U ) and Λ ∧ F ; E such that γ ⊂ γ 0 .
Information about current selections may have to be included in the states. This means we
have to write the intervals occurring the selections as simple bounds. Atomic representations
denote those simple bounds that corresponds to the intervals of the respective selection. They
are based on the atomic representations of integer intervals mentioned in the preliminaries of
this section.
Definition 8. Let γ be a selection with respect to a state (S, U ) and a transition. The atomic
representation at(γ) of γ is defined as follows:
S (1) If U = {x1 , . . . , xn }, then
at(γ) := i=1,...,n at(γ(i), xi ), and
(2) if U = ∅, then at(γ) := ∅.
In a transition from a state to a new state, the new state is the result of an update of the
former state. The updates are based on the update sets E of the transitions Λ ∧ F ; E ∈
(TU ∪ TR ). The way how updates are done depends on the type of the transition: Updates with
respect to rule transitions are different from updates with respect to user transitions. We first
define updates of rule transitions.
Definition 9. The rule update operator /R takes a state (S, U ) and a pair (E, γ) as arguments,
where (1) E is an update set and (2) γ is a selection with respect to (S, U ) and a rule transition
Λ ∧ F ; E ∈ TR . It is defined as (S, U ) /R (E, γ) := (S 0 , U 0 ), where
• U 0 := U \ varl (E),
• S 0 := {L|L literal over Π, L ∈ S, L 6∈ E}∪
{L|L literal over Π, L ∈ E}∪
{x ◦ t|x ◦ t ∈ S, x ∈ X \ U, x 6∈ varl (E)}∪
{x ◦ t|x ◦ t ∈ at(γ), x ∈ U, x 6∈ varl (E)}∪
{x ◦ t|x ◦ t ∈ E}.
The propositional literals and simple atoms of the update set E replaces the propositional
literals and simple atoms of the old state literal set S if those are of the same propositional
variables and left-hand variables, respectively, to form the new state literal set S 0 . We fix the
variables on the left-hand sides of simple atoms x ◦ t to be the relevant variables determining
the updates of atoms. Expressions of E with variables new to the old state are added to S 0
too. Expressions in S whose propositional variables or left-hand variables do not occur as
propositional variables or left-hand variables in E are preserved in S 0 . However, there is a
distinction in what is preserved with respect to whether the left-hand variables x of the simple
atoms x ◦ t are in U . If x is not a user variable, then the simple atoms x ◦ t from S are just
carried over in the next state. If x ∈ U , then it is not the simple atoms from S that are
preserved but the simple atoms in the atomic representation at(γ) where x appears on the left
sides of the atoms. The general rationale behind this is the following: The selection γ can
7
42
A Dynamic Logic for Configuration Tang and Weidenbach
be seen as a subset of the user choices defined by S|U that makes the transition possible, as
described earlier with the definition of selections. It is crucial to keep track of what selection
is responsible for the transition. Therefore, a simple atom x ◦ t of at(γ) is contained in the
new state by definition unless x occurs in varl (E). In that case, the corresponding atom from
E takes precedence and is contained in S 0 instead of the one from at(γ). We consider the
expressions appearing in the update set E of a rule transition to be “overwriting” existing user
decisions. That is why, after the update, we do not see those variables of U occurring in varl (E)
as user variables anymore and we set U 0 := U \ varl (E). This corresponds to the situation in
the configuration when it is necessary to overwrite user choices due to the system constraints.
In general, if (S 0 , U 0 ) 6= (S, U ), we also say that the update or transition changes or alters the
state (S, U ).
We can now formally define rule transitions. If a state is consistent and there is an appro-
priate maximal selection with respect to a transition, then there is a transition from that state
to a new state with respect to the corresponding transition, with the new state being the result
of an update by the rule update operator /R .
Definition 10. A rule transition from a state (S, U ) to a state (S 0 , U 0 ) with respect to a rule
transition Λi ∧ Fi ; Ei ∈ TR and a selection γ is written as
(S, U ) →(i,γ) (S 0 , U 0 ),
where (1) ∀~xu ∃~y S|U → (S \ S|U ) ∪ C is satisfiable, (2) γ is a maximal selection with respect to
(S, U ) and Λi ∧ Fi ; Ei , and (3) (S 0 , U 0 ) = (S, U ) /R (Ei , γ).
The criterion that ∀~xu ∃~y S|U → (S \ S|U ) ∪ C must be satisfiable is the same as the one
used for the initial state (SI , UI ) in the definition of specifications. It is the general criterion
determining the consistency of a state.
In the configuration systems we consider, as mentioned earlier, all the rules are applied
whenever possible until a fixed point is reached. Then, a user decision may happen after which
another round of rule applications takes place. As long as rules can be applied that can change
a state, no user action is allowed. To define user updates and user transitions, we therefore need
the notion of rule-terminal states to denote states that are indeed “ready” for user transitions.
Definition 11. Let γ be a maximal selection with respect to a state (S, U ) and a user transition
Λ∧F ; E ∈ TU . (1) If γ 6= (), then we call a selection γ 0 with γ 0 ⊆ γ a rule-terminal subselection
of γ if the following holds: (a) there is no selection γ ∗ with respect to (S, U ) and a rule transition
Λ∗ ∧ F ∗ ; E ∗ ∈ TR , such that γ ∗ ∩ γ 0 6= ∅ and (S, U ) 6= (S, U ) /R (E, γ ∗ ), and (b) there is no
other selection γ # that fulfills (a) and γ 0 ⊂ γ # . (2) If γ = (), then we call γ rule-terminal if
() is not a maximal selection with respect to (S, U ) and a rule transition Λ∗ ∧ F ∗ ; E ∗ ∈ TR
such that (S, U ) 6= (S, U ) /R (E, ()). In the respective cases, we say that (S, U ) is rule-terminal
with respect to γ 0 or () and to Λ ∧ F ; E.
A state is thus rule-terminal with respect to a selection γ 0 and a user transition if γ 0 is such
a subselection of a maximal selection γ with respect to the state and the user transition that
it does not have a non-empty intersection with another selection that can be used for a rule
transition changing the state. A non-empty intersection would mean that the current selection
making the user transition possible also contains instances of the user decisions that enable rule
transitions that alter the state. Therefore, the state cannot be considered to be a fixed point
yet with respect to that selection. What we are interested in is a subselection γ 0 for which
the state becomes a fixed point. To have uniqueness, we only consider those γ 0 that are not
subselections of selections having the same property, analogously to the definition of maximal
selections.
8
43
A Dynamic Logic for Configuration Tang and Weidenbach
The definition of the user update operator is very similar to that of the rule update operator.
The difference is that rule updates may reduce the set of user variables, while user updates may
increase it. This is because user transitions represent user actions, so the corresponding update
set E can introduce new user variables.
Definition 12. The user update operator /U takes a state (S, U ) and a pair (E, γ) such that
(1) E is an update set, (2) γ is a rule-terminal selection with respect to (S, U ) and a user
transition Λ∧F ; E ∈ TU , and is defined as (S, U )/U (E, γ) := (S 0 , U 0 ), where U 0 := U ∪varl (E)
and S 0 is defined in the exact same way as in the case of the rule update operator /R .
User transitions are then defined analogously to rule transitions, with respect to rule-
terminal states.
Definition 13. A user transition from a state (S, U ) to a state (S 0 , U 0 ) with respect to a user
transition Λi ∧ Fi ; Ei ∈ TU and a selection γ is written as
(S, U ) →(i,γ) (S 0 , U 0 ),
where (1) ∀~xu ∃~y S|U → (S \ S|U ) ∪ C is satisfiable, and (2) (S, U ) is rule-terminal with respect
to γ and Λi ∧ Fi ; Ei , and (3) (S 0 , U 0 ) = (S, U ) /U (Ei , γ).
A classic notion connected to state transition systems is that of reachability. We give the
corresponding concepts in our semantics involving paths and reachability. A path tells us, in
particular, what user actions and rule actions were responsible for reaching a certain state,
starting from the initial state (SI , UI ) of a specification.
Definition 14. A path from a state (S, U ) to a state (S 0 , U 0 ) is a tuple ((i1 , γ1 ), . . . , (in , γn ))
such that (S0 , U0 ) →(i1 ,γ1 ) (S1 , U1 ) →(i2 ,γ2 ) · · · →(in−1 ,γn−1 ) (Sn−1 , Un−1 ) →(in ,γn ) (Sn , Un ) is
a sequence of transitions, where for all j = 1, . . . , n it holds that γj is a maximal selection with
respect to (Si−1 , Ui−1 ) and a Λij ∧ Fij ; Eij ∈ TR or (Si−1 , Ui−1 ) is rule-terminal with respect
to γj and a Λij ∧ Fij ; Eij ∈ TU , and moreover (S0 , U0 ) = (S, U ) and (Sn , Un ) = (S 0 , U 0 ).
Definition 15. A state (S 0 , U 0 ) is reachable from a state (S, U ) if there is a path from (S, U )
to (S 0 , U 0 ). A state (S, U ) is always reachable from itself via the empty path.
The question whether a specification is consistent is determined by whether it has a model.
A model is basically the set of all states and transitions between them when starting from the
initial state, where no inconsistent world according to the definition of Σ-interpretations as
described in the preliminaries subsection is reachable.
Definition 16. An interpretation of an admissible specification S+ is a tuple (VS+ , TS+ , IS+ )
with (1) the state space VS+ := {(S, U )|(S, U ) reachable from (SI , UI )}, (2) the transition space
TS+ := {((S, U ), i, γ, (S 0 , U 0 ))|(S, U ), (S 0 , U 0 ) ∈ VS+ ,
(S, U ) →(i,γ) (S 0 , U 0 ), Λi ∧ Fi ; Ei ∈ (TU ∪ TR )}, and
(3) the state interpretations IS+ := {((S, U ), IΣ )|(S, U ) ∈ VS+ , IΣ |= S}.
Note that indeed (SI , UI ) ∈ VS+ according to our definition of reachability. An interpreta-
tion is a model if the constraints C are satisfied in each world.
Definition 17. An interpretation (VS+ , TS+ , IS+ ) is a model of a an admissible specification
S+ if IΣ |= C for each ((S, U ), IΣ ) ∈ IS+ .
Definition 18. An admissible interpretation S+ is sound if it has a model. Moreover, S+
is complete with respect to a set XU of user variables if for every σ : XU → Z with Cσ being
satisfiable, there is (S, U ) ∈ VS+ such that (S ∪ C)σ is satisfiable and for each x ∈ XU there is
a user transition Λi ∧ Fi ; Ei ∈ TU with x ∈ varl (Ei ), ((Sj−1 , Uj−1 ), i, γ, (Sj , Uj )) ∈ TS+ .
9
44
A Dynamic Logic for Configuration Tang and Weidenbach
Soundness and completeness can be effectively checked, once a finite representation of the
transition graph is computed. Such a graph is the result of the algorithm buildInterpreta-
tion, Algorithm 1.
From a user’s perspective, soundness means that he/she cannot navigate the system into
an inconsistent state. Completeness means that within the initial bounds with respect to the
overall constraints, any product can be configured by respective user actions for a given set of
user controllable variables.
The following theorem follows from the finiteness of the components of admissible specifi-
cations and the fact that the transition variables in them are over bounded integers.
Theorem 19. The components VS+ and TS+ of each interpretation of an admissible specifi-
cation S+ are finite. Soundness and completeness are decidable.
We conclude this section with an example.
Example 20. Assume the following admissible specification:
Π = {A, B, C, D, E},
X = {x1 , x2 , y1 },
SI = {¬A},
UI = ∅,
C = {x1 ≥ 0, x1 ≤ 100,
x2 ≥ 0, x2 ≤ 100,
y1 ≥ 0, y1 ≤ 1000,
C → D},
TU = {¬A ;u1 {A, B, x1 ≥ 20, x1 ≤ 90},
x1 < 74 ∧ B ;u2 {x2 > 5, x2 < 20}},
TR = {x1 ≤ 30 ;r1 {¬C},
x2 ≥ 10 ∧ D ;r2 {y1 ≈ x1 · x2 , C},
y1 ≥ 600 ∧ y1 ≤ 800 ;r3 {¬E}}.
In the following, we describe how the set of states that are reachable from the initial state can
be derived. We refer to transitions Λi ∧ Fi ; Ei by their indices i. From the initial state
(SI , UI ) = ({¬A}, ∅), we see that user transition u1 is possible using the empty selection (),
since UI is empty. With that, the relevant criterion for () to be the right selection is that
∀~y {¬A} ∪ C → ¬A is valid, which is obviously the case. We get a transition
(SI , UI ) →(u1 ,()) (S1 , U1 ), where S1 = {A, B, x1 ≥ 20, x1 ≤ 90} and U1 = {x1 },
according to the update (SI , UI ) /U ({A, B, x1 ≥ 20, x1 ≤ 90}) as defined in Definition 12.
Note that the update overwrites the literal ¬A from the initial state and replaces it with the
literal A. The new state (S1 , U1 ) symbolizes user choices of the variable x1 with integer values
between 20 and 90. From (S1 , U1 ), there are two possible transitions, one of which is a rule
transition and the other is a user transition. First, rule transition r1 is applicable for the max-
imal selection ([20, 30]). Note that indeed ∀~y (S1 |U1 ∧ (S1 \ S1 |U1 ∪ C → x1 ≤ 30))σ is valid for
all σ = {x1 7→ v}, v ∈ [20, 30] as required in Definition 5. We register a transition
(S1 , U1 ) →(r1 ,([20,30])) (S2 , U2 ),where S2 = {A, B, ¬C, x1 ≥ 20, x1 ≤ 30} and U2 = {x1 },
according to /R as defined in Definition 9. On the other hand, there is a rule-terminal selection
with respect to (S1 , U1 ) and user transition u2 . The maximal selection with respect to (S1 , U1 )
and user transition u2 is [20, 73]. The subselection that is rule-terminal with respect to that is
[31, 73]. No other rule transition that changes the state is possible in this subselection. Thus,
we have
10
45
A Dynamic Logic for Configuration Tang and Weidenbach
(S1 , U1 ) →(u2 ,([31,73])) (S3 , U3 ), where
S3 = {A, B, x1 ≥ 31, x1 ≤ 73, x2 > 5, x2 < 20} and U3 = {x1 , x2 },
which represents that the user has now additionally set x2 . State (S3 , U3 ) warrants rule tran-
sition r2 with the selection ([31, 73], [10, 19]). We get
(S3 , U3 ) →(r2 ,([31,73],[10,19])) (S4 , U4 ), where
S4 = {A, B, C, x1 ≥ 31, x1 ≤ 73, x2 ≥ 10, x2 ≤ 19, y1 = x1 · x2 } and U4 ≈ {x1 , x2 }.
Finally, there are more than one possible selections to enable rule transition r3 . If we choose
the selection ([50, 61], [12, 13]), we get
(S4 , U4 ) →(r3 ,([50,61],[12,13])) (S5 , U5 ), where
S5 = {A, B, C, ¬E, x1 ≥ 50, x1 ≤ 61, x2 ≥ 12, x2 ≤ 13, y1 ≈ x1 · x2 } and U5 = {x1 , x2 }.
Again, note that all selections given in this example are maximal in the sense that they are
not subselections of any other selections with the same properties demanded in the definition
of transitions and rule-terminal states.
3 Algorithms
The algorithm buildInterpretation, Algorithm 1, computes an abstract partial interpreta-
tion according to Definition 16 of an admissible specification if it exists. It takes an admissible
specification S+ and computes the components VS+ and TS+ of a possible interpretation of
S+ , named V and T in the algorithm. It aborts and returns “inconsistent” if it encounters
an inconsistent state, which means the specification is inconsistent. Otherwise, it returns the
resulting state graph G = (V, T ) that can serve as the basis for further analyses of the properties
of the specification and thus of the modeled configuration system.
A central element is the computation of selections, that is, integer intervals as defined in
the semantics (Definition 5). Since the intervals represent valuations of bounded user variables,
as explained in the previous section, this task is decidable and can be carried out in the most
naive way by enumerating the finitely many possibilities. A more efficient alternative to this is
an appropriate use of interval arithmetic [11]. In this paper, we restrict ourselves to assuming
that selections relevant to transitions as defined in the semantics (Definitions 10, 11 and 13)
are available in the form of maxSelections S+ , given a state and a transition.
Definition 21. Let (S, U ) be a state, and Λ ∧ F ; E ∈ (TU ∪ TR ) be a transition. Then
maxSelections S+ (S, U, Λ ∧ F ; E) is the set of all maximal selections γ with respect to (S, U )
and Λ ∧ F ; E.
buildInterpretation starts with the initial state of the input specification, as shown by
the initialization of N , which is the set of states not yet processed by the algorithm. The set
H stores all the states that the algorithm has computed so far. The algorithm runs as long as
there are states to be processed (line 5). In each iteration, consistency of the current state is
checked (line 7) first, using an external solver, according to the same consistency criterion as
stated in the transition semantics (Definitions 10 and 13). The algorithm stops if the state is
not consistent, otherwise it continues. Then, for each suitable maximal selection with respect
to the current state and a rule transition, a new state is computed according to /R (line 11).
The new transition is registered in line 12. If the new state differs from the current one, the
current selection is one of the selections under which the state is truly changed, and these are
collected in a set Γ (line 14). Also, if the newly generated state has not appeared before, it is
added to V , H and N (lines 15-18). This makes sure that we do not process states more than
once.
11
46
A Dynamic Logic for Configuration Tang and Weidenbach
After that, the user transitions with respect to the current state are investigated. If Γ = {()}
(check in line 19), it means that there has been a selection, namely (), that changes the state
with the set of user variables being empty (Definition 5). This means the state is not rule-
terminal in any case by Definition 11. If this is not the case, it is checked if the current state
is rule-terminal with respect to any selections. Given the current maximal selection γ with
respect to the current state and current user transition, and the set Γ of all selections where
rule transitions alter the state, reduceSelection (Algorithm 2) is used to find all rule-terminal
subselections of γ (line 22). The subselections γ 0 returned by reduceSelection that are sound
and complete (Theorem 22), have the following property, as explained further below: If γ 0 does
not include an empty interval or γ 0 is the empty selection (), then the current state is rule-
terminal with respect to γ 0 and the current user transition (line 23). buildInterpretation
then creates a new state with γ 0 and does the same steps as in the case of rule transitions. At
the end of the while loop, we remove the current state from the set N of states to be processed
(line 33). Provided that the algorithm has not encountered an inconsistent state, it returns V
and T , which are the components of every interpretation and, in particular, every model of the
consistent specification.
We give an overview on the recursive algorithm reduceSelection in the following. It
takes as arguments a selection γ and a set Γ of selections of the same length, and it returns
a set of selections ∆ such that all elements of ∆ are (1) subselections of γ and (2) have only
empty intersections with the selections in Γ. In addition, each selection δ ∈ ∆ is maximal
in the sense that there is no other selection δ 0 with δ ⊂ δ 0 and that fulfills (1) and (2). The
basic idea is that, in each recursive step, γ is reduced to a subselection so that it just about
has an empty intersection with one selection γ 0 from Γ. That selection γ 0 is removed from Γ
for the next recursion step, and once Γ has become empty, we get a reduced γ that has the
above properties. This is why the current γ in line 2 is returned as a singleton. If Γ is not
empty, we keep removing selections γ 0 from Γ until we have removed everything or we have
found a selection γ 0 that has a non-empty intersection with the current γ (lines 3 to 7). Again,
reduceSelection returns {γ} if it turns out that it has no non-empty intersections with the
rest of Γ (line 9). If we now assume we have found a γ 0 with non-empty intersection with γ,
the next step is to reduce γ so that there is an empty intersection. There is potentially more
than one possibility to do the reduction. At each position i of the |γ| positions, we consider
the difference γ(i) \ γ 0 (i) (line 12) and replace γ(i) with that difference, thus making γ having
an empty intersection with γ 0 . Another branching action can be required at this point: If
the set difference consists of two intervals that are not connected (line 13), which is the case
if min(γ) < min(γ 0 ) ≤ max (γ 0 ) < max (γ), then we consider two separate recursive calls of
reduceSelection with γ(i) being replaced by each one of the intervals respectively (line 14).
Otherwise, we simply replace γ(i) with the difference (line 16) in one recursive call. We collect
all the possible solutions into a result set R.
Theorem 22 says that the use of reduceSelection(γ, Γ) in line 22 of buildInterpreta-
tion gives us the correct rule-terminal subselections as defined in the semantics in a complete
way. Note that the results of reduceSelection can include “extra” subselections that have
been so much reduced from γ that they contain empty components. These selections are dis-
carded by buildInterpretation because they are no longer selections with respect to the
current state and user transition (line 23). The case γ 0 = () means that there are no user
variables (Definition 5) and that Γ = ∅, since otherwise Γ = {()}, which is not the case
(line 19). Consequently, reduceSelection immediately returns {()}, a singleton containing
a rule-terminal selection.
Theorem 22. Let γ be a maximal selection with respect to a state (S, U ) and a user transition
12
47
A Dynamic Logic for Configuration Tang and Weidenbach
Algorithm 1: buildInterpretation(S+ )
1 N := {(SI , UI )}
2 H := {(SI , UI )}
3 V := {(SI , UI )}
4 T := ∅
5 while N 6= ∅ do
6 let (S, U ) ∈ N
7 if ∀~xu ∃~y S|U → (S \ S|U ) ∪ C is satisfiable then
8 Γ := ∅
9 for each Λi ∧ Fi ; Ei ∈ TR do
10 for each γ ∈ maxSelections S+ (S, U, Λi ∧ Fi ; Ei ) do
11 (S 0 , U 0 ) := (S, U ) /R (Ei , γ)
12 T := T ∪ {((S, U ), i, γ, (S 0 , U 0 ))}
13 if (S 0 , U 0 ) 6= (S, U ) then
14 Γ := Γ ∪ {γ}
15 if (S 0 , U 0 ) 6∈ H then
16 V := V ∪ {(S 0 , U 0 )}
17 H := H ∪ {(S 0 , U 0 )}
18 N := N ∪ {(S 0 , U 0 )}
19 if Γ 6= {()} then
20 for each Λi ∧ Fi ; Ei ∈ TU do
21 for each γ ∈ maxSelections S+ (S, U, Λi ∧ Fi ; Ei ) do
22 for each γ 0 ∈ reduceSelection(γ, Γ) do
23 if γ 0 (j) 6= ∅ for all j or γ 0 = () then
24 (S 0 , U 0 ) := (S, U ) /U (Ei , γ 0 )
25 T := T ∪ {((S, U ), i, γ 0 , (S 0 , U 0 ))}
26 if (S 0 , U 0 ) 6= (S, U ) then
27 if (S 0 , U 0 ) 6∈ H then
28 V := V ∪ {(S 0 , U 0 )}
29 H := H ∪ {(S 0 , U 0 )}
30 N := N ∪ {(S 0 , U 0 )}
31 else
32 return inconsistent
33 N := N \ {(S, U )}
34 return (V, T )
Λ∧F ; E ∈ TU . A selection γ ∗ with γ ∗ ⊆ γ and γ ∗ (i) 6= ∅ for all i is a rule-terminal subselection
of γ if and only if γ ∗ ∈ reduceSelection(γ, Γ), where Γ is the set of all selections γ 0 such
that γ 0 is a maximal selection with respect to (S, U ) and a rule transition Λ0 ∧ F 0 ; E 0 ∈ TR
with (S, U ) 6= (S, U ) /R (E 0 , γ 0 ).
Proof. (Idea) Using associativity of set differences, the fact that all selections occurring as the
first argument in reduceSelection are subselections of the input selection γ and induction
over the recursion depth.
Apparently, each state computed by buildInterpretation implies a path of transitions as
indicated by the set T in the algorithm. It is easy to see they are analogous to the paths defined
13
48
A Dynamic Logic for Configuration Tang and Weidenbach
Algorithm 2: reduceSelection(γ, Γ)
1 if Γ = ∅ then
2 return {γ}
0
3 let γ ∈ Γ
0
4 Γ := Γ \ {γ }
0
5 while Γ 6= ∅ and γ ∩ γ = ∅ do
0
6 let γ ∈ Γ
7 Γ := Γ \ {γ 0 }
0
8 if γ ∩ γ = ∅ then
9 return {γ}
10 R := ∅
11 for i = 1 to |γ| do
12 s := γ(i) \ γ 0 (i)
13 if s = I1 ∪ I2 , I1 , I2 intervals and I1 ∩ I2 = ∅ then
14 R := R ∪ reduceSelection(γ[i/I1 ], Γ) ∪ reduceSelection(γ[i/I2 ], Γ)
15 else
16 R := R ∪ reduceSelection(γ[i/s], Γ)
17 return R
in the semantics in Definition 14. Theorem 23 then says buildInterpretation is sound and
complete with respect to the semantics of PIDL+.
Theorem 23. Let S+ = (Π, X, SI , UI , C, TU , TR ) be an admissible specification. A state
(S, U ) is reachable from the initial state (SI , UI ) via a path τ if and only if (S, U ) ∈ V
and we have a sequence ((S0 , U0 ), i1 , γ1 , (S1 , U1 )), . . . , ((Sn−1 , Un−1 ), in , γn , (Sn , Un )), where
((Sj−1 , Uj−1 ), ij , γj , (Sj , Uj )) ∈ T and τ (j) = (ij , γj ) for all j = 1, . . . , n, |τ | = n, (S0 , U0 ) =
(SI , UI ), (Sn , Un ) = (S, U ) and buildInterpretation(S+ ) = (V, T ).
Proof. (Idea) By induction over the length of the path τ .
4 Conclusions
We have presented PIDL+, a logic suited for formalizing configuration systems whose dynamics
stem from the effects of user interaction and rule actions. Boolean variables and arithmetic
expressions of the configurations are considered. The choice of polynomials is motivated by the
real-world systems we have already investigated for the design of PIDL+. Of course, PIDL+
can be extended to other suitable choices of closed arithmetic expressions. What distinguishes
PIDL+ from similar logics is that it takes the characteristic features of such configuration
systems into account by incorporating two types of transitions and the notion of rule-terminal
states. This, in principle, forms the basis for a systematic analysis of the whole configuration
process, making an a priori verification of those systems possible. Natural next steps include the
implementation of the shown decision procedures and conducting corresponding experiments
on real-world data. Related to that is the development and implementation of further decision
procedures to investigate properties of interests of configuration systems, as we have done in
the case of PIDL [9].
14
49
A Dynamic Logic for Configuration Tang and Weidenbach
References
[1] Jérôme Amilhastre, Hélène Fargier, and Pierre Marquis. Consistency restoration and explanations
in dynamic csps application to configuration. Artif. Intell., 135(1-2):199–234, 2002.
[2] Philippe Balbiani, Andreas Herzig, and Nicolas Troquard. Dynamic logic of propositional as-
signments: A well-behaved variant of PDL. In 28th Annual ACM/IEEE Symposium on Logic in
Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 143–152, 2013.
[3] Razieh Behjati and Shiva Nejati. Interactive configuration verification using constraint program-
ming. Lyon, France, 2014.
[4] Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using
branching-time temporal logic. In Logic of Programs, Workshop, pages 52–71, London, UK, UK,
1982. Springer-Verlag.
[5] Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. MIT Press, Cambridge,
MA, USA, 1999.
[6] Andreas Classen, Patrick Heymans, Pierre-Yves Schobbens, Axel Legay, and Jean-François Raskin.
Model checking lots of systems: efficient verification of temporal properties in software product
lines. In Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering -
Volume 1, ICSE 2010, Cape Town, South Africa, 1-8 May 2010, pages 335–344, 2010.
[7] K. Czarnecki and A. Wasowski. Feature diagrams and logics: There and back again. In Software
Product Lines, 11th International Conference, SPLC 2007, Kyoto, Japan, September 10-14, 2007,
Proceedings, pages 23–34. IEEE Computer Society, 2007.
[8] Deepak Dhungana, Paul Grünbacher, and Rick Rabiser. The DOPLER meta-tool for decision-
oriented variability modeling: a multiple case study. Autom. Softw. Eng., 18(1):77–114, 2011.
[9] Deepak Dhungana, Ching Hoo Tang, Christoph Weidenbach, and Patrick Wischnewski. Auto-
mated verification of interactive rule-based configuration systems. In 28th IEEE/ACM Interna-
tional Conference on Automated Software Engineering, ASE 2013, pages 551–561. IEEE Digital
Library, 2013.
[10] Michael J. Fischer and Richard E. Ladner. Propositional dynamic logic of regular programs. J.
Comput. Syst. Sci., 18(2):194–211, 1979.
[11] Martin Fränzle, Christian Herde, Tino Teige, Stefan Ratschan, and Tobias Schubert. Efficient
solving of large non-linear arithmetic constraint systems with complex boolean structure. Journal
on Satisfiability, Boolean Modeling, and Computation, 1:209–236, 2007.
[12] Paul Harrenstein, Wiebe van der Hoek, John-Jules Ch. Meyer, and Cees Witteveen. Boolean
games. In Proceedings of the Eight Conference on Theoretical Aspects of Rationality and Knowl-
edge, pages 287–298, 2001.
[13] Kyo Kang, Sholom Cohen, James Hess, William Novak, and A. Peterson. Feature-oriented domain
analysis (foda) feasibility study. Technical Report CMU/SEI-90-TR-021, Software Engineering
Institute, Carnegie Mellon University, Pittsburgh, PA, 1990.
[14] Martin J. Osborne and Ariel Rubinstein. A Course in Game Theory. The MIT Press, Cambridge,
USA, 1994. electronic edition.
[15] Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of
Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pages 46–57.
IEEE Computer Society, 1977.
[16] Marcello La Rosa, Wil M. P. van der Aalst, Marlon Dumas, and Arthur H. M. ter Hofstede.
Questionnaire-based variability modeling for system configuration. Software and System Modeling,
8(2):251–274, 2009.
[17] Paolo Turrini. Endogenous boolean games. In IJCAI 2013, Proceedings of the 23rd International
Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013, 2013.
15
50