We define the new dynamic logic PIDL+ that extends our previously developed logic PIDL (Propositional 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.
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
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-andtransitions 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
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 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 expected, intersection of a tuple t = (I1, . . . , In) with another t0 = (I10, . . . , In0) is defined componentwise: 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
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 (
∀~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 , (
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 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. (
V x ≥ cx1 ∧ x ≤ cx2 ∧ V 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 (
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 Φ. 2.3
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: (
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. 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: (
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 (
U 0 := S0 :=
U \ varl (E), {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 S0. 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 S0 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 S0. 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 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 S0 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 (S0, 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 appropriate 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 (S0, U 0) with respect to a rule transition Λi ∧ Fi ; Ei ∈ TR and a selection γ is written as
(S, U ) →(i,γ) (S0, U 0),
where (
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 . (
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.
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
(
User transitions are then defined analogously to rule transitions, with respect to ruleterminal states.
Definition 13. A user transition from a state (S, U ) to a state (S0, U 0) with respect to a user transition Λi ∧ Fi ; Ei ∈ TU and a selection γ is written as
(S, U ) →(i,γ) (S0, U 0),
where (
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 (S0, 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) = (S0, U 0). Definition 15. A state (S0, U 0) is reachable from a state (S, U ) if there is a path from (S, U ) to (S0, 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 (
(S, U ) →(i,γ) (S0, U 0), Λi ∧ Fi ; Ei ∈ (TU ∪ TR)}, and
(
Note that indeed (SI , UI ) ∈ VS+ according to our definition of reachability. An interpretation 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+.
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 buildInterpretation, 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 specifications 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 specification S+ are finite. Soundness and completeness are decidable.
Π = {A, B, C, D, E}, X = {x1, x2, y1}, SI = UI = {¬A}, ∅, 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 maximal 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 (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 transition 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
The algorithm buildInterpretation, Algorithm 1, computes an abstract partial interpretation 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 maxSelectionsS+ , given a state and a transition. Definition 21. Let (S, U ) be a state, and Λ ∧ F ; E ∈ (TU ∪ TR) be a transition. Then maxSelectionsS+ (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.
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 ruleterminal 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 ruleterminal 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 (
Theorem 22 says that the use of reduceSelection(γ, Γ) in line 22 of buildInterpretation 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 discarded 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 Algorithm 1: buildInterpretation(S+) Λ∧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 ; E0 ∈ TR with (S, U ) 6= (S, U ) /R (E0, γ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 Algorithm 2: reduceSelection(γ, Γ) 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 ).
4
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].