This is Appendix B of the Semantic Web Services Ontology (SWSO) document.
This appendix contains the axiomatization of the First-order Logic Ontology for Web Services (FLOWS) process model, expressed in SWSL-FOL. FLOWS is also known as SWSO-FOL. The hyperlinked concept and relation names refer to concepts and relations defined in the Process Specification Language (PSL).
Every service is associated with an activity.
forall ?s (service(?s) ==> exists ?a (service_activity(?s,?a))).
A service activity is an activity in the PSL Ontology.
forall ?s,?a
(service_activity(?s,?a) ==>
activity(?a)).
A service occurrence is an occurrence of the activity that is associated with the service.
forall ?s,?o ((service_occurrence(?s,?o) and occurrence_of(?o,?a)) ==> service_activity(?s,?a)).
An AtomicProcess is equivalent to a primitive activity in the PSL Ontology such that its preconditions and effects depend only on the fluents that hold prior to the an occurrence of the activity.
forall ?a
(AtomicProcess(?a) <==>
(primitive(?a) and
markov_precond(?a) and
(markov_effects(?a) or context_free(?a))).
If a fluent is an input to an activity, then the reference of the fluent must be known as a precondition for the activity to occur.
forall ?s,?a,?iofluent
((occurrence_of(?s,?a) and
legal(?s) and
input(?a,?iofluent)) ==>
prior(Kref(?iofluent),?s)).
If ?iofluent is an output to an activity that is conditional on the fluent ?f, then the effect of the activity occurrence when ?f holds prior to the activity occurrence is that the reference of ?iofluent is known.
forall ?s,?a,?f,?iofluent
((occurrence_of(?s,?a) and
legal(?s) and
prior(?f,s) and
output(?a,?f,?iofluent)) ==>
holds(Kref(?iofluent),?s)).
The following axioms define the epistemic fluents.
The K fluent represents the accessibility relation in the possible-world model of knowledge. An activity occurrence ?s1 is accessible from an activity occurrence ?s if as far as is known in ?s, ?s1 might have occurred.
forall ?a,?s,?s2
(occurrence_of(?s,?a) ==>
(holds(K(?s2),?s) <==>
exists ?s1
((?s2 :=: successor(?a,?s1)) and
legal(?s2) and
holds(K(?s1),?s) and
(SR(?a,?s) :=: SR(?a,?s1))))).
The Knows fluent holds if the K fluent holds at all accessible activity occurrences.
forall ?f,?s
(holds(Knows(?f),?s) <==>
forall ?sp
(holds(K(?sp),?s) ==> holds(?f,?sp))).
The fluent neg is used to reify negation for fluent terms.
forall ?f,?s
(holds(neg(?f),?s) <==> (neg holds(?f,?s))).
The Kref fluent holds whenever the reference of its argument is known.
forall ?f,?s
(holds(Kref(?f),?s) <==>
exists ?x
(holds(Knows(?f :=: ?x),?s))).
The composedOf relation is equivalent to the subactivity relation in the PSL Ontology.
forall ?a1,?a2
(composedOf(?a1,?a2) <==>
subactivity(?a2,?a1)).
An Split activity is equivalent to a strong_poset activity in PSL. The activity trees all have the same structure and each activity tree consists of branches that are in one-to-one correspondence with sequences of subactivity occurrences that satisfy the partial ordering constraints.
forall ?a
(Split(?a) <==>
(uniform(?a) and
exists ?occ
(occurrence_of(?occ,?a) and
neg simple(?occ) and
ordered(?occ) and
strong_poset(?occ)))).
An Sequence activity is equivalent to an activity in PSL whose activity trees all have the same structure and such that each activity tree consists of a unique branch.
forall ?a
(Sequence(?a) <==>
(uniform(?a) and
exists ?occ
(occurrence_of(?occ,?a) and
simple(?occ) and
rigid(?occ) and
ordered(?occ) and
strong_poset(?occ)))).
An Unordered activity is equivalent to an activity in PSL whose activity trees all have the same structure and such that each activity tree is a bag. In this case, there is a one-to-one correspondence between branches of the activity tree and all permutations of subactivity occurrences.
forall ?a
(Unordered(?a) <==>
(uniform(?a) and
exists ?occ
(occurrence_of(?occ,?a) and
bag(?occ)))).
A Choice activity is equivalent to an activity in PSL whose activity trees all have the same structure and such that each activity tree is nondeterministic (that is, each branch contains occurrences of different subactivities.
forall ?a
(Choice(?a) <==>
(uniform(?a) and
exists ?occ
(occurrence_of(?occ,?a) and
simple(?occ) and
rigid(?occ) and
unordered(?occ) and
choice_poset(?occ)))).
An IfThenElse activity is equivalent to a conditional activity in the PSL Ontology.
forall ?a
(IfThenElse(?a) <==>
conditional(?a)).
An Iterate activity is equivalent to an activity in the PSL Ontology whose occurrences are repetitive. Activity trees for this activity have different structure, depending on the cardinality of the repeated subtrees.
forall ?a
(Iterate(?a) <==>
activity(?a) and
(forall ?occ
(occurrence_of(?occ,?a) ==>
(repetitive(?occ) and
multiple_outcome(?occ)))).
A RepeatUntil activity is equivalent to a conditional activity in the PSL Ontology whose occurrences are repetitive. Activity trees for this activity have different structure, depending on the cardinality of the repeated subtrees.
forall ?a
(RepeatUntil(?a) <==>
activity(?a) and
(conditional(?a) and
forall ?occ
(occurrence_of(?occ,?a) ==>
(repetitive(?occ) and
multiple_outcome(?occ)))).
An Ordered activity is equivalent to an activity in PSL whose activity trees all have the same structure and such that each activity tree is ordered if and only if the branches contain occurrences of the same subactivities.
forall ?a
(OrderedActivity(?a) <==>
(uniform(?a) and
exists ?occ
(occurrence_of(?occ,?a) and
(ordered(?occ) <==> (neg simple(?occ))))).
An OccActivity is equivalent to an activity in PSL whose activity trees all have the same structure and such that each activity tree consists of subtrees whose branches contain occurrences of the same subactivities.
forall ?a
(OccActivity(?a) <==>
(uniform(?a) and
exists ?occ
(occurrence_of(?occ,?a) and
(permuted(?occ) or (nondet_permuted(?occ))))).
A TriggeredActivity is equivalent to a trigger activity in the PSL Ontology.
forall ?a
(TriggeredActivity(?a) <==>
trigger(?a)).
Messages are objects in the ontology.
forall ?m,?o,?msgtype
(message_info(?m,?msgtype,?x) ==> object(?m)).
A message is produced,read, or destroyed by an AtomicProcess.
forall ?o,?m,?a ((produces(?o,?m) or reads(?o,?m) or destroys(?o,?m)) and occurrence_of(?o,?a) ==> AtomicProcess(?a)).
For any occurrence that reads a message, the the reference of the input described by the message type is known after the occurrence.
forall ?o,?m,?msgtype,?x,?iofluent
((reads(?o,?m) and
message_info(?m,?msgtype,?x) and
described_by(?msgtype,?iofluent) and
legal(?o)) ==>
holds(Kref(?iofluent),?o)).
For any occurrence that produces a message, the reference of the output described by the message is known before the occurrence.
forall ?o,?m,?msgtype,?x,?iofluent
((produces(?o,?m) and
message_info(?m,?msgtype,?x) and
described_by(?msgtype,?iofluent) and
legal(?o)) ==>
prior(Kref(?iofluent),?o)).
Every activity occurrence that reads a message is preceded by an activity occurrence that produces the message.
forall ?o1,?m
(reads(?o1,?m) ==>
exists ?o2
(produces(?o2,m) and
precedes(?o2,o1))).
A message object is created by an activity occurrence that produces a message.
forall ?o,?m
(produces(?o,?m) ==>
((beginof(?m) :=: endof(?o)) and
holds(existing_mobject(?m),?o))).
A message object is destroyed by an activity occurrence that destroys a message.
forall ?o,?m
(destroys(?o,?m) ==>
((endof(?m) :=: endof(?o)) and
(neg holds(existing_mobject(?m),?o)))).
A ProduceMessage activity is an activity whose occurrences produce messages.
forall ?a
(ProduceMessage(?a) <==>
(activity(?a) and
(forall ?o
(occurrence_of(?o,?a) ==>
exists ?m
(produces(?o,?m))))).
A ReadMessage activity is an activity whose occurrences read messages.
forall ?a
(ReadMessage(?a) <==>
(activity(?a) and
(forall ?o
(occurrence_of(?o,?a) ==>
exists ?m
(reads(?o,?m))))).
A DestroyMessage activity is an activity whose occurrences destroy messages.
forall ?a
(DestroyMessage(?a) <==>
(activity(?a) and
(forall ?o
(occurrence_of(?o,?a) ==>
exists ?m
(destroys(?o,?m))))).
If a message is contained in a channel, then it is produced by an occurrence of a service that is a source for the channel.
forall ?c,?m (channel_mobject(?c,?m) ==> exists ?s,?o,?o1 (channel_source(?c,?s) and occurrence_of(?o,?s) and produces(?o1,?m) and subactivity_occurrence(?o1,?o))).
If a message is contained in a channel, then it is read by an occurrence of a service that is a target for the channel.
forall ?c,?m (channel_mobject(?c,?m) ==> exists ?s,?o,?o1 (channel_target(?c,?s) and occurrence_of(?o,?s) and reads(?o1,?m) and subactivity_occurrence(?o1,?o))).
Exceptions form a sublcass of fluents.
forall ?e (exception(e) ==> fluent(e)).
The following axioms capture the relationships in Figure 2.2.
An exception ?e is handled by an activity ?a.
forall ?a,?e (is_handled_by(?e,?a) ==> (activity(?a) and exception(?e))).
An activity ?a has an exception ?e.
forall ?a,?e (has_exception(?a,?e) ==> (activity(?a) and exception(?e))).
An activity ?a is an exception-handling activity if and only if it is a TriggeredActivity that there exists an exception that is handled by ?a.
forall ?a (handle_exception(?a) <==> exists ?e (is_handled_by(?e,?a) and TriggeredActivity(?a))).
find_exception and fix_exception are the two subclasses of exception-handling activities.
forall ?a (handle_exception(?a) <==> (find_exception(?a) or fix_exception(?a))).
detect_exception and anticipate_exception are the two subclasses of exception-finding activities.
forall ?a (find_exception(?a) <==> (detect_exception(?a) or anticipate_exception(?a))).
avoid_exception and resolve_exception are the two subclasses of exception-fixing activities.
forall ?a (fix_exception(?a) <==> (avoid_exception(?a) or resolve_exception(?a))).
The relation is_found_by is the restriction of the is_handled_by relation
to exception-finding activities.
The relation is_fixed_by is the restriction of the is_handled_by relation
to exception-fixing activities.
forall ?a,?e (is_handled_by(?e,?a) <==> ((is_found_by(?e,?a) and find_exception(?a)) or (is_fixed_by(?e,?a) and fix_exception(?a)))).
The relation is_detected_by is the restriction of the is_found_by relation
to exception-detecting activities.
The relation is_anticipated_by is the restriction of the is_found_by relation
to exception-anticipating activities.
forall ?a,?e (is_found_by(?e,?a) <==> ((is_detected_by(?e,?a) and detect_exception(?a)) or (is_anticipated_by(?e,?a) and anticipate_exception(?a)))).
The relation is_avoided_by is the restriction of the is_fixed_by relation
to exception-avoiding activities.
The relation is_resolved_by is the restriction of the is_fixed_by relation
to exception-resolving activities.
forall ?a,?e (is_fixed_by(?e,?a) <==> ((is_avoided_by(?e,?a) and avoid_exception(?a)) or (is_resolved_by(?e,?a) and resolve_exception(?a)))).