Formal Semantics of OWL-S with F-Logic

OWL-S provides Web Service providers with a core ontological framework and guidelines for describing the properties and capabilities of their Web Services in unambiguous and, computer-interpretable form. To support effective verification tools of OWL-S, a formal semantics of the language is highly desirable. In this paper we propose a declarative methodology based on F-logic for modeling OWL-S ontologies, present a formal F-logic semantics of OWL-S and specify their global properties and frame as F-logic formulas. This methodology allows us to bring to bear a body of work for using first order logic based model checking to verify certain global properties of OWL-S constructed service systems.