wsmo logo

D8v0.1 Language Evaluation and Comparison

WSMO Working Draft 08 March 2004

This version:
http://www.wsmo.org/2004/d8/v01/20040308/
Latest version:
http://www.wsmo.org/2004/d8/v01/
Previous version:
http://www.wsmo.org/2004/d8/v01/20040308/
Editors:
Uwe Keller
Jos de Bruijn
Authors:
Jos de Bruijn
Ying Ding
Uwe Keller
Axel Polleres

This document is also available in non-normative PDF version.
Copyright 2004 DERI, All Rights Reserved. DERI liability, trademark, document use, and software licensing rules apply.


Table of contents

Executive summary:

In this document we investigate and analyze several different formal and logical frameworks for describing knowledge about a static world as well as formalisms that allow to model dynamic aspects of a changing world.

We aim at defining an adequate logical foundation for both, the Web Service Modeling Ontology (WSMO) [Keller et al., 2004] which represents the basic modeling elements for describing Semantic Web Services according to the Web Service Modeling Framework (WSMF) [Fensel & Bussler, 2002], as well as the future Web Service Modeling Language (WSML) which will be based on the modeling elements included in WSMO and will extend the ontology to a fully-fledged description language for Semantic Web Services.

A rigorous underpinning of WSMO and WSML by means of a formal framework with a well-defined semantics eventually assures that the semantic description of any web service in WSMO/WSML defines non-ambiguously it's capabilities and behaviour. Since these descriptions are represented in a formal language, they can be automatically applied by agents - the semantics of the service becomes machine-processable and agents can discover, invoke, combine and reason about services automatically without human interaction. Thus, a formal foundation for a description language for web services is a necessary precondition for exploiting the full potential of web service technology in areas like Enterprise Application Integration and eCommerce.

We start with the definition of an evaluation scheme that provides a means for identifying several important properties of formal frameworks that are relevant in our context: The description web services and their interaction according to WSMF.

Then we briefly survey several formal frameworks and languages that have different characteristics and analyse them with respect to the established evaluation scheme.

A comparison of different languages with each other which address similar problems follows. In particular, we show what different categories of descriptions have to be representable for formalizing WSMO/WMSL and what formalisms within a certain category fits best our needs.

Finally, we conclude with the definition of a formal framework that can serve as a formal basis for WSMO and WSML.


1. Introduction

1.1 Motivation

Yet to be written!
web services, semantic webservices description languages in general
what is already there. Formal semantics ...

1.2 Goal

In this document we investigate and analyze several different formal and logical frameworks for describing knowledge about a static world as well as formalisms that allow to model dynamic aspects of a changing world.

We aim at defining an adequate logical foundation for both, the Web Service Modeling Ontology (WSMO) [Keller et al., 2004] which represents the basic modeling elements for describing Semantic Web Services according to the Web Service Modeling Framework (WSMF) [Fensel & Bussler, 2002], as well as the future Web Service Modeling Language (WSML) which will be based on the modeling elements included in WSMO and will extend the ontology to a fully-fledged description language for Semantic Web Services.

Why do we need a formal framework? A rigorous underpinning of WSMO and WSML by means of a formal framework with a well-defined semantics eventually assures that the semantic description of any web service in WSMO and WSML defines non-ambiguously it's capabilities and behaviour. Since these descriptions are represented in a formal language, they can be automatically applied by agents - the semantics of the service becomes machine-processable and agents can discover, invoke, combine and reason about services automatically without human interaction. Thus, a formal foundation for a description language for web services is a necessary precondition for exploiting the full potential of web service technology in areas like Enterprise Application Integration and eCommerce.

1.3 Overview of the paper

We start with the definition of an evaluation scheme that provides a means for identifying several important properties of formal frameworks that are relevant in our context in chapter 2: The description web services and their interaction according to WSMF.

Then we briefly survey in chapter 3 several formal frameworks and languages that have different characteristics and analyse them with respect to the established evaluation scheme.

In section 3.5 a comparison of different languages with each other which address similar problems follows. In particular, we show what different categories of descriptions have to be representable for formalizing WSMO resp. WMSL and what formalisms within a certain category fits best our needs.

Finally, we conclude in chapter 4 with the definition of a formal framework that can serve as a formal basis for WSMO and WSML.


2. Evaluation Framework

2.1 Motivation

2.2 Evaluation Scheme

This is the general template that should be used in the evaluation in chapter 3. The single elements in the template contain some proposals what could/should be contained when instantiating the language for a particular framework.

It is possible, that we will refine the framework later on. If you have an additions to the template please feel free to add that (after discussion with the group).

Introduction

Some general notes, motivation for invention of the language, typical application scenarios ...

Syntax

Brief description of the syntax

States.
What expression are used for describing states? How rich is the syntax for describing states of the world? Can we touch states explicitly (names for states)?
State-transitions.
Can we distinguish between elementary/atomic state transitions and composed state transitions ? Can the user define names of atomic state transitions by himself? What operators (= constructive approach) are allowed to combine state transitions to complex state transitions (program flow)? Or do we instead only constrain possible state transitions declaratively (by means of logical expressions)
Protocols.
Are there any means to specify interaction between two agents (protocols) ? How can we describe communication between agents? Can we represent concurrency ? Can we represent properties of protocols like deadlock, livelock, etc. ?

Semantics

Brief description of the semantics

