We devise a general framework for formalizing Dynamic Systems centered around a Description Logic knowledge base. Our framework is parametric w.r.t. both the description logic and the progression mechanism. For such kinds of systems, we provide general decidability results for verification and adversarial synthesis of first-order -calculus properties under a natural assumption which we call “state-boundedness”. We then apply such results to the case of DL-Lite and ALCQIknowledge bases and a progression mechanism grounded in epistemic first-order queries.
Integrating semantic mechanisms like Description Logics (DLs), to describe static
knowledge, and full-fledged mechanisms like transition systems, to describe dynamics
is of great interest, especially in the context of a semantic view of data-aware and
artifact-based processes [
Recently, to overcome such difficulties, a looser coupling of the static and dynamic
representation mechanisms has been proposed, giving rise to a rich body of research
[
In this paper, we follow this approach and devise a general framework for DL Based
Dynamic Systems, which is parametric w.r.t. the DL used for the knowledge base and
the mechanism used for progressing the state of the system. Using this framework, we
study verification and (adversarial) synthesis for specifications expressed in a variant of
first-order -calculus, with a controlled form of quantification across successive states.
We recall that -calculus subsumes virtually all logics used in verification, including
LTL, CTL and CTL . Adversarial synthesis for -calculus captures a wide variety of
synthesis problems, including conditional planning with full-observability [
We provide key decidability results for verification under a “bounded-state”
assumption. Such assumption states that while progressing, the system can change arbitrarily
the stored individuals but their total number at each time point cannot exceed a certain
bound. Notice that along an infinite run (and hence in the overall transition system),
the total numer of individuals can still be infinite. We then turn to adversarial synthesis,
where we consider the system engaged in a sort of game with an adversarial environment.
The two agents (the system and the environment) move in alternation, and the problem is
to synthesize a strategy for the system to force the evolution of the game so as to satisfy
a given synthesis specification. Such a specification is expressed in the above first-order
-calculus, using the temporal operators to express that the system is able to force a
formula in the next state regardless of the environment moves, as in the strategy logic
ATL [
The rest of the paper is organized as follows. In Section 2 we introduce the general
framework of DL Based Dynamic Systems, and in Section 3, the verification formalism,
based on first-order -calculus with a controlled form of quantification across states.
In Section 4, we show the general decidability result of model checking such a variant
of -calculus against DL Based Dynamic Systems. In Section 5, we show decidability
of adversarial synthesis in our setting. In Section 6, we study the instantiation of the
framework in which the DL knowledge base is expressed in DL-Lite or ALCQI, and
the progression mechanism is that of [
In this paper we follow Leveque’s functional approach [
DL knowledge bases. A (DL) knowledge base (KB) (T; A) is constituted by a TBox T representing the intensional knowledge about the domain of interest in terms of concepts and roles, and an ABox A representing extensional knowledge about individuals. The TBox T is a finite set of universal assertions (we don’t allow nominals, to avoid confusion between intensional and extensional levels). The ABox A is a finite set of assertions consisting of facts, i.e., atomic formulas of the form N (d) and P (d; d0), where N is a concept name, P is a role name (we use binary roles, but all our results can be extended to n-ary relations), and d, d0 are individual constants in . We use ADOM(A) to denote the set of constants actually appearing in A. We adopt the standard DL semantics based on first-order interpretations and on the notion of (first-order) model. Naturally, the only TBoxes of interest for us are those that are satisfiable, i.e., admit at least one model. We say that an ABox A is consistent w.r.t. a TBox T if (T; A) is satisfiable, and that (T; A) logically implies an ABox assertion , denoted (T; A) j= , if every model of (T; A) is also a model of . As usual in DLs, we assume that reasoning, i.e., checking KB satisfiability and logical implication are decidable tasks.
Description Logic based Dynamic Systems. A Description Logic based Dynamic System (DLDS) is a tuple S = (T; A0; ), where (T; A0) is a KB and is a finite set of actions. The set ADOM(A0) of constants in A0 are called distinguished and we denoted them by C, i.e., C = ADOM(A0). Such constants play a special role because they are the only ones that can be used in verification formulas (see Section 4). Actions are parametrized, and when an action is executed formal parameters are substituted with individual constants from . Formal parameters are taken from a countably infinite set P of parameter names. Interestingly, we do not assume that the number of formal parameters of an action is fixed a priory, but we allow it to depend on the KB (actually, the ABox, since the TBox is fixed) on which the action is executed.
Notice that this mechanism is more general than what typically found in procedures/functions of programming languages, where the number of parameters is fixed by the signature of the procedure/function. Our mechanism is directly inspired by web systems, in which input forms are dynamically constructed and customized depending on data already acquired. For example, when inserting author data in a conference submission system, the input fields that are presented to the user depend on the (previously specified) number of authors.
Once formal parameters are substituted by actual ones, executing the action has the effect of generating a new ABox. We use AT to denote the set of all ABoxes that can be constructed using concept and role names in T , and individuals in . Formally, each action in has the form ( ; ), where – : AT ! 2P is a parameter selection function that, given an ABox A, returns the finite set (A) P of parameters of interest for w.r.t. A (see below); – : AT P 7! AT , is a (partial) effect function that, given an ABox A and a parameter assignment m : (A) ! , returns (if defined) the ABox A0 = (A; m), which (i) is consistent wrt T , and (ii) contains only constants in ADOM(A)[ IM(m).3 3 By IM( ) we denote the image of a function.
Observe that since (A) is finite, so is IM(m), thus only finitely many new individuals, w.r.t. A, can be added to A0.
In fact, we focus our attention on DLDS’s that are generic, which intuitively means that the two functions constituting an action are invariant w.r.t. renaming of individuals4. Genericity is a natural assumption that essentially says that the properties of individuals are only those that can be inferred from the KB.
To capture genericity, we first introduce the notion of equivalence of ABoxes modulo renaming. Specifically, given two ABoxes A1, A2, sets S1 ADOM(A1) [ C and S2 ADOM(A2) [ C, and a bijection h : S1 ! S2 that is the identity on C, we say that A1 and A2 are logically equivalent modulo renaming h w.r.t. a TBox T , written A1 =hT A2, if: 1. for each assertion 1 in A1, (T ; A2) j= h( 1); 2. for each assertion 2 in A2, (T ; A1) j= h 1( 2); where h( 1) (resp. h 1( 2)) is a new assertion obtained from 1 (resp., 2), by replacing each occurrence of an individual d 2 with h(d) (resp., h 1(d)). We say that A1 and A2 are logically equivalent modulo renaming w.r.t. T , written A1 =T A2, if A1 =hT A2 for some h. We omit T when clear from the context.
A DLDS S = (T ; A0; ) is generic, if for every ( ; ) 2 and every A1; A2 2 AT s.t. A1 =T A2, we have that (i) (A1) = (A2), and (ii) for every two parameter assignments m1 : (A1) ! and m2 : (A2) ! , if there exists a bijection h : ADOM(A1) [ C [ IM(m1) ! ADOM(A2) [ C [ IM(m2) s.t. A1 =hT A2, then, whenever A01 = (A1; m1) is defined then also A02 = (A2; m2) is defined and viceversa, and moreover A01 =hT A02.
DLDS Transition System. The dynamics of a DLDS S is characterized by the transition system S it generates. The kind of transition systems we consider here have the general form = (U; T ; ; s0; abox ; )), where: (i) U is the universe of individual constants, which includes the distinguished constants C; (ii) T is a TBox; (iii) is a set of states; (iv) s0 2 is the initial state; (v) abox is a function that, given a state s 2 , returns an ABox associated with s, which has terms of as individuals, and which conforms to T ; (vi) ) L is a labeled transition relation between states, where L is the set of labels.
With a little abuse of notation we also introduce an unlabeled transition relation )
obtained from the labeled transition relation by projecting out the labels (we use
this notion when dealing with verification properties). Given a DLDS S = (T ; A0; ),
its (generated) transition system S = (U; T ; ; s0; abox ; )) is defined as: (i) U = ;
(ii) abox is the identity function (thus AT ); (iii) s0 = A0; (iv) ) L is
a labeled transition relation where L = M, with M the domain of action parameter
assignments, is a set of labels containing one pair (a; m) for every action a 2 and
corresponding parameter assignment m 2 M; (v) and ) are defined by mutual
induction as the smallest sets satisfying the following property: if A 2 then for every
( ; ) 2 , m : (A) ! , and A0 2 AT , s.t. A0 = (A; m), we have A0 2 and
`
A ) A0, s.t. ` = (( ; ); m).
4 This name is due to the notion of genericity in databases [
DLp
To specify dynamic properties over DLDSs, we use a first-order variant of -calculus
[
In our variant of -calculus, we allow local properties to be expressed as queries in
any language for which query entailment for DL KBs is decidable [
At the same time we allow for a controlled form of first-order quantification across
states, inspired by [
j
LIVE(x) ^ h i j LIVE(x) ^ [ ] j Z j Z: where Q is a (possibly open) query as described above, in which the only constants that may appear are those in C, Z is a second order predicate variable (of arity 0), and, with a slight abuse of notation, we write LIVE(x1; : : : ; xn) = Vi2f1;:::;ng LIVE(xi). For DLp, the following assumption holds: in LIVE(x) ^ h i and LIVE(x) ^ [ ] , the variables x are exactly the free variables of , once we substitute to each bounded predicate variable Z in its bounding formula Z: 0. We use the usual abbreviations, including: LIVE(x) ! h i = :(LIVE(x) ^ [ ]: ) and LIVE(x) ! [ ] = :(LIVE(x) ^ h i: ). Intuitively, the use of LIVE( ) in DLp ensures that individuals are only considered if they persist along the system evolution, while the evaluation of a formula with individuals that are not present in the current database trivially leads to false or true.
The formula Z: denotes the least fixpoint of the formula (seen as the predicate transformer Z: ). As usual in -calculus, formulae of the form Z: must obey to the syntactic monotonicity of w.r.t. Z, which states that every occurrence of the variable Z in must be within the scope of an even number of negation symbols. This ensures that the least fixpoint Z: always exists.
The semantics of DLp formulae is defined over possibly infinite transition systems of the form (U; T; ; s0; abox ; )) seen above. Since DLp also contains formulae with both individual and predicate free variables, given a transition system , we introduce
(Q)v;V = fs 2 j (T ; abox (s)) j= Qvg (: )v;V = n ( )v;V ( 1 ^ 2)v;V = ( 1)v;V \ ( 2)v;V (9x:LIVE(x) ^ )v;V = fs 2 j 9d 2 ADOM(abox (s)):s 2 ( )v[x=d];V g (LIVE(x) ^ h i )v;V = fs 2 j x=d 2 v implies d ADOM(abox (s))
and 9s0:s ) s0 and s0 2 ( )v;V g (LIVE(x) ^ [ ] )v;V = fs 2 j x=d 2 v implies d ADOM(abox (s))
and 8s0:s ) s0 implies s0 2 ( )v;V g (Z)v;V = V (Z) ( Z: )v;V = TfE j ( )v;V [Z=E] E g an individual variable valuation v, i.e., a mapping from individual variables x to U , and a predicate variable valuation V , i.e., a mapping from the predicate variables Z to subsets of . With these three notions in place, we assign meaning to formulae by associating to , v, and V an extension function ( )v;V , which maps formulae to subsets of . Formally, the extension function ( )v;V is defined inductively as shown in Figure 1. Intuitively, ( )v;V assigns to such constructs the following meaning. (i) The boolean connectives have the expected meaning. (ii) The quantification of individuals is done over the individuals of the “current” ABox, using the special LIVE( ) predicate (active domain quantification). Notice that such individuals can be referred in a later state, provided that they persist in between (see below). (iii) The extension of h i consists of the states s s.t.: for some successor state s0 of s, holds in s0 under v. (iv) The extension of Z: is the smallest subset E of s.t., assigning to Z the extension E , the resulting extension of (under v) is contained in E . That is, the extension of Z: is the least fixpoint of the operator ( )v;V [Z=E], where V [Z=E ] denotes the predicate valuation obtained from
h s2, if there exists a persistence preserving bisimulation B between 1 and 2 such that (s1; h; s2) 2 B. A transition system 1 is persistence preserving bisimilar to 2, written 1 2, if there exists a partial bijection h0 and a persistence preserving bisimulation B between 1 and 2 s.t. (s01; h0; s02) 2 B. A suitable bisimulation-invariance theorem hold:
DLp closed formula , we have that 1 j= if and only if 2 j= .
The proof follows the line of an analogous one in [
Next we focus on checking a DLp formula against a DLDS. It is easy to show, by
reduction from the halting problem, that this is in general undecidable, even under the
assumption of genericity (see, e.g., [
Undecidability calls for the identification of decidable classes of the problem. To this end, we focus our attention on a particular class of DLDS, which we call state-bounded. Under the assumption of genericity, we are able to prove decidability of verification for state-bounded DLDS. A state-bounded DLDS K is one for which there exists a finite bound b s.t., for each state s of K, jADOM(abox (s))j < b. When this is the case, we say that K is b-bounded. Observe that state-bounded DLDS contain in general infinitely many states, and that a DLDS K can be state-unbounded even if, for every state s of
K, jADOM(abox (s))j is finite (but not bounded). W.l.o.g., for state-bounded DLDS, we assume that the maximum number n of parameters that actions may request is known.5
We prove now that model checking of DLp over state-bounded, generic DLDS
is decidable, by showing how it can be reduced to model checking of propositional
-calculus over finite-state transition systems. The crux of the proof, outlined below, is
the construction of a finite-state transition system KD s.t. KD K, where K is the
transition system generated by K. This is done through an abstraction technique inspired
by that of [
Observe that the infiniteness of K comes from that of , which yields a potential infinite number of ABoxes and assignments to action parameters, thus infinite branching. As a first step, we show that K can be “pruned”, so as to obtain a persistence-bisimilar finite-branching transition system K, and that any transition system obtained in this way is persistence-bisimilar to 5 This number can be obtained in PSPACE by constructing all the ABoxes of size b, up to logical equivalence modulo renaming, and by applying all actions to them, so as to obtain the corresponding parameters.
To define such prunings we introduce the notion of equality commitment, i.e., a set of equality constraints involving parameter assignments and distinguished individuals. An equality commitment over a finite set S [ P of individuals and parameters, is a partition H = fH1; : : : ; Hng of S, s.t. every Hi contains at most one d 2 . Given ( ; ) 2 , an ABox A, and an equality commitment H over ADOM(A) [ (A) [ C, a parameter assignment m : (A) ! respects H if, for every two parameters p1; p2 2 (A), m(p1) = m(p2) iff p1 and p2 belong to the same Hi 2 H , and m(p1) = m(p2) = d, iff d 2 Hi. Observe that, being S finite, the number of possible equality commitments over S, is finite, too.
A pruning of K is a transition system K = ( ; T ; ; s0; abox ; )), s.t.: (i) abox is the identity; (ii) s0 = A0 2 ; (iii) and ) are defined as smallest sets constructed by mutual induction from s0 as follows: if A 2 , then for every ( ; ) 2 and every equality commitment H over ADOM(A) [ (A) [ C, nondeterministically choose finitely many parameter assignments mi : (A) ! respecting H , and add transitions A )` A0 where A0 = (A; mi) and ` = (( ; ); mi).
Intuitively, a pruning is obtained from K, by executing, at each reachable state A, an arbitrary, though finite, set of instantiated actions. This set is required to cover and all the possible equality commitments over the parameters that the selected action requires. It can be seen that, since is finite and, for fixed A, only finitely many H exist, prunings have always finite branching, even if K does not. The following lemma says that, despite their structural differences, if K is generic, then K is preservation-bisimilar
Proof (sketch). By genericity, for an ABox A and an action ( ; ), if two parameter assignments m1; m2 : (A) ! respect the same equality commitment H on ADOM(A) [ (A) [ C, the applications of ( ; ) with m1 and m2, result in logically equivalent (modulo renaming) ABoxes, i.e., A1 = 1(A; m1) =hT A2 = 2(A; m2). Further, still by genericity, we have that ADOM(A)\ ADOM(A1) = ADOM(A)\ ADOM(A2), that is, A1 and A2 preserve the same values w.r.t. A. This can be taken as the basic step for constructing a persistence-preserving bisimulation between K and K, starting from the observation that A0 =T A0.
Prunings are in general infinite-state. An important question is whether there exists some that are finite-state and effectively computable. This, by Lemma 1, Th. 1, and the fact that verification is decidable for finite-state transition systems, would yield decidability of verification for K. While this is not the case in general (we already stated undecidability), we can prove that this holds on state-bounded, generic DLDS.
Given a b-bounded, generic DLDS, consider a finite set D of individual constants so.nt.lyDindividaunadlsCfromDD.Leint aKcDtiobne tphaerafrmagetmerenatssoifgtnrmanesnittiso. nSsuycshteam oKDfKisbfiunilitteusainndg effectively computable. We have the following result.
Lemma 2. If jDj b+n+jCj, then KD is a pruning of K.
Proof (sketch). The construction of KD essentially follows the inductive structure of the definition of pruning. In particular, since D is finite, only finitely many parameter assignments are considered at each step. It can be seen that, because D n, for every action application and corresponding equality commitment H, we can find a parameter assignment that respects H. Further, since D b + n we have enough individuals to construct, at each step, the successor state, containing at most b individuals, that results from the action application. Finally, genericity ensures that the particular choice of D, as long as containing C, does not affect, except for individual renaming, the behavior of the effect function .
Together, Lemma 1 and 2 imply the following decidability result:
able, and can be reduced to model checking of propositional -calculus over a finite-state
transition system, whose number of state is at most exponential in the size of K.
Proof (sketch). By Lemma 1, we know that KD is bisimilar to K. By Lemma 2,
we know that KD contains at most an exponential number of states in the size of the
specification K, which includes the initial ABox, thus the (finite) set of distinguished
constants C. Hence, by Theorem 1, we can check formulae over the finite transition
system KD instead of K. Since the number of objects present in KD is finite, DLp
formulae can be propositionalized and checked through standard algorithms [
We turn now to the problem of adversarial synthesis, i.e., we consider a setting in
which two agents act in turn as adversaries. The first agent, called environment, acts
autonomously, whereas we control the second agent, called system. The joint behavior of
the two agents gives rise to a so-called two-player game structure (2GS) [
We can deal with adversarial synthesis in our framework by building a 2GS in which we encode explicitly in the DL KB the alternation of the moves of the two players. Specifically, we introduce a fresh concept name Turn and two fresh distinguished constants te and ts, whose (mutual exclusive) presence in Turn indicates which of the two players will move next. We denote with AeT the set of ABoxes in AT that contain Turn(e) (and not Turn(s)). Similarly, for AsT .
A DL based 2GS (DL2GS) is a DLDS K = (T; A0; ), where Turn(e) 2 A0 and the set of actions is partitioned into a set e of environment actions and a set s of system actions. The effect function of each environment action is defined only for ABoxes in e and brings about an ABox in s. Symmetrically, the effect function of each system action is defined only for ABoxes in s and brings about an ABox in e. In this way we achieve the desired alternation of environment and system moves: starting from the initial state, the environment moves arbitrarily and the system suitably responds to the environment move, and this is repeated (possibly forever).
Logics of interest for 2GSs are temporal logics in the style of ATL [
Z: j
Z: j 9x:LIVE(x) ^ LIVE(x) ^ [h i]s LIVE(x) ^ [h i]w j 8x:LIVE(x) !
j j LIVE(x) ! [h i]s j LIVE(x) ! [h i]w j where [h i]s stands for [ ](LIVE(x) ^ h i ), and [h i]w stands for [ ](LIVE(x) ! h i ). Technically, ADLp is a fragment of DLp, where negation normal form is enforced, i.e., negation is pushed inwards so that it appears only in front of atoms (in our case, queries Q). Intuitively, both [h i]s and [h i]w mean that the system can force to hold, i.e., for every (environment) move there is a (system) move leading to . The difference between the two is that [h i]s precludes the environment from dropping objects existing before its move, while [h i]w does not.
As an immediate consequence of Theorem 2 we have:
able.
We are not only interested in verifying ADLp formulas, but also in synthesizing
strategies to actually fulfill them. A strategy is a partial function f : (AeT AsT ) AeT 7!
s M where M is the domain of action parameter assignments, such that for every
history = Ae0; As0 Aen; Asn; Aen+1, it is the case that Ais = f( [i])(Aie; mf( [i]))
where [i] is prefix of of length i, and mf( [i]) : f( [i])(Aie) ! , and symmetrically
Aie+1 = (Ais; m) for some m : (Ais) ! . We say that a strategy f is winning
if by resolving the existential choice in evaluating the formulas of the form [h i]s
and [h i]w according to f , the goal formula is satisfied. Notably, model checking
algorithms provide a witness of the checked property [
and a ADLp formula , realizes a concrete strategy to force .
Proof (sketch). The algorithm iterates over three steps: (i) matching of the current concrete history with an abstract history over which f is defined; (ii) extraction of the action and corresponding abstract parameter assignment; (iii) concretization of the obtained parameter assignment. The first step requires building a family of functions, in fact bijections, that transform each pair of consecutive states of the concrete history, into a pair of abstract successor states, so as to satisfy the same equality commitments at the abstract and at the concrete level, and to guarantee that f is defined over the obtained abstract history . This can be done as both and the abstract DL2GS contain, by state boundedness, only finitely many distinct elements, thus only finitely many such functions exist. The existence of is guaranteed by the bisimilarity, induced, in turn, by genericity. By applying f to the abstract history , we extract the action ( ; ) and abstract parameter assignment m to execute next, in the abstract game, i.e., (( ; ); m) = f ( ). Finally, in order to concretize m, it is sufficient to reconstruct the equality commitment H enforced by m and the bijection over the last pairs of states of and , and then replacing the abstract values assigned by m with concrete ones, arbitrarily chosen, so as to satisfy H . By genericity, for any such choice, we obtain an action executable at the concrete level, after , and that is compatible with (at least) one strategy of the family defined by f . In this way, at every step, the system is presented a set of choices, namely one per possible concretization of the abstract assignment, that can thus be resolved based on information available at runtime.
Theorem 4 and its proof give us an effective method for actually synthesizing strategies to force the desired property. Obviously, optimizations for practical efficiency (which are out of the scope of this paper) require further study. 6
As a concrete instantiation of the abstract framework introduced in Section 2, we consider
a variant of Knowledge and Action Bases (KABs) [
An action 2 Act modifies the current ABox A by adding or deleting assertions,
thus generating a new ABox A0. consists of a set fe1; : : : ; eng of effects, that take
place simultaneously. An effect ei has the form Qi A0i, where
– Qi is an ECQ, i.e., a domain independent first-order query whose atoms represent
certain answers of unions of conjunctive queries (UCQs) [
Given an action 2 Act , we can capture its execution by defining an action ( ; ) as follows: – (A) returns the ground Skolem terms obtained by executing the queries Qi of the effects over (T; A), instantiating the facts A0i using the returned answers, and extracting the (ground) Skolem terms occurring therein. – (A; m) returns the ABox obtained by executing over (T; A) the queries Qi of the effects, instantiating the facts A0i using the returned answers, and assigning to the (ground) Skolem terms occurring therein values according to a freely chosen parameter assignment m, as long as such an ABox is consistent with T . If the ABox is not consistent with T , then (A; m) is undefined.
In this way, we can define from Act , and hence the DLDS S = (T; A0; ) corresponding to the KAB K = (T; A0; Act ). Notice that, being the parameter assignment freely chosen, the resulting DLDS is actually generic.
In this context, we use ECQs also as the query language for the local properties in the verification and synthesis formalism. Now observe that if the TBox is expressed in a lightweight DL of the DL-Lite family, answering ECQ queries is PSPACE-complete in combined complexity (and in AC0 in data complexity, i.e., the complexity measured in the size of the ABox only). The same complexity bounds hold for the construction of (A) and (A; m), and hence, under the assumption of state-boundedness, the abstract transition system generated by S can be constructed in EXPTIME. It follows that both verification and synthesis can be done in EXPTIME.
Instead, if the TBox is expressed in an expressive DL such as ALCQI, the cost that dominates the construction of the abstract transition system is the 2EXPTIME cost of answering over (T; A) the UCQs that are the atoms of the EQL queries in the actions. Finally, if instead of using as atoms UCQs, we use atomic concepts and roles (i.e., we do instance checking), the cost of query evaluation drops to EXPTIME, and so does the cost of building the abstract transition system.
These results can be extended to other DLs as long as they do not include nominals, given that the presence of nominals blurs the distinction between the extensional and the intensional knowledge, and hence requires more careful handling. 7
This work complements and generalizes two previous papers focussing on forms of
verification on DL-based dynamics. One is [