Our digital world is characterized by various concurrent processes that interact with the physical world. Each of them follows its own rules and goals and only few of them are under a central control. While usually a human mediates between these processes, we developed the SHIP-tool to orchestrate these processes automatically. It uses Description Logic to represent a current state, which is constantly updated by messages sent by sensors and other processes. Temporal-logical formulas act as monitors that supervise the evolution of the system. The failure or success of monitors can initiate procedures given as programs on actions and speci ed in a Dynamic Logic. In this paper we describe in particular the aspect of storing and maintaining the state of the system in Description Logic ontologies. We formulate restrictions on ABoxes and their updates to always ensure a constructive speci cation of the current state while keeping the general rules of the system (i.e the TBox and RBOX) invariant.
While independently developed computer systems obtain more and more the ability to communicate with each other on a technical level, there is an upcoming need to orchestrate and combine the processes performed by these systems on an operational or work- ow level. In the past, typically humans were responsible to supervise the processes and to translate and exchange important information between them. The SHIP-Tool is an attempt to automate this task and is based on an abstract (logic) symbolic representation of an actual situation, the ways the processes can change a situation, and the expectations of future developments in a situation.
It provides an implementation, execution and simulation platform for workow processes allowing the user to integrate and monitor existing devices, services or even entire systems. This is achieved by providing a logical formalism to describe the real world in an abstract way. Changes in the real world are communicated to the tool in terms of updates changing its abstract representation. ? This work is supported by the German Federal Ministry of Education and Research (BMBF) under grant 01 IW 10002 (SHIP) Vice versa, the tool can initiate changes in the real world by executing actions or processes.
Complex behaviors can be de ned guided by changes in the abstract world. The behavior of the world is monitored. Process descriptions can be provided to react on successful or failed developments of the world. This enables us, for instance, to monitor the behavior of a black-box device or some users and to react to any non-expected behavior. At the other end of the spectrum it allows us to dene complex activities and work- ows in terms of processes acting on existing devices and services and communicating with the user. The interweavement of process descriptions with monitoring as well as the interleaved execution of parallel processes, both based on the same world representation, provides a powerful formalism to implement processes to assist and monitor activities in the environment in interaction with users and based on existing services and devices.
Using Description Logic to
represent the environment allows for
processes being dynamic description logic
(DDL) programs [
Modeling the World. The SHIP-Tool uses description logic [
Given a set NC of concept names, a set NR of role names and a set of NI of individuals, concepts are de ned inductively from NC and roles from NR. We introduce the description logic SROIQ, which will be used for queries, but only its SRIQ fragment will be used to de ne the ontology. For SROIQ, concepts are formed using the constructors given in Table 1, where T and F are prede ned top and bottom atomic concepts, C and D are either concept names from NC or Name Top Bottom Atomic concept Intersection Union Negation Value Restriction Existential quant.
Number Restriction Nominal concept
Syntax T F c 2 NC C u D C t D :C 8R:C 9R:C = n R.C n R.C n R.C fi1; : : : ; ing
I ; cI CI \ DI CI [ DI
I nCI fa 2 I j8b:(a; b) 2 R ) b 2 CI g fa 2 I j9b:(a; b) 2 R ) b 2 CI g fa 2 I jjfb 2 I j(a; b) 2 RI j = ng fa 2 I jjfb 2 I j(a; b) 2 RI j ng fa 2 I jjfb 2 I j(a; b) 2 RI j ng fi1I ; : : : ; iIng complex concept expressions formed accordingly, R is either a role name from NR or the inverse of a role name R 1, and ij are individual names from NI .
The terminological part of an ontology consists of de nitions and inclusion axioms of concept and role names. Concept names c can be declared as subconcepts of concepts by concept inclusion axioms c v D or de ned by concept equality c = D. Disjointness of concepts is declared by Disjoint. A concept name c directly depends on a concept name d if c is de ned by c = D and d occurs in D. A concept name c depends on a concept name d, if c directly depends on d or there exists a concept name e which depends on d and c directly depends on e. We denote the dependency relation between concept names by >c.
Roles are declared by indicating their domain and range. Similar to concepts, subroles can be declared by limited complex role inclusion axioms r0: : : : :rn v r where r 2 NR and '.' denotes role composition. Furthermore, role names can be de ned as the composition of roles r = r0: : : : rn or as the re exive, transitive closure of another role r = r0*. This is not expressible in description logic and it is translated to r0 v r, Trans(r), Ref(r) when translating to DL. However, it is important as a meta-property to ensure that nothing else than the transitive closure of r0 is in r when enforcing constructiveness of ontologies and it will be used there. SHIP supports the standard role properties Sym, Asym, Trans, Ref, Irref, Func, and FuncInv). A role name directly depends on a role name r0 if r is de ned by r = R and r0 occurs in R. A role name r depends on a role name r0, if r directly depends on r0 or there exists a role name r00 which depends on r0 and r directly depends on r0. We denote the dependency relation between role names by >r.
For SHIP, a TBox consists of the concept inclusions, de nitions and disjointness assertions from Table 2 and those obtained to encode role declarations r:C D. An RBox consists of role inclusions and de nitions as show in Table 2 and property assertions. Furthermore, we require the induced dependency rela
Concept de nition c = C, c 2 Nc, C in SRIQ
SRIQ
Role de nition r = r0 . ... . rn, r 2 NR, r0I rnI = rI where n 1 RI R0I = f(x; z)j9y:(x; y) 2
RI; (y; z) 2 R0Ig.
r = r0*, r 2 NR r0I rI Role properties Fun(r), Invfun(r), Ref(r), as usual
Irref(r), Trans(r), Sym(r),
Asym(r), r 2 Nr Table 2. TBox- and RBox-assertions and their satis ability in an interpretation I I j= ' if . . . cI CI cI = CI cI \ dI = ; RI CI tion on concept and role names to be irre exive (i.e. we consider acyclic TBoxes and RBoxes modulo the transitivity of roles). The TBox and RBox form the terminological part of a SHIP-ontology.
In addition we use the following syntactic sugar to ease the de nition of ontologies in a style inspired by abstract datatypes: { c ::= C1(r11 : D11; : : : ; r1n1 : D1n1 )|...|Cm(rm1 : Dm1; : : : ; rmnm : Dmnm ), c 2 NC is expanded to c = C1 t : : : t Cn and Disjoint(Ci; Cj) 8i 6= j.
Ci v (9ri1:Di1) u : : : u (9rini :Dini ) 81 i m, and rij : Ci Dij, Fun(rij) 81 i m; 1 j ni.
As an example consider the DL declarations de ning Lists over elements Elem. List ::= EmptyList
| NonEmptyList ( hd : Elem , tl : List ) which is expanded to List = EmptyList t NonEmptyList Disjoint ( EmptyList , NonEmptyList ) NonEmptyList v (9hd . Elem ) u (9tl . List ) hd : NonEmptyList Elem Fun ( hd ) tl : NonEmptyList List Fun ( tl )
The ABox part consists of a list of concept assertions a:C, C in SRIQ, declaring a to be a member of the concept C, and role assertions (a,b):R, stating that relation R holds between the individuals a and b. For every SHIP-DL-ontology we assume the unique name assumption. Complex ontologies can be composed by importing and renaming existing ontologies. For instance from the List-ontology before we build an ontology for Routes specifying routes along Positions by hmonitor i ::= `monitor' hstringi hparamsi `=' hfoltl i hfoltl i ::= haboxassi j `not' haboxassi j hstringi hparamsi j hfoltl i `and' hfoltl i j hfoltl i `or' hfoltl i j hfoltl i `=>' hfoltl i j (`all' j `ex') haboxassi `.' hfoltl i j `(' hfoltl i `)' j (`X'j`F'j`G') hfoltl i j hfoltl i `U' hfoltl i import basic . Lists with concepts Elem as Position , List as Route , E mp ty Li st as
EmptyRoute , N o n E m p t y L i s t as N o n E m p t y R o u t e roles hd as route_next , tl as r o u t e _ r e s t i n d i v i d u a l s nil as e m p t y r o u t e where nil:EmptyList is declared in the List-ontology as an empty list.
Throughout the rest of the paper we will denote by O ` ' that ' is satis ed
by the ontology O, where ' can be a TBox, RBox or ABox-assertion.
Monitors. SHIP uses linear temporal logic (LTL) [
When monitoring a property, di erent situations can arise: (i) the property is satis ed after a nite number of steps { in this case, the monitor evaluates to true and terminates successfully; or (ii) the property evaluates to false independently of any continuation { in this case, the monitor terminates with failure; or (iii) the behavior that was observed so far allows for di erent continuations that might both lead to a failure as well as success { in this case, the monitor is still running.
The language is a rst-order temporal logic over description logic
ABoxassertions and similar to that used in [
As an example for a monitor formula we consider a use case where di erent autonomous wheelchairs operate in a building in which they can ride along routes consisting of positions. The SHIP-Tool has been used to add a control layer on top of the wheelchairs to avoid con icting situations by scheduling the routes of the wheelchairs. One simple behavior one wants to monitor is when a new schedule must be computed. The part of the ontology specifying Routes has been introduced before. For the purpose of illustrating this monitor, we use the following TBOX/RBOX-assertions: IDObject ::= WheelChair ( whc_route : Route , whc_carries : OptPerson ) | OptPerson OptPerson = Person | Nobody WCEmptyroute = WheelChair u 9 whc_route . EmptyRoute WCNonEmptyroute = WheelChair u 9 whc_route . NonEmptyRoute It de nes WheelChairs to have a route and carrying a Person or Nobody. Subconcepts are wheelchairs having an empty resp. a non-empty route. To know if a new schedule must be computed, we must successfully observe the behavior: (9wc : WCEmptyroute .F( wc : WCNonEmptyroute )) or (9wc : WCNonEmptyroute .
F( wc : WCEmptyroute and F( wc : WCNonEmptyroute )))
This expresses that either in the current situation we have a wheelchair with an
empty route and that wheelchair eventually gets a non-empty route. Or there is
a wheelchair which currently has a non-empty route, eventually gets an empty
route and then again eventually a non-empty route. If one of these behaviors
is observed, then we must compute a new schedule. The actual monitoring is
performed by formula progression (see, e.g., [
Another example making use of the expressivity provided by SROIQ is when some light l in an area of the at should be on depending on the current day time time, planned rides of the wheelchairs and where the occupants of the at currently are: monitor LightShouldBeOn ( time ,l) = time : Night and l: AbstractOff and 9area :( Area u (9 associated_light 1. { l }) ) . ( // 1. Either some wheelchair has a non - empty route , and ... (9wc : WCNonEmptyroute . ( // carries a person or there is a person in the area ... ( wc : WCCarriesPerson or 9 person :( Person u (9 elementIsInArea . { area }) ) . true ) and // ... the wheelchair is already in or about to enter (( wc , area ): elementIsInArea or (wc , area ): wcnextarea ))) Name simple condition complex condition iteration sequence monitor start guarded execution parallel bounded parallel
Syntax
Semantics if a then b branches according to a or waits until a can be decided else c switch branches according to the speci ed cases case c1 => p which are checked in order. can be used : : : as default case, then, the condition never case ck => p stutters. p* applies p until it fails, always succeeds p ; q applies p then q init m starts the monitor, continues when the monitor succeeds or fails when the monitor fails p +> q executes p; if p fails, q is executed, but the modi cations of p are kept p jj q executes p and q in parallel (interleaved), terminates when both p and q terminate, fails when one of them fails forall c => p executes p for all instances matching c in parallel, terminates when all terminate, fails when one of them fails
Table 3. Process combinators or // the w he el ch ai r is assigned to a person in the same area (9 person :( Person u (9 e l e m e n t I s I n A r e a . { area }) ) . 9 wc :( W he el Ch air u (9 w c A s s i g n e d T o P e r s o n . { person }) ) .
( wc , area ) : e l e m e n t I s I n A r e a ) )
Actions and Processes. The SHIP processes are dynamic description logic
processes based on actions and similar to those in the literature (e.g, [
Using free variables in the e ects, new individuals can be added to O, where a fresh name is created at run-time. By annotating a variable with delete, individuals can also be removed from the ontology. This is necessary, for instance, to remove individuals whose counterpart in the real world no longer exists.
SHIP provides a language to de ne complex processes that interact with the environment. Starting from actions, complex system behaviors can be described by combining other processes as well as by interacting with monitors. Starting from atomic actions, more complex processes can be de ned using the combinators shown in Table 3.
The states of a speci ed system are represented by ABoxes with respect to xed
TBox and RBox and the transition of states corresponds to ABox-updates. Thus
ABox-updates do not change the underlying TBox/RBox semantics
characterizing the overall system states. Hence the approach to ABox-updates from [
Following this line of reasoning we interpret the construction of complex concepts as a kind of speci cation for abstract datatypes. The use of an existential quanti cation in IDObject v 9at . AbstPosition corresponds to the de nition of a mandatory attribute \at" indicating a position in the abstract datatype denoted by IDObject. Conjunction of concepts combines the attributes of the corresponding datatypes while disjunction of concepts resembles the notion of variants. 3.1
Similar to an initialization of all records in new instances of a data-structure we want to enforce a constructive de nition of each individual of a complex concept in an ABox. For instance, having an individual d for the concept IDObject above, we know that d has a position and we demand that the ABox should also provide the knowledge which position d actually has. Furthermore, since we allow for disjunction of concepts D v E t F we also want to know for each individual in D whether it belongs to E or F or both. That means that for any individual d of a (complex) concept the ABox always provides the full information about the composition and settings of the individual. In other words, the ABox provides the individuals necessary to name the values of the various attributes and there is no need to invent new values by introducing Skolem functions.
The same rigor of constructiveness is applied to the speci cation of roles. SHIP allows for the de nition of composed roles, e.g. by de ning r = r1 r2. Knowing that two individuals a; b are in the relation r there must be some individual c such that (a; c) : r1 and (c; b) : r2 holds. We demand that also this witness is speci ed explicitly, i.e. the ABox contains some individual c and the necessary relations between c and the individuals a and b.
These properties can be formalized in the following de nition of constructive ontologies, where E denotes the negation of concept E in negation normalform.
Let O := hT; R; Ai be an ontology wrt. concept names NC , role names NR and individual names NI . The signature of O is O := ( C ; R; I ) (NC ; NR; NI ) of those names of concepts, roles and individuals occurring in O. An ontology O is constructive i the followings hold: 1. if a 2 I , O ` a : D and O ` D v 9r:E then there is some b 2 O ` b : E and O ` (a; b) : r
I with 2. if a 2 I , O ` a : D and O ` D v ( n r:E) then there exist distinct b1; : : : ; bn 2 I with O ` bi : E and O ` (a; bi) : r 3. if a 2 I , O ` a : D and O ` D v E1 t E2 then O ` a : Ei or O ` a : Ei for i = 1; 2 4. if O ` (a; b) : r with a; b 2 NI and O ` r = r1:r2 then there is some c 2 I such that O ` (a; c) : r1 and O ` (c; b) : r2. 5. if O ` (a; b) : r with a; b 2 I and O ` r = r1 then there is a set fc1; : : : ; ckg I such that O ` (ci; ci+1) : r1 for all i 2 f1; : : : ; k 1g and a = c1 and b = ck. 3.2
Demanding constructive ontologies to specify a system (TBox + RBox) and its
actual state (ABox), the concepts an individual belongs to are basically de ned
bottom up. Given an individual a of a xed concept D the de nition above
requires the speci cation of additional information about a. In many cases this
\additional" information is now su cient to deduce that a is (also) of concept
D making the original speci cation that a : D redundant (even worse, specifying
explicitly a : D would render the ontology inconsistent). Analogously to Nebel
[
Based on this normalized TBox the acyclic dependency relation >c on concepts is used to de ne that a concept c 2 c is de ned i there is a concept d 2 c such that c >c d holds and otherwise primitive. Analogously, we use the acyclic relation >r on roles to de ne de ned and primitive roles.
Now, given an ontology O we will enforce non-redundancy by imposing that all ABox-assertions are only primitive concept and role assertions. Furthermore, we use the criteria from the last section to check that O is constructive. As an example, consider the ontology for Lists from Section 2. The only primitive concept is EmptyList and the primitive roles are hd and tl. The ABox containing only the primitive assertions nil:EmptyList, (a,nil):tl is non-redundant, but not constructive. Adding the primitive assertion (a,e):hd makes it constructive. 3.3
In our setting, updates of the ABox correspond to state transitions of the speci ed system. The updates are initiated either by the processes (cf. Section 2) running in the system or by the environment interacting with the system. Regardless of the source of an update we demand that updates will always preserve the constructiveness of the ontology. To this end we enforce that they are speci ed in a non-redundant form by ABox-assertions exclusively over primitive concepts and roles. An update is a pair ( ; ), where is a consistent set of primitive ABox-assertions to be added and primitive ABox-assertions to be removed. For a given ontology O = hT; R; Ai and consistent primitive update ( ; ) the new ABox is determined from the old ABox by 1. If (i : C) 2
is removed; 2. If ((a; b) : R) 2 removed.
and (i : D) 2 A and C and D are disjoint concepts, then (i : D)
, ((a; c) : R) 2 A and R is functional, then (a; c) : R is Finally, all assertions from
are removed. Formally, the update is de ned by A0 := [ (A n ( [f(i : D) 2 Aj(i : C) 2 ; C and D are disjointg
[f((a; c) : R) 2 Aj((a; b) : R) 2 ; R is functionalg) The resulting ontology hT; R; A0i may well be inconsistent, for instance if number restrictions are violated. If so, the update is refused and we stick to the previous ontology O. If an action triggered the update, the action fails in the process semantics. If the environment triggered the update, respective repair processes must have been speci ed to synchronize the SHIP-Tool and the environment. If the ontology is consistent, it is not necessarily constructive. To this end we use the procedure from the last section to check if the resulting ontology hT; R; A0i is constructive. If not, the SHIP-Tool can provide detailed information which information is missing. This can be used to statically analyse the e ects of actions of the de ned processes whether they only contain primitive ABox-assertions and if they are complete enough to preserve constructiveness of the ontology. 3.4
Sometimes updates do also have indirect or implicit consequences that are not
necessarily known to the process that performs the update. In such a situation,
it might be necessary to integrate the indirect consequences immediately to the
ontology in order to prevent some monitors to fail, as sending another update
would introduce a new point in time on our time axis. The problem of how
to describe the indirect e ects of an action { or more generally, an arbitrary
update { in a concise way is known as the rami cation problem. In SHIP we use
causal relationships as introduced in [
The SHIP-Tool is implemented in Scala1 and uses the Pellet Reasoner [
So far, we have used it mainly in three applications: First, for the orchestration of services in an instrumented living environment, the Bremen Ambient Assisted Living Lab (BAALL)2. In this application we have developed in the SHIP-Tool processes to manage transport requests from the inhabitants of the BAALL, to schedule the routes of the wheelchairs operating in the BAALL and to provide assistance by automatically opening and closing doors and switching on and o the lights along the routes of the wheelchairs. A second application is concerned with medical guideline conformant patient treatment, and is pursued in the course of the SIMPLE project.3 Another application is the SmartTies system for the management of the documents arising during the development of safety-critical software.
In all these applications the possibility to include behavior monitoring via LTL over description logic axioms and dynamic description logic proceses provides a suitable mechanism to develop the processes. With respect to the updates, the rst attempt to deal with updates was { roughly speaking { to simply include all e ects of actions. If the new ontology is inconsistent, then we used axiom pinpointing to compute a minimal set of ABox-assertions already contained in the previous ABox which must be removed to restore consistency. That made updates computationally expensive and processes slow. With the approach presented in this paper, this could be resolved resulting in a sensible speedup. Moreover, the constraints imposed by the constructiveness criteria on the ontology and the updates resulted in cleaner ontologies as well as much more concise formulations of actions. 5
This paper presented the SHIP-Tool as a framework to manage the orchestration of heterogeneous programs. Each of these programs communicate with the SHIPTool via ABox-updates. The SHIP-Tool allows for the integration of black-box services by encoding their responses in terms of updates as well as of white-box programs de ned in terms of Dynamic Description Logic and operating natively 2 http://baall.informatik.uni-bremen.de/ 3 http://www.dfki.de/cps/projects/simple on the concepts de ned in the ontology speci ed in the SHIP-Tool. In the same way humans interact with the system by ABox-updates. Hence, ABox-updates become the central notion of computation and we introduced constructive ontologies to speed up the computation of such updates. The resulting restrictions on how ontologies in general and ABoxes in particular have to be speci ed also enforce a proper structuring of the provided concepts and roles. Monitors allow one to control the overall behavior of the orchestrated system and can initiate appropriate measures depending on the success or failure of the monitor. The semantics of the SHIP-Tool is based on combining concepts of dynamic logic, description logic and temporal logic. Embedding these concepts in a combined logic, which is actually under development, we will also be able to verify properties of the systems speci ed and executed inside the SHIP-Tool.