Formalization of Service A subclass of Action: W(P,E) with additional property relations:

• Provider of a service takes a value of type Agent.
• Caller (consumer) of a service takes a value of type Agent.
• Known is a special fluent that is true when an agent knows its propositions are true in some state.
• Input and Output are special preconditions and effects, respectively, with the fluent Known.
  Designated Input(W) ∈ P(W) and Output(W) ∈ E(W)
• Sent is a relation such that
  (Sent (W, S_i, Agent₁, Agent₂, Input(W)))
  is true after the caller Agent₁ has signaled in State S_i to the Provider Agent₂ that
  the service W should be performed using information from Input(W).
• Received is a relation such that
  (Received (W, S_i, Agent₁, Agent₂, Output(W))
  is true after the provider Agent₂ has signaled in State S_j to the Caller Agent₁ that
  the service W has been performed and provided the knowledge Output(W).
• Inputs and Outputs may be defined as null for a service.
• S_i=S_p < S_j=S_e

Two services that have identical P,E (including I,O) are identical,
except when the Providers have been instantiated and are different.

---

---

©2012 Charles Petrie - permission to reproduce widely with attribution.