Most useful Web services are reactive systems that repeatedly act and react in interaction with their environment without necessarily terminating. Current Standards (XML based/Ontologies) for specifying behavioural semantics of services consider transformational aspects of service behaviour. Specification of reactive Web services require representation of properties that are temporal in nature. The properties need to be specified in a declarative form that is consistent with the dialect used for describing other aspects of the service. In the context of describing semantic Web services, these properties need to be expressed as ontologies that can be integrated with ontological representation frameworks for Web services for e.g. OWL-S. In this paper we present “TeSCO-S”, a framework for enriching Web service interface specifications, described as OWL ontologies with temporal assertions. The TeSCO-S model is based on Interval Temporal Logic (ITL), our underlying formalism for reasoning about service behaviour over periods of time. TeSCO-S provides an OWL ontology for specifying properties in ITL, a pre-processor, “OntoITL” for transforming ontology instances into ITL formulae and an interpreter, “AnaTempura” that executes and validates temporal properties expressed in “Tempura”, an executable subset of ITL.
Traditionally, Web services have been thought of and designed as being
information-intensive, transformational systems. In order to fully utilise the
distributed nature of control provided by interactive services deployed on the
web, a change in the paradigm is desired. Web services may provide and
transform information, but they may also exert control over their environment,
facilitate behaviour, prevent behaviour and facilitate communication. Consider
a typical example of a flight reservation service. The service provides results
for a flight search and reserves tickets for the selected flight, thus changing
the status of a seat from unbooked to booked i.e. transforming information
by execution of a database query. However, the final selection of flight by a
travel agent can span over an unlimited period of time, going through several
rounds of selection. A typical interaction is shown in fig. 1. The service may
also exert control over the environment by terminating the user session after
pre-specified time limits of inactive sessions. Further, once a flight has been
booked, the agent also has the option of cancelling the booking within a
stipulated time period. From this and several related scenarios, we observe that
most useful Web services repeatedly act and react in interaction with their
environment without necessarily terminating. Their behaviour can be considered
analogous to an important class of systems called “Reactive systems” 1 [
h c r a e S s lt u s e R tilr e F s tl u s e R s lt u s e R tilr e F t c e l e S k o o B
ifrnoCm lecanC racehS
behaviours’ due to their continuous interaction with the environment. Their execution may last anywhere from a few minutes to a few months. Examples include, web services deployed and composed as e-commerce applications, where an order once placed may be cancelled, changed or put on hold because of unexpected conditions anytime before its fulfillment. In certain cases a refund may also be requested later if the service/product does not meet its specifications. In corporate e-businesses, it may not be a simple database query that generates a document, but an entire business process involving multiple partners. The final generation of the document may span several days. Web 1Reactive systems can be contrasted with transformational systems that take inputs, once in the beginning and produce outputs, once before terminating services deployed on wireless devices may take more than expected time to provide the requested service due to poor connection facilities. In general, reactive services are required to satisfy real time constraints in response to the behaviour of the environment. For e.g. the database of the flight reservation service must be updated fast enough for all requests to be considered in a timely manner. Reactivity emerges when services communicate to form networks or compositions. For a service executing as part of a network, the environment is composed of all other services executing in that network. Further, Web services are perceived as black boxes where the internal computation of a process is not known. Reactive behaviour therefore needs to be specified, both at the abstract and declarative level as part of the service description.
An important aspect of reactive Web service specification is the representation of properties/rules that enable/constrain the behaviour of services and their continuous interactions with other services i.e. properties that are temporal in nature. High level description of services need to be enriched with properties which would enable reasoning about “ongoing” service behaviour. The properties need to be specified in a declarative form that is consistent with the language used for describing other aspects of the service. In the context of describing semantic Web services, these properties need to be expressed as ontologies that can be integrated with ontological representation frameworks for Web services. We observe that current Web service description frameworks suffer from the lack of their ability to fully specify properties that enable reasoning about reactive service behaviour and proving their correctness.
The need for more expressive service specification also becomes evident,
while reasoning about the composition of services and validation of the
composition at runtime. Model checking [12] and theorem proving are commonly
used techniques for formal verification. In the context of analysing services
and their composition at runtime, these techniques are not feasible due to the
possible exponential growth in the number of reachable global states. In
contrast to formal verification, practical validation techniques provide a
mechanism to verify only properties which are of interest to the service requester or
provider. Our notion of validation is different from the classical technique of
“testing”, generally associated with it. We believe, validation is a process of
checking for inconsistent, redundant, incomplete or incorrect properties for a
service. Properties are checked not for all possible behaviours [30] as in
verification, but for a particular trace or execution of a service. As shown in our
earlier work on service composition [
In this paper we propose a methodology to augment the semantic
description of a reactive service, with temporal properties that provide the required
support for reasoning about “ongoing” behaviour. The properties are specified
in Interval Temporal Logic (ITL) [
The paper is organised as follows: We begin by presenting a motivating example of an e-Bookshop in section 2, which we follow throughout the paper, to explain vital concepts and constructs. Section 3 briefly discusses ITL, as our formal model for TeSCO-S. Section 4 provides a detailed presentation on TeSCO-S and its architecture. Section 5 discusses the relationship of TeSCO-S with existing standards and finally section 6 outlines conclusions and ongoing work. 2.
The e-Bookshop as shown in fig 2 is a sequential composition of four services: Book search, Book buy, Payment validation and Book delivery. Each of these services is a reactive service, as they continuously interact with the customer. The e-Bookshop requires the customer to be registered with the service, in order to search or buy a book. The customer sends the ISBN number of the book to the Book search service, which returns a message with the search results. The customer can continue searching for more books, always supplying the ISBN number or proceed to buy the book. The Book buying service, takes as input the list of books selected by the customer, the delivery address and the credit card details. The Card details and address are passed to the Payment validation service. If the card is validated, then depending on the amount paid and mode of delivery selected (standard or express), the book is arranged to be delivered to the customer. We informally define properties of the composition, some of which we formalise in the subsequent sections. We perceive Web services as black boxes and hence the properties strictly characterise the observable behaviour of services in the composition.
At all times during the execution of the composed service, the customer is required to be a registered member of the e-Bookshop. This is a useful property to validate, when an inactive customer session is activated after a considerable period of time. Most services store customer regis
User Agent
tration details as session data, which is reset after a predefined period of inactivity.
Once a customer starts searching for a book, the price of the book has to be constant till the search is over or if the customer buys the book, the price has to be constant till the book has been delivered to the customer. During the search, at any time if the customer sends an ISBN number, he gets back the search results, for the same ISBN number. Once a book or a list of books have been selected and ordered, the parameters of the book (title, language etc) should not change, till the book has been delivered to the customer.
In order to buy a book, the customer needs to have a valid credit card. Once the credit card has been validated, the e-Bookshop makes a commitment to deliver the book as per the delivery terms and conditions agreed with the customer. 3.
In this section we present the formal framework underlying TeSCO-S. We base our work on Interval Temporal Logic (ITL) and its executable subset Tempura. Our selection of ITL is based on a number of points. It is a flexible notation for both propositional and first-order reasoning about periods of time. Unlike most temporal logics, ITL can handle both sequential and parallel composition and offers powerful and extensible specification and proof techniques for reasoning about properties involving safety, liveness and projected time. Timing constraints are expressible and furthermore most imperative programming constructs can be viewed as formulas. Tempura, an executable subset of ITL, provides a framework for developing, analysing and experimenting with suitable ITL specifications.
An interval is considered to be a (in)finite sequence of states, where a state is a mapping from variables to their values. An interval σ in general has a length |σ | ≥ 0 and a nonempty sequence of |σ | + 1 states σ 0 . . . σ |σ |. Thus the smallest intervals have length 0 i.e. one state.
The syntax of ITL is defined below where μ is an integer value, a is a static variable (doesn’t change within an interval), A is a state variable (can change within an interval), v a static or state variable, g is a function symbol and p is a predicate symbol. ITL contains conventional propositional operators such as
Expressions e ::= μ | a | A | g(exp1, . . . , expn) f ::=
Formulae p(e1, . . . , en) | ¬f | f1 ∧ f2 | ∀v q f | skip | f1 ; f2 | f ∗ ∧, ¬ and first order ones such as ∀ and =. There are temporal operators like “; (chop)”, “* (chopstar)” and “skip”. Additionally in ITL, there are temporal operators like (next) and (always). Expressions and formulae are evaluated relative to the beginning of an interval.
The informal semantics of the most interesting temporal constructs are defined as follows: skip : unit interval (length 1).
The formula skip has no operands and is true on an interval iff the interval has length 1 (i.e. exactly two states). skip : σ • 0 σ • 1 f1; f2 : A formula f1; f2 is true on an interval σ with states σ 0 . . . σ |σ | iff the interval can be “chopped” into two sequential parts (i.e. a prefix and a suffix interval) sharing a single state σ k for some k ≤ | σ | and in which the subformula f1 is true on the left part σ 0 . . . σ k and the subformula f2 is true on the right part σ k . . . σ |σ |. f ∗ : A formula f ∗ is true over an interval iff the interval can be chopped into zero or more sequential parts and the subformula f is true on each. Figure 4 pictorially represents the semantics of skip, chop and chopstar. Some ITL formula together with intervals which satisfy them are shown in fig 5
Some of the frequently used abbreviations are listed in Table 5. We do
not present the formal semantics of ITL, due to lack of space. We refer the
interested reader to [
We now formalise some of the interesting properties of the e-Bookshop service from section 2. The temporal properties that are required to hold at various f =b skip ; f next more =b true non-empty interval empty =b ¬more empty interval ♦f =b finite ; f sometimes
f =b ¬♦¬f always fin f =b (empty ⊃ f ) final state ♦if =b f ; true some initial subinterval i f =b ¬( ♦i¬f ) all initial subintervals ♦af =b finite ; f ; true some subinterval a f =b ¬( ♦a¬f ) all subintervals stages of the composition are as shown in fig 6. We also define the interval over which the properties are required to hold.
At all states (σ 0 . . . σ l) during the execution of the composed service, the customer is required to be a registered member of the e-Bookshop.
(isRegistered(userID)) Once a customer starts searching for a book, the price of any book returned as a result has to be constant till the search is over or if the customer buys the book, the price has to be constant till the book has been delivered to the customer i.e. the price of the book has to be constant at all states (σ 0 . . . σ l).
(isN otChanged(bookP rice)) During the search (σ 0 . . . σ m), at any state if the customer sends an ISBN number, he gets back the search results, for the same ISBN number in the next state.
((searchBook(ISBN )) ⊃
(searchResults(ISBN ))) Once a book or a list of books have been selected and ordered, the parameters of the book (title, language etc) should not change, till the book has been delivered to the customer (σ m . . . σ l).
(isBook(selectedBook)) In order to buy a book, the customer needs to have a valid credit card. that stays valid atleast till the book has been delivered to the customer
User Agent BookSearch
BookBuy Card Validation Book Deliver 0 m n k l □ (searchBook(ISBN) ⊃ searchResults (ISBN)) Temporal Properties □isRegisteredCustomer(userID) □isBook(SelectedBook) □validCard(cardNumber) keep (¬ receivePayment(BookPrice,UserID)) ∧ (fin receivePayment(BookPrice, UserID)) (fin validCard(UserID, CardNumber)) ; □ (DeliveryPeriod = CalculatedDays) □isNotChanged(BookPrice) Once the credit card has been validated, the e-Bookshop makes a commitment to deliver the book as per the delivery terms and conditions agreed with the customer (σ n . . . σ l).
(f in validCard(U serI D, CardN umber));(DeliveryP eriod = CalculatedDays) 3.2
Assumption-Commitment properties for Web services
An important class of tempoal properties for Web services are
“Assumptioncommitment” properties. In our earlier work [
We have also proposed compositional proof rules based on assumptioncommitment properties that allow validation of ongoing behaviour of services. Keeping in perspective the e-Bookshop service which is sequentially composed, we present the rules here for sequential composition.
S1 ;S2 S1
S2 ω1 ω1' ⊃ ω2
ω2'
(As, Co) : {ω}S{ω0 }
A Service, S, in ITL is expressed as a quadruple
where,
ω : state formula about initial state
As : a temporal formula specifying properties about the environment
Co : a temporal formula specifying properties about the service
ω0 : state formula about final state
We consider the sequential composition (ref. Fig. 7) of two services, S1 and
S2. For a detailed explanation of the rules and its proof obligations, the
interested reader is referred to [
` ` ` ` ` ` (As, Co) : (As, Co) : ω10 ⊃ As ≡
Co ≡ (As, Co) : {ω1}S1{ω10} {ω2}S2{ω20} ω2 a As Co∗ {ω1}S1; S2{ω20} (1) (2) (3) (4) (5) (6) 4.
TeSCO-S: Temporal SemantiCs for OWL enabled
Services
TeSCO-S is a framework (ref. Fig.8) for semantically annotating and validating Web service specifications with temporal properties, defined using ITL and its executable subset “Tempura”. The objective is: to provide an ontology for service providers to declaratively specify temporal properties in ITL. to provide a pre-processor for service requesters/composing middleware/software agents to process the declarative markup of properties and transform them into concrete ITL/Tempura formulae. to provide an execution engine for the generated tempura formulae, which can be used to validate properties about the service as well as perform runtime validation of assumption - commitment properties for service composition.
The semantics of the formulae and expressions modeled using TeSCO-S are the semantics as defined in ITL and implemented in its executable subset Tempura. TeSCO-S uses OWL as the ontology representation language. The choice of OWL as a representation format over XML is motivated by two objectives: (a) Our ultimate goal is to be able to automate reasoning about ITL formulae and expressions. (b) we want to be able to seamlessly use the ontology within standrads like OWL-S for services. Tools for reasoning about ITL-Tempura ontology, can be integrated with automated reasoning tools for services specified in OWL. For realising the objectives highlighted above, TeSCO-S includes the following components:
An OWL ontology for first order formulae, expressions and temporal constructs as defined in ITL and Tempura.
A pre-processor that transforms ontological representations of ITL and Tempura constructs defined in the ontology above to concrete formulae and expressions.
An interpreter,“AnaTempura” that provides execution support for Tempura.
Ontology for ITL and Tempura Concrete ITL./Tempura
OntoITL pre-processor for ITL and
Tempura Ontologies
AnaTempura execution and validation engine
Validation
Result Tcl/TK Interface
Validation
Result
TeSCO-S
Architecture The following sections present a detailed discussion of each of these components. 4.1
The objective of the ITL-Tempura ontology is to express the syntactical framework of ITL and Tempura, as concepts and properties in OWL. ITL is very expressive and provides a number of primitive and derived constructs for the specification of a wide variety of temporal assertions. We have restricted the ontology to only a specific set, which we believe will be most useful and sufficient to express the kind of properties that most service providers would want to expose. On the other hand, the ontology itself is very modularly structured to enable future extensions. As discussed in section (3), the syntax of ITL is defined primarily by Expressions and Formulae. Expressions can be of various types for e.g. static and state variables, functions, and constants. Similarly formulae can be subclassed as being atomic: e.g. “skip”,composite: e.g. “f1 ; f2” and predicates: e.g. “isRegistered(userID)“ amongst others. Expressions and Formulae in the ontology are built incrementally. The root class of all Formulae is “Formula”, while that of Expressions is “Expression”. Formula has several subclasses such as “Atomic”, “Composite” and “Prefixed” amongst others.“TempuraFormula”, defines formulae specified in Tempura and which can be executed by AnaTempura. “Operator” denotes the kind of operators that can be used with formulae and expressions. Classes have properties and restrictions associated that define the kind of parameters that are required to build the expression or formula. Properties provide the link between expressions/formulae and operators. We follow an incremental approach to building ontology instances using the ITL-Tempura ontology as shown in the e-Bookshop example presented in secton 4.2. The modular approach to building ITL and Tempura formulae allows reusability of formulae and expression instances between ontologies.
We use the Protege OWL plugin [4] for modelling the ontology. Table 4.1
shows how formulae and expressions are structured. A complete description
of the ontology is beyond the scope of the paper. A graphical and hierarchical
representation of the classes in the ontology can be found at [
ITL-Tempura Ontology::=
Formula::= Expression::=
Operator::= TemporalOperator::=
Formula | Expressions | TempuraConstuct Connective | Operator | Quantifier Atomic | TempuraAtomic | Equality | Composite | CompositeWithExpressions | Len | Negated | Prefixed | PrefixedWithExpressions Predicate | Quantified | Suffixed | StateVariable | StaticVariable | Constant | Function | CompositeExpresions | MathFunc | NextExpression | PrefixExpression EqualityOperator | TemporalOperator
InfixOpeartor | PrefixOperator | SuffixOperator
In this section, we model some interesting properties of the e-Bookshop service 3.1 using the ITL-Tempua ontology. Since most of the properties are composite formulae, we begin by defining the “Composite” formula class in the abstract Description Logic (TBox) syntax 2. 2For brevity and readability purposes, we have abstained from providing the actual ontological representation. The syntax has been specified here as abstract Description Logic syntax. For more details, please refer to the ontology
Composite v Formula u (∀ hasPrefixedSubFormula.Formula) u (∀ hasSuffixedSubFormula.Formula) u (=1 hasInfixOperator.Operator) u (=1 hasPrefixedSubFormula.Formula) u (=1 hasSuffixedSubFormula.Formula) We choose the following properties from the e-Bookshop example
Property (1): During the search, at any state if the user sends an ISBN number, he gets back the search results, for the same ISBN number in the next state.
((searchBook(ISBN )) ⊃ We define the properties as assertional axioms (ABox) in Description Logic. We build the formula incrementally as shown below: ABox representation of Property (1): ISBN:StateVariable, P1:Predicate, P2:Predicate (P1, searchNook):hasName, (P1, ISBN):hasExpressionList (P2, searchResults):hasName, (P2, ISBN):hasExpressionList PR1:Prefixed, (PR1, Next):hasPrefixOperator, (PR2, P2):hasSubFormula C1:Composite, (C1, Imp):hasInfixOperator (C1,P1):hasPrefixedSubFormula, (C1, PR1):hasSuffixedSubFormula PR2:Prefixed, (PR2, Always): hasPrefixOperator, (PR2, C1):hasSubFormula Property (2): Once the credit card has been validated, the e-Bookshop makes a commitment to deliver the book as per the delivery terms and conditions agreed with the user. (f in validCard(U serID, CardN umber));(DeliveryP eriod = CalculatedDays) ABox representation of Property (2): UserID:StateVariable, CardNumber:StateVariable DeliveryPeriod:StateVariable, CalculatedDays:StateVariable P1:Predicate, (P1, validCard):hasName, (P1, (UserID,CardNumber)):hasExpressionList PR1:Prefixed, (PR1, fin):hasPrefixOperator, (PR2, P1):hasSubFormula EQ1:Equality, (EQ1, Equals):hasEqualityOperator, (EQ1, DeliveryPeriod):hasPrefixExpression (EQ1, CalculatedDays):hasSuffixExpression C1:Composite, (C1, Chop):hasInfixOperator (C1,P1):hasPrefixedSubFormula, (C1, EQ1):hasSuffixedSubFormula 4.3
OntoITL: A pre-processor for Temporal Ontologies
So far, we have seen how ITL formulae and expressions can be modelled using the ITL-Tempura ontology. This enables service providers to specify temporal constraints as part of their service specification. In order to interpret this semantic markup of temporal properties, a utility is needed to generate concrete formulae and expressions from the OWL representation. The idea behind providing such a tool is to automate the process of generating, interpreting and analysing temporal properties of services. Service requestors and composers can use the tool to extract temporal properties that they would like to validate, while interacting with the service. At runtime, the properties are monitored against the behaviour of the interacting services.
OntoITL is a pre-processor that generates concrete ITL and executable Tempura formulae from instance ontologies built using the ITL-Tempura Ontology. The instances are defined using the core ontology as described in Section 4.1 or from ontologies that import these instances. It provides as output, complete information about instances of State and Static variables, Expressions, Formulae and Temporal Formulae modeled in the ontology. An output of the preprocessor for properties of the e-Bookshop, modeled using the ITL-Tempura Ontology and as explained in section 4.2 is shown in the Fig. 9: OntoITL takes as input, the instance ontology in OWL for a formula or a set of formulae. It then generates ITL/Tempura formulae keeping the syntactical structure of the formula intact. OntoITL offers several options to store the generated ITL and Tempura formulae. It also provides the facility to directly pass the tempura formula to the AnaTempura interpreter, that executes the formulae and validates temporal properties. Alternatively, OntoITL stores the generated outputs in files that can be executed via the Tcl/Tk interface of AnaTempura as discussed in section 4.4. 4.4
AnaTempura: Runtime Validation of Tempura specification
AnaTempura (available from [
An overview of the run-time analysis process in AnaTempura is depicted in Fig. 10. There are two ways of validating properties via AnaTempura:
The OntoITL pre-processor for ITL-Tempura Ontology
Properties (Tempura Code)
Concrete Tempura formulae generated by the OntoITL pre-processor are directly passed to AnaTempura. The results of the validation and execution are returned to OntoITL for display.
Concrete Tempura formulae generated by the OntoITL pre-processor are stored in files for validation at a later stage. The results of the validation and execution can be displayed via the Tcl/Tk interface of AnaTempura. AnaTempura generates a state-by-state analysis of the system behaviour as the computation progresses. At various states of execution, values for variables of interest are passed from the system to AnaTempura. The Tempura properties are validated against the values received. If the properties are not satisfied AnaTempura indicates the errors by displaying what is expected and what the current system actually provides. The approach goes beyond a “keep tracking” approach, i.e. giving the running results of certain properties of the system, by not only capturing the execution results but also comparing them with formal properties. The general architecture that employs AnaTempura for validation of service properties is shown in Fig. 11. The validation results of the instanceOntology for ITL and Tempura
Instance Ontologies Concrete ITL./Tempura
OntoITL preprocessor for ITL and
Tempura Ontologies
AnaTempura execution and validation engine ontology-formulae, generated from the TeSCO-S framework, can be returned to the composing agents, the middleware or to the service requestor depending on the design of the service composition.
eBookshop
Validating the Customer : e-Bookshop Composition We have validated some of the properties of the e-Bookshop as formalised in section 3.1. We present the validation of one such property,
(isRegistered(U serID) We adopt the second approach to validating properties as mentioned in section 4.4. The property is extracted as a tempura formula, from its ontological representation using the OntoITL pre-processor and stored in a file. At the initial state, the customer registers using his login details 3. The login details are set for the customer session and passed to AnaTempura. For each isRegistered(userID)
isRegistered(userID) Book Search phase of the composition (search, buy etc.) and for every interaction between the e-Bookshop and the customer, at any state, the property is validated by AnaTempura against the values set in the session for that state. If the values in the session are found to be reset and do not match the ones passed to AnaTempura in the initial state, a warning message is sent to the e-Bookshop as shown in fig. 12. It is worth noting that AnaTempura only validates the properties of interest. It does not define the behaviour of the service in case the properties are not satisfied. This is a design decision that has to be taken before the composition is realised. 3For practical purposes, we do not model the registration process over an interval, although this may well be the case if the user enters incorrect login details, and takes several attempts to correct login.
Based on service interfaces definitions [
TeSCO-S provides an OWL ontology for modelling temporal properties of services and a tool to validate them. In our earlier work, we have shown how temporal properties for services can be declaratively specified in SWRL. The ITL-Tempura ontology provides richer expressiveness in the specification of properties due to more concepts and properties being available. It can be integrated very easily with SWRL and with existing Web service standards that describe service interfaces in OWL. As an example, the definition of “StateVariable ” can be extended to define it as a SWRL variable. Similarly “head” and “body” atoms can be defined in terms of “Predicate” in the ITL ontology. Temporal properties that define execution monitoring of OWL-S services can be readily defined as Tempura formulae, which AnaTempura validates at runtime.
In this paper, we provide a modular approach, TeSCO-S, to building and executing temporal properties of services, with interfaces described as OWL ontologies. TeSCO-S is based on Interval Temporal Logic (ITL) and Tempura, its executable subset. Our pre-processor “OntoITL” enables transformation of the bulky XML representation of temporal properties into concrete ITL and Tempura formulae, that can be handled readily by AnaTempura. The ontology within the TeSCO-S framework can be used by service providers to describe temporal capabilities of services. Service requestors and composing agents can use “OntoITL” and AnaTempura for on-the-fly transformation and validation of these temporal properties. The ontology provides constructs not only for specifying temporal expressions and formulae, but general first order predicates and formulae as well. It can therefore, also be used to specify preconditions/post-conditions and effects in frameworks like OWL-S and WSMO. Ongoing work in TeSCO-S is providing reasoning support over temporal ontologies and tools for exploiting ITL formulae to build temporal ontologies. It is planned to have a protege plugin for defining temporal ontologies, that could be used along with the OWL-S editor for modelling OWL-S services. [4] The protege ontology editor and knowledge acquisition system. [5] Simple Object Access Protocol.
http://www.w3.org/TR/2002/CR-soap12-part0-20021219/. [6] The Rule Markup Initiative.
http://www.dfki.uni-kl.de/ruleml/. [7] OWL Web Ontology Language http://www.w3.org/TR/owl-ref/.
Reference, 10
February 2004. [8] A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems - a survey of current trends. Current trends in Concurrency, LNCS 224:510–584, 1986. [9] F. Bry and S. Spranger. Temporal constructs for a web language, 2003. [10] Dr. Frank Leymann, IBM Software Group. Web Services Flow Language (WSFL) Version 1.0, 2001. [11] Drew McDermott and Dejing Dou . Representing Disjunction and Quantifiers in RDF
Embedding Logic in DAML/RDF. International Semantic Web Conference, 2002. [12] E.M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999. [13] Ian Horrocks, Peter F. Patel-Schneider, Harold Boley, Said Tabet, Benjamin Grosof, Mike Dean. SWRL: A Semantic Web Rule Language Combining OWL and RuleML . Technical report, Version 0.5 of 19 November 2003. [14] Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems:
Specification. Springer-Verlag, New York, 1991. [15] Z. Manna and A. Pnueli. The Temporal Verification of Reactive Systems: Safety. Springer
Verlag, New York, 1995.
Release., 2004.