States.
Interpretation of an expression wrt. a single state vs. a sequence/tree of states? What is the semantics of a state? Which structure represents states: Algebras, First-order structures, Sets of fomulas?
State-transitions.
What is the meaning of elementary transitions? What is the meaning of operators for combining state transitions?
Protocols.
What is the semantics of an interaction/protocol between agents? How is the communication between the agents interpreted?

Operationalization

Calculus and Prover.
Is there a complete and sound calculus ? Is there any prover for this framework available? Do we know anything about performance, version, commercial vs. academic prototype? Are there any projects using the inference engine? Can we also check protocol related properties automatically?
Decidability and Complexity.
How complex is reasoning in this framework? Is logical entailment/satisfiability decidable or not? Are there fragments of the language that are decidable?
Logic Programming.
Can we use the framework for logic programming? Is there any logic programming environment for the framework available?
Extension and Combination.
Can the formalism be combined with other formalisms? How difficult is the integration? In particular, the combination of dynamic and static formalisms is relevant!

Representing Ontologies

Here we only care about the ability to represent an ontology.

Can we represent all modeling elements that are contained in the Ontology? What can't be expressed? What things can only be expressed tediously? What can we express additonally? Might this be useful for applications ? Relationship to existing ontology languages ?

Representing Dynamic Aspects of Web Services

Here we care about the ability to represent dynamic aspect of WSMO.

Can we express Pre- and Postconditions of web services? Can we express constraints on the execution of web services? Can we express composition and grey box models of web services (control flow and black-box actions?) Can the description of a composition / protocol be executed by an interpreter ?

Example

Use the example (when it's available) described in the next section.

2.3 Running Example

In this section we introduce a simple example, which illustrates our needs when formalizing real-world secenarios. At the same time this example will be used in chapter 3 as a fairly simple test-bed, that clarifies the strengths and weaknesses of the several formalisms with respect to our specific problem domain.

This example originally has been invented in []. We follow the scenario given in this paper as far as possible.

2.3.1 Scenario


3. Evaluation of Logical and Formal Frameworks

- Placeholder -

3.1 Overview

- Placeholder -

3.2 Languages for Representing Knowledge about a static World

- Placeholder -

3.2.1 OWL & SWRL

OWL basics

The World Wide Web Consortium [W3C] has set the standard for the ontology language on the Semantic Web, with the name of OWL [Dean & Schreiber, 2004]. OWL has three dialects with the names of OWL Lite, OWL DL and OWL Full. Each lower (less expressive) dialect is both syntactically and semantically contained in the higher (more expressive) dialects, where OWL Lite is the least expressive and OWL Full is the most expressive dialect.

OWL is based on Description Logics (earlier called terminological logics) [Baader et al., 2003], which is a class of logic languages with a history in knowledge representation\footnote{Note that ontologies come from the Artificial Intelligence research area of Knowledge Representation. An ontology is used to represent some knowledge which is held by some group of people.}. In the 1980s several early Description Logic-based Knowledge Representation systems were developed, such as CLASSIC [Borgida et al., 1989] and KL-ONE [Brachman and Schmolze, 1985].

In the beginning of the 2000s, the Web ontology language OIL (Ontology Inference Layer) [Fensel et al., 2001] was created, combining Description Logics, with its many efficient implementations of reasoners, and frame-based primitives, used to support the development and maintenance of ontologies, with XML and RDF to create an ontology language based on Web standards. In 2001, the DAML+OIL language [Horrocks and van Harmelen, 2001], a combination of the DAML-ONT [McGuinness et al., 2003] and the mentioned OIL efforts, was finalized and submitted to the W3C as the basis for the new Web Ontology Language (i.e. OWL).

Both OIL and DAML+OIL have a translation to the expressive SHIQ Description Logic language, for which efficient reasoning implementations exist (cf. [Horrocks, 2002]).

Description Logic Basics We will now try to explain the basics of Description Logics without going into too much detail.

There are three important concepts in Description Logics. These are concepts, roles and individuals. The major strength of Description Logics is its ability to classify concepts and individuals using descriptions of individuals and definitions of concepts. For example, if there exists a concept definition stating:

Student ≡ Msc-Student ⊔ PhD-Student

Which means that the concept Student encompasses all individuals in the concepts of Msc-Student and PhD-Student. It also means, because of symmetricalness of the equivalence relationship (≡), that all individual for the concept Student are either contained in the concept Msc-Student or in the concept PhD-Student or in both. We now know for every particular individual that is an instance of the concept Msc-Student or an instance of the concept PhD-Student, that it is also an instance of the concept Student. We have, however, also excluded the possibility of having other students than Msc or PhD students. If we were to introduce a concept Bsc-Student, it would not be possible to group it under Student, unless we change the definition of Student to incorporate Bsc-Student.

The most important aspect of Description Logics, from a modeler's point of view, is that roles are specified independently from concepts. This allows for automatically determining the class of an individual based on the roles specified for that individual. This is conceptually a nice feature, but not always very clear for the human user, because humans tend to think in roles belonging to concepts and individuals specified directly as belonging to specific concepts.

For a more elaborate introductory to Description Logics we refer the interested reader to [Baader et al., 2003].

OWL Full combines RDF with the expressive SHIQ(D) (which is SHIQ extended with datatype support) Description Logic language in order to create an ontology language for the Semantic Web, which is (both syntactically and semantically) layered on top of RDF. OWL DL restricts OWL Full to that part, which is still (theoretically) decidable. OWL DL is equivalent to the SHOIN(D) Description Logic. Reasoning in OWL DL is still very hard; entailment (proving that one statement in OWL DL is a logical consequence of another) has a worst-case complexity of NExpTime (non-deterministic exponential time) [Horrocks et al., 2003].

OWL Lite restricts OWL DL further to a language which has the expressivity of the SHIF(D) Description Logic. In the SHIF(D) language, satisfiability is computable in ExpTime (exponential time). And because entailment in OWL Lite can be reduced to satisfiability in SHIF(D) [Horrocks and Patel-Schneider, 2003], entailment in OWL Lite can be computed in ExpTime.

3.2.2 CARIN

- Placeholder -

3.2.3 Frame Logic

- Placeholder -

3.2.4 TRIPLE

- Placeholder -

3.2.5 $\mathcal{DLR}_{Reg}$

[AP: I need the running example here in order to decide whether it makes really sense to mention this language here. It is definitely interesting wrt. what we currently investigate in the Logic Programming workgroup.]

Another interesting language for representing ontologies is the logical language DLR<sub>reg</sub>, which stems more from the Database community, defined by [Calvanese et al., 1998]. This language is originally meant to define Database schemas with constraints rather than ontologies in general. However, since databases with relational inclusion constraints can also be modeled, this language allows most usual modelling primitives of common ontology languages.

There is no dedicated XML syntax for this language available and no implemented reasoners. However, it is interesting for two reasons:

It defines very general concepts which can express several conceptual relations in an ontology such as functional dependencies, cardinality constraints, etc. on a strong formal basis. The language contains interesting features such as regular expressions built from the projection of arbitrary relations to two of its attributes which are not common in current ontology languages. Note that $\mathcal{DLR}_{Reg}$ assumes unique names.

Remarkably, [Calvanese et al., 1998] provides formal background and decidability results for query containment under constraints in such a powerful ontology language, where queries can be basically viewed as nonrecursive datalog programs with negation with respect to the features of $\mathcal{DLR}_{Reg}$.

These results might be particularly intersting with respect to capability matching of web services with respect to a set of given constraints, which amounts to deciding query containment. The authors state decidability results for two classes of queries, where either cardinality constraints or regular expressions are prohibited. Decidability of query containment for the combination of these two features is still open. Furthermore, undecidability is proven, if term inequality is allowed as a predicate in rule bodies of queries.

These results are based on translating the language to a special form of PDL.

The relation to respective complexity results for several discussed extensions of Description Logics remains to be investigated.

3.2.6 SHOE

The Simple HTML Ontology Extensions (SHOE) Language [Heflin et al., 1999] is an extension of HTML which allows to incorporate metadata and semantic knowledge in HTML or other WWW documents dating back from the pre-OWL era. It allows to specify a class taxonomy and relations between classified elements and a simple way to specify ontologies containing rules. In SHOE, concepts are called categories and arbitrary relations (n-ary) relations are allowed. SHOE does not offer as rich expressions as OWL on the one hand but on the other hand it has the full power of Horn clauses.

To make ontology declarations possible SHOE adds several tags to HTML providing an overall HTML-compatible syntax.

You can import ontologies by the USE-ONTOLOGY construct, for instance

     <USE-ONTOLOGY ID="base-ontology" VERSION="1.0" PREFIX="b"
                   URL="http://www.cs.umd.edu/projects/plus/SHOE/base.html"/>

To state a describe a class taxonomy, you write constructs like

     <DEF-CATEGORY NAME="Person" ISA="b.SHOEentity">

Furthermore, you can define relations by typing their parameters, for instance

    <DEF-RELATION NAME="Parent">
         <DEF-ARG POS="1" TYPE="Person">
         <DEF-ARG POS="2" TYPE="Person">
    </DEF-RELATION>

Some fixed data-types like ".DATE", ".NUMBER", ".STRING", and ".TRUTH" are defined in the SHOE Base ontology.

Instances are given fixed (unique) ID[1] in form of a URI. For example, an instance in SHOE could look as follows:

    <INSTANCE KEY="http://www.cs.umd.edu/users/george/#Axel">
    <CATEGORY NAME="Person">
    <RELATION NAME= "Parent">
        <ARG POS=TO VALUE="http://www.cs.umd.edu/users/george/#Herbert">
    </RELATION>
    </INSTANCE>

Here position "TO" is a shortcut which may be used for binary relations (i.e. properties).

Finally, SHOE allows for adding inferences over relations and classes by arbitrary Horn rules. Furthermore, SHOE offers simple means for versioning. SHOE is no longer actively developed although there are some nice tools like the Knowledge annotator to support semi-automatic annotation of Web-Sites using SHOE. Via Horn Rules the formal semantics of SHOE seems to be straightforward.

While syntactically not very powerful there are still features like arbitrary (n-ary) relations and Horn rules which can not be easily expressed in DL-based languages like OWL.

3.3 Language for Representing Dynamics - States & State Changes

- Placeholder -

3.3.1 Transaction Logic

- Placeholder -

3.3.2 Dynamic Logic

Dynamic Logic (DL) is a multimodal logic to represent the state changes. It adds a little above the classical logic with a fixed modality for each program. It also uses various calculi of programs in conjunction with the rules of classical propositional and predicate logic to give a rich family of systems for analyzing the interaction of programs and formulas. By analogy with the construction of composite formulas from atomic ones, the calculi of programs allow the construction of complex programs from atomic ones. Typical atomic programs are assignment statements and basic tests, the operators used to construct composite programs may be familiar programming constructs such as if-then-else and while-do.

DL is good at representing the state changes and verifying precondition, postcondition and relation between input and output. DL is not tailored to reasoning about program behaviour manifested in intermediate states of a computation (while process logic and temporal logic can).

Dynamic Logic has two groups: Propositional DL (PDL) and first-order DL (FDL). Propositional DL is like propositional logic in classical predicate logic. It describes the properties of the interaction between programs and propositions that are independent of the domain of computation. Propositional DL is the subsystem of first-order DL and the main differences between Propositional DL and first-order DL can be summarized as followings:

Propositional DL is the subsystem of first-order DL. First-order DL provides more expressive power. Here we focus on first-order DL, which is shorted to FDL in the rest of the section.



Syntax

The vocabulary of FDL isplaceholder, where f, g denote typical function symbols of placeholder, and p, r denote typical relation symbols. Associated with each function and relation symbol of placeholderis a fixed arity (number of arguments). Nullary functions are called constants. Countable set of individual variables placeholder.

DL has formulas and programs. The main role of program is to change the values of variables in the formulas, therefore it changes the values of formulas. Formulas and programs are built inductively from the atomic ones using the following operators:

Formula operators:

implication

0 falsity

placeholder for all quantifier

Program operators:

; composition

U choice

* iteration

Mixed operators:

[] necessity

? test

If placeholder, placeholder are formulas and placeholder, placeholder are programs, then

placeholderplaceholder formula implication

[placeholder]placeholder program necessity

are formulas, while

placeholder; placeholder sequential composition (first placeholderthen placeholder))

placeholder nondeterministic choice (nondeterministicaly choose one of placeholderor placeholderand execute it))

placeholder* iteration (execute placeholdersome nondeterministicaly chosen finite number of times)

are programs.

Inductive definition of programs and formulas are intertwined and can not be separated. While in the ancestor of DL, which is called Hoare Logic, programs and formulas are defined separately and there are not intertwined with each other. Furthermore, the formula operators placeholder, placeholder, placeholder, placeholder, and 1 can be defined from formula operators, while <> can be defined from the necessity operator. placeholder can be defined from placeholder.



Atomic formulas and programs

In FDL, atomic formulas are atomic formulas of first-order vocabulary placeholder. So formulas are the followings:

where r is an n-ary relation symbol of placeholderare terms of placeholder.



Atomic programs include assignment, which can be: Simple assignment is atomic program which assigns the value to variable.

placeholder

where placeholderand t is a term of placeholder. This can be used to represent that state changes to a new state in which the new value of x is t and the values of all other variables are the same as they were before. In DL, this assignment can be further extended to stack, array, and nondeterministic “wildcard” assignments:

Nondeterministic or wildcard assignment or nondeterministic choice construct is also allowed in FDL.



Compound formulas and programs

Formulas are defined inductively from atomic formulas using various formulas or mixed operators, such as:

, [placeholder]placeholder are compound formulas.

: It is possible to execute program placeholderstarting from the current state and halt in a state where formulasplaceholderis true. Here formula placeholdercan be considered as post condition. Such as:placeholder is equal to this DL formula placeholder

: If program placeholderhalts when started in the current state, then it must be in a state where formula placeholderis true. Here formula placeholdercan be considered as post condition.



Compound programs are formed from the atomic programs and tests by induction, using the composition, conditional, and while operators, such as, if placeholder is a test and placeholderand placeholderare programs, then the followings are compound programs:

then do placeholder)

if placeholder then placeholderelse placeholder

while placeholder do placeholder

Some definitions of compound programs are:

placeholder

Program skip and fail are the program that does nothing and or fail. The ternary if-then-else operator and the binary while-do operator are the usual conditional and while loop constructs found in conventional programming languages. The constructs if-|-fi and do-|-od are the alternative guarded command and iterative guarded command constructs.



State

In FDL, state is defined to be a valuation function that assigns a value to each program variables. The value for variable x must belong to the domain associated with x, which includes certain distinguished constants, basic operations, and tests that can be performed on those values. At any given time during its execution, the program is at some state determined by the instantaneous values of all its variables.



EXAMPLE1.

The following program implements the Euclidean algorithm for calculating the greatest common divisor (gcd) of two integers. It takes as input a pair of integers in variable x and y and outputs in variable x:

While y=/=0 do
begin
z:= x mod y;
x:= y;
y:=z
end

A state for the gcd program above can be (15, 27, 0, …)where the first, second, and third components of the sequence denote the values assigned to x, y, and z respectively. The ellipsis “…” refers to the values of the other variables which we do not care since they do not occur in the program.

In PDL, state is represented by the truth values of set of predicates holding in a state.

EXAMPLE2.

Representing a state in FDL: (15, 27, 0, …)

Representing a state in PDL: 1 (true), 0 (false)



State transitions

Both PDL and FDL can provide explicit definitions of transitions. But transitions can only be defined in terms of assignments to variables, or true assignments to propositions or predicates.

A program can be viewed as a transformation on states. Given an initial (input) state, the program will go through a series of intermediate states, perhaps eventually halting in a final (output) state. The program in EXAMPLE1 will go through the following sequence of states:

(15,27,0), (15,27,15), (27,27,15), (27,15,15), (27,15,12), (15,15,12), (15,12,12), (15,12,3), (12,12,3), (12,3,3), (12,3,0), (3,3,0), (3,0,0).

In DL, a program is represented by a binary relation between initial and terminal states. There is no explicit representation of intermediate states of the program execution. So DL can only represent step-based control, while temporal logic can represent sequence-based control (it can define the explicit representation of the intermediate states of the program execution).

In PDL, transition can only be characterized implicitly. No operational definitions can be given for how to compute transitions. They can only be characterized by defining the properties of the original and final state of a transition, such as a formula:

means that program placeholderis executed in a state where p holds, and if placeholderterminates, the result will be a state where q holds.

In FDL, transition can be described explicitly. Operational definitions are given to compute transitions.



Elementary state transition

Elementary state transition should be described without enforcing any details to the algorithmic realization. It means that it is purely external definition. Only input and output of the system are concerned, while internal details should not be represented. But elementary state transition can be refined to the lower level of specification, where an internal specification should be given. So after refinement, the elementary transition is considered to be a composed transition.

FDL represents elementary state transition by assigning value to program variables. It is first-order structure, such as x : = t

In PDL, atomic programs are just abstract binary relations.

EXAMPLE3.

Elementary state transition in FDL: x : = t

Elementary state transition in PDL: p: = True



Composed state transition

Constraining specification (nonconstructive) defines contrains only (not directly into the actual control flows) Constructive specification defines the actual control flow of a system and each control flow which is not defined is not possible to be further executed.

In DL, control is specified using programs (with assignment, test, iteration, etc.). Thus the specification of control in DL is constructive. While a choice operator can bring in the indeterminism. Such as the example to obtain a square root of y would be the program, which is the composed transition by elementary transition using loop constructs:

; while placeholder do placeholder

Composed transition can be defined by composing elementary transitions via sequence, iteration, and choice operators.

EXAMPLE4.

Composed state transition in FDL: x : = t1; y : = t2

Composed state transition in PDL: p: = True U r: = false



Protocols

DL cannot represent concurrency.



Semantics



The semantics of programs and formulas in FDL can be interpreted over a first-order structure. The operational view of program semantics is that programs change the values of variables by sequences of simple assignments or other assignments, and flow of control is determined by the truth values of tests performed as various times during the computation. Formulas are precondition or the post condition of the program before and after the execution of the program. The state (an instantaneous snapshot of all information at any moment) during the execution of the program is represented by the values of the program variables. In FDL, possible worlds defined as value assignments to variables, and accessibility relations between possible worlds for each of the elementary and composed transition.

The semantics of DL comes from the semantics for modal logic. Modal logic is particularly well suited for reasoning in dynamic situations – situations in which the truth values of statements are not fixed, but may vary over time. Classical first-order logic is static, in the sense that the truth values of its statements are immutable. Sentences of classical first-order logic can be interpreted over a single structure, or world. In modal logic, an interpretation consists of a collection K of many possible worlds or states. If states can change somehow, then so can the truth values.

The truth of modal formulae is determined by an accessibility relation between these possible worlds. The accessibility relations are determined by the set of possible worlds. Thus the set of possible worlds plus the accessibility relation form a Kripke structure . The accessibility relations are defined semantically as the associated pair (u,v) of the valuations with the program placeholder, which means t hat if the program starts in the state with the valuation u, execute the program placeholder, and it halts in the state with the valuation of v. So (u,v) is called the input/output pair of placeholder and v is a finite variant of u. This is also resulted in a Kripke frame.





Atomic formulas and programs

In PDL, a Kripke frame is a pair placeholder, where K is a set of elements u, v, w,… called states and placeholderis meaning function assigning a subset of K to each atomic proposition and a binary relation on K to each atomic program, that is,

placeholderplaceholder

We can extend the definition of the function placeholderby induction below to give a meaning to all elements of formulas and programs, such that

placeholder



In FDL, every program placeholderis associated with a binary relation:

placeholder

is associated with a set:

placeholder



Composed formulas and programs

In PDL, composed programs are defined inductively by atomic formulas and programs:

placeholder

placeholder

In FDL, semantics of the composed programs are defined as followings:

placeholder

In FDL, semantics of the composed formulas are defined as followings:

placeholder

0.2.1State

In PDL, the declarative semantics is defined as a possible world which is a truth assignment to all the predicates.

In FDL, the declarative semantics of state is the values of all the variables (valuations u, v, … of the variables V. A state is a mapping from variables to values in some domain.



0.2.2State transitions

In DL, programs are interpreted as binary input/output relations and the program constructs as operators on binary relations. placeholder, ;, * are interpreted as operators on sets of strings over a finite alphabet. While programs is equivalent to the subclass of the regular programs in which the program operator placeholder, ;, * are constrained to appear only in these forms. The relation denoted by a compound program is determined by the relations denoted by its parts.

EXAMPLE5.

Elementary state transition in FDL: x : = t, semantics are:

placeholderState1: x=1, y=2

After executing x : = t

State2: x=t, y=2



Elementary state transition in PDL: p: = True, semantics are:

placeholderState1: p=T, r=F

After executing p := True

State2: p=T, r=F



EXAMPLE6.

Composed state transition in FDL: x : = t1; y : = t2, semantics are:

placeholderState1: x=1, y=2

After executing x : = t1

State2: x= t1, y=2

After executing y : = t2

State3: x= t1, y= t2



placeholderComposed state transition in PDL: p: = True U r: = False, semantics are:

State1: p=F, r=T

if executing p := True

State2 will be: p=T, r=T

if executing r := False

State2 will be: p=F, r=F



Operationalization

[Spruit et al., 1995] presents a proof calculus for PDL which is sound and complete for full Kripke structures.

Dynamic Logic is a modal logic, while propositional logic and first-order logic are also kinds of modal logic. Therefore FDL and PDL can be combined with F-Logic, which are implemented in transaction logic. Since they are just kinds of modal logic, by adding more modality to modal logic, the combination can be easily achieved.

Propositional logic can be extended to propositional modal logic by adding a new unary operator, the necessary operator (the possibility operator can be defined based on the necessary operator).

Let program A={a, ….} be a set of modalities. Instead of augmenting propositional logic with one modality, we can augment it with a separate modality for each placeholder. Such as if placeholderis a formula and placeholder, then [a] placeholderis a formula. Such as Kripke frame is multimodal structure.

While programs in FDL can be extended to include constructs such as blocks with declarations, recursive procedures with various parameter passing mechanisms, higher-order procedures, concurrent processes etc. It is easy to extend to many other programming languages, and many other logics.

The axiomization is sound and complete only for full structures (domains should be finite)

Representing Dynamic Aspects of Web Services.

The variables in programs hold the input and output values or intermediate results. Input and output can be values from a specific domain of computation, which is a structure consisting of a set of data values along with certain distinguished constants, basic operations, and tests that can be performed on those values.

DL can reason about the behaviour of a program that is manifested in its input/output relation. It is not well suited to reasoning about program behaviour manifested in intermediate states of a computation (while process logic and temporal logic do).


Formulas are conditions, formula in the left side is pre condition, formula in the right side is post condition. Programs happen at certain state and after executing the program, the states changes.

3.3.3 Temporal Logic

- Placeholder -

3.3.4 Process Logic

- Placeholder -

3.3.5 Modal Change Logic

- Placeholder -

3.3.6 Situation Calculus

The situation calculus [McCarthy & Hayes, 1969], a good overview is also given in [Reiter, 2001] is a language for reasoning about actions based on Predicate Calculus (i.e. first-order logic). Here, actions are denoted by function symbols. Furthermore, the predicates and functions describing the current state of the world are called fluents. Relational Fluents are predicates. Functional fluents on the other hand are function symbols, to be used for instance in equations. Situations are terms of the form s or do(act,s), where s denotes a situation and act denotes an action and do is a distinct function symbol expressing the execution of an action. The initial situation is denoted by the constant symbol s0. For instance, in order to express that a block a is on top of block b after being moved there in situation s can be expressed as follows:


\begin{displaymath}\forall a,b,s on(a, b, do(move(a,b),s))\end{displaymath}

or alternatively:


\begin{displaymath}\forall a,b,s on(a, do(move(a,b),s))= b\end{displaymath}

when considering on as a functional fluent. Note that in some formulations also relational fluents are denoted by function symbols, using a distinct predicate holds instead, e.g.


\begin{displaymath}\forall a,b,s holds(on(a, b), do(move(a,b),s))\end{displaymath}

[AP: Again, I would need the running example to incorporate this properly!]

The above situation calculus formula is an example of an effect axiom. In the very general setting of the situation calculus, there are several other problems which have to be expressed explicitely, in order to achieve correct semantics of the clipping of the world one wants to formalize.

Qualification problem

The qualification problem is how to define the executability of an action. Usually, this is expressed by a distinct predicate Poss(act, s) stating that action act is possible in situation s. However, finding the formula F such that $F \supset Poss(act, s)$ is normally hardly possible, since it is tedious to define all conditions which might hamper the execution of an action. Thus, one often makes some world-closing assumptions when formalizing qualification axioms.

Frame problem

Adhering to the general law of inertia it has to be defined what fluents remain unaffected by executing an action. The problem here is that the number (or the size, respectively) of the frame axioms is quadratic (m x n if m is the number of fluents and n is the number of actions) in the worst case.

Solutions of the frame problem are considered to be methods to generate these frame axioms in a parsimonious, automated fashion. Here, for instance Pednault [Pednault, 1989] found out that if


\begin{displaymath}E^+(\vec{x},\vec{y},s) \sup F(\vec{x}, do(A(\vec{y}),s)\end{displaymath}


\begin{displaymath}E^-(\vec{x},\vec{y},s) \sup \neg F(\vec{x}, do(A(\vec{y}),s)\end{displaymath}

(i.e., the conditions which make a fluent $F(\vec{x})$ true, or false, resp., when a particular action $A(\vec{y})$ is executed) are completely known, then the frame axioms are easy to state. Pednault's approach is covered in the planning language ADL. Note that nondeterminsm can not be expressed in this appraoch, since effect axioms of the above form cannot be given for any non-deterministic action. However, for deterministic actions this solution provides a systematical approach to the frame problem, but the representation of frame axioms is still quadratic (i.e. not parsimonious).

On the other hand, nondeterminism of actions can be easily expressed in the Situation Calculus, e.g.:


\begin{displaymath}\forall coin, s heads(coin,do(toss(s)) v tail(coin,do(toss(s))\end{displaymath}

In its general form, the Situation Calculus has the full flexibility of first-order logic for reasoning about actions and their effects and therefore defines a clear formal semantics for such reasoning. Compared with other formalisms on reasoning about dynamics, it makes some limiting assumptions like atomic actions which are sequentially executed, i.e. concurrent action execution is not foreseen. Additionally, a discrete notion of time is implicit, where each action takes exactly one time unit. So, durative actions and effects can also not directly be expressed.

Concerning efficient reasoning in the situation calculus, it is interesting that several restricted subsets of the situation calculus like STRIPS and ADL (discussed in the next section) allow for efficient reasoning engines for particular reasoning prolems, namely, the planning problem. Since apart from STRIPS and ADL, there are several dedicated languages for planning available, these will be covered in an own section below.

3.3.7 Planning Languages - STRIPS and Descendants

The planning problem is, given a set of actions along with their pre-conditions and effects, an initial state and a goal, automatically finding some sequence of actions which achieve that goal. In the context of web-services, planning in its various forms is often considered in the literature as a possible technique for solving the automatic composition problem, although these hopes seem to be doubtful. Still, there could be hope that the long-term experience of the planning community and the sophisticated heuristic search methods which have been developed over the past years to solve planning problems can be fruitfully applied to some of the subproblems related to Web Service Composition.

STRIPS [Fikes & Nilsson, 1971] is a very simple approach for formalizing actions and change Here, an action (often called operator) a is defined by lists of preconditions pc(a), negative (delete-list) effects del(a), and positive (add-list) effects add(a), where these lists are simple conjunctions of fluents.

The example from above could be modeled in STRIPS as follows (STRIPS and its descendants often use a LISP-like syntax):

(:action move
 (:parameters ?block ?from ?to)
 (:preconditions (and (clear ?block) (clear ?to)
                      (on ?block ?from)))
 (:effect        (and (clear ?from) (on ?block ?to)
                      (not (clear ?to)))) )

Semantics of STRIPS is clearly defined with implicit frame axioms for all fluents. Since in STRIPS effects are not conditional and deterministic, Pednault's approach from above can be trivially applied.

However, the expressive power of pure STRIPS is quite restricted by that only conjunctions of preconditions and effects are allowed. Alternative qualifications for an action have to be modeled by different operators. Due to its formal basis on the Situation Calculus, sequential execution of actions is assumed, i.e., no parallel execution of operators is allowed. Effects can only be modeled as consequences of actions, but there are no means of describing ramifications, i.e., state axioms or indirect effects.

Nevertheless, STRIPS and its descendants ADL [Pednault, 1989] and later PDDL [Ghallab et al., 1998,Fox & Long, 2003], etc. have gained great popularity in the planning community. These descendants also include extensions to express conditional effects (ADL), state axioms, durative actions, etc. where several of these extensions are beyond what is directly expressible in the Situation Calculus. Last but not least, PDDL has become a quasi standard, being the official language used in the International Planning Competition (IPC) held every second year in the course of the ``International Conference on Automated Planning and Scheduling (ICAPS)'' (formally, ``Artificial Intelligence Planning and Scheduling Conference (AIPS)'').

A major drawback of all these languages is their strict operator-based syntax which is far from natural language descriptions of transitions between states. Furthermore, all these languages are restricted to complete knowledge on the initial state and deterministic effects of actions. Extensions of these classical planning languages by means of expressing nondeterminism or incomplete knowledge are manyfold (e.g. by the language NPDDL [Bertoli et al., 2003]), but no proposal has made its way to the PDDL standard yet. Since providing a standard, widely accepted language for the IPC is the main focus of PDDL, extensions are accepted only very cautiously.

3.3.8 Action Languages

- To be filled -

3.3.9 EaGLe

- To be filled -

3.3.10 Abstract State Machines

- Placeholder -

3.4 Language for Representing Dynamics - Interactions & Protocols

3.4.1 BPEL4WS

- Placeholder -

3.4.2 BPML/WSCI

- Placeholder -

3.4.3 Process Algebra

- Placeholder -

3.4.4 $\pi $-Calculus

- Placeholder -


3.5 Comparison

- Placeholder -

3.5.1 Frameworks for modeling static Information

- Placeholder -

3.5.2 Frameworks for modeling Dynamics

- Placeholder -

3.5.3 Combining Frameworks

- Placeholder -

3.6 Conclusions

- Placeholder -


4. Conclusions

4.1 Lessons learned from the Evaluation

4.1.1 Static Aspects

4.1.2 Dynamic Aspects

4.2 Defining a logic for WSMO/WSML

4.3 A formal Foundation for WSMO

Mapping WSMO to our logical Framework. Detailed explanation!

4.4 Future Work

A formal Foundation for WSML

Look at other frameworks: - First-Order Logic - Description Logics - HiLog

References

[Baader et al., 2003] F. Baader, D. Calvanese, and D. McGuinness: The Description Logic Handbook, Cambridge University Press, 2003.

[Bertoli et al., 2003] Bertoli, P., Cimatti, A., Lago, U. D., & Pistore, M. (2003). Extending PDDL to Nondeterminism, Limited Sensing and Iterative Conditional Plans. In Proceedings of ICAPS'03 Workshop on PDDL Trento, Italy.

[Borgida et al., 1989] Borgida, A., Brachman, R. J., McGuinness, D. L., and Resnick, L. A. (1989). Classic: A structural data model for objects. In Proceedings of the 1989 ACM SIGMOD International Conference on Management of Data, pages 59 - 67.

[Brachman and Schmolze, 1985] Brachman, R. and Schmolze, J. (1985). An overview of the kl-one knowledge representation system. Cognitive Science, 9(2):171 - 216.

[Calvanese et al., 1998] Calvanese, D., Giacomo, G. D., & Lenzerini, M. (1998). On the Decidability of Query Containment under Constraints. In Proceedings of the Seventeenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, June 1-3, 1998, Seattle, Washington (pp. 149-158).: ACM Press.

[Dean & Schreiber, 2004] M. Dean and G. Schreiber (eds.): OWL Web Ontology Language Reference, W3C Recommendation, 10 February 2004. Available at http://www.w3.org/TR/2004/REC-owl-ref-20040210/.

[Fensel & Bussler, 2002] Fensel, D. & Bussler, C. (2002). The Web Service Modeling Framework WSMF. Electronic Commerce Research and Applications, 1(2), 113-137.

[Fensel et al., 2001] Fensel, D., van Harmelen amd I. Horrocks amd D. L. McGuinness, F., and Patel-Schneider, P. (2001). OIL: An ontology infrastructure for the semantic web. IEEE Intelligent Systems, 16(2).

[Fikes & Nilsson, 1971] Fikes, R. E. & Nilsson, N. J. (1971). STRIPS: A new Approach to the Application of Theorem Proving to Problem Solving. Artificial Intelligence, 2(3-4), 189-208.

[Fox & Long, 2003] Fox, M. & Long, D. (2003). PDDL 2.1: An Extension to PDDL for Expressing Temporal Planning Domains. Manuscript.

[Ghallab et al., 1998] Ghallab, M., Howe, A., Knoblock, C., McDermott, D., Ram, A., Veloso, M., Weld, D., & Wilkins, D. (1998). PDDL -- The Planning Domain Definition language. Technical report, Yale Center for Computational Vision and Control. Available at http://www.cs.yale.edu/pub/mcdermott/software/pddl.tar.gz.

[Heflin et al., 1999] Heflin, J., Hendler, J., & Luke, S. (1999). SHOE: A Knowledge Representation Language for Internet Applications. Technical Report CS-TR-4078 (UMIACS TR-99-71), Dept. of Computer Science, University of Maryland at College Park.

[Horrocks, 2002] Horrocks, I. (2002). DAML+OIL: a reason-able web ontology language. In Proc. of EDBT 2002, number 2287 in Lecture Notes in Computer Science, pages 2 - 13. Springer.

[Horrocks and Patel-Schneider, 2003] Horrocks, I. and Patel-Schneider, P. F. (2003). Reducing OWL entailment to description logic satisfiability. In Proc. of the 2003 International Semantic Web Conference (ISWC 2003), Sanibel Island, Florida.

[Horrocks et al., 2003] Horrocks, I., Patel-Schneider, P. F., and van Harmelen, F. (2003). From SHIQ and RDF to OWL: The making of a web ontology language. Journal of Web Semantics, 1(1).

[Horrocks and van Harmelen, 2001] Horrocks, I. and van Harmelen, F. (2001). Reference description of the daml+oil (march 2001) ontology markup language. Technical report, DAML. http://www.daml.org/2001/03/reference.html.

[Keller et al., 2004] Keller, U., Lausen, H., & Roman (editors), D. (2004). Web Service Modeling Ontology (WSMO). Working draft, Digital Enterprise Research Insitute (DERI). Look at http://www.nextwebgeneration.org/projects/wsmo/2004/.

[McCarthy, 1990] McCarthy, J. (1990). Formalization of Common Sense, papers by John McCarthy edited by V. Lifschitz. Ablex.

[McCarthy & Hayes, 1969] McCarthy, J. & Hayes, P. J. (1969). Some Philosophical Problems from the Standpoint of Artificial Intelligence. In B. Meltzer & D. Michie (Eds.), Machine Intelligence 4 (pp. 463-502). Edinburgh University Press. reprinted in [[McCarthy, 1990]].

[McGuinness et al., 2003] McGuinness, D. L., Fikes, R., Stein, L. A., and Hendler, J. (2003). DAML-ONT: An ontology language for the semantic web. In Fensel, D., Hendler, J., Lieberman, H., and Wahlster, W., editors, Spinning the Semantic Web: Bringing the World Wide Web to Its Full Potential, chapter 3, pages 65 - 93. MIT Press.

[Pednault, 1989] Pednault, E. P. D. (1989). Exploring the Middle Ground between STRIPS and the Situation Calculus. In Proceedings of the 1st International Conference on Principles of Knowledge Representation and Reasoning (KR'89) (pp. 324-332). Toronto, Canada: Morgan Kaufmann Publishers, Inc.

[Reiter, 2001] Reiter, R. (2001). Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems. MIT Press.

[Spruit et al., 1995] P.Spruit, R.Wieringa, and J.-J. Meyer (1995). Axiomatization, declarative semantics and operational semantics of passive and active updates in logic databases. J. Logic and Computation, vol. 5, no. 1, pp. 27-50.

[W3C] World Wide Web Consortium. http://www.w3.org/



Footnotes

[1] i.e., SHOE adheres to the unique name assumption.


Acknowledgements

The work is funded by the European Commission under the projects DIP, Knowledge Web, Ontoweb, SEKT, SWWS, Esperonto, COG and h-TechSight; by Science Foundation Ireland under the DERI-Lion project; and by the Vienna city government under the CoOperate programme.


$Date: 2004/03/08 11:07:56 $

webmaster