AT4WS09 slide-6

Planning Assumptions

The plan consists of a partial order of service calls: states ordered by the relation subsequent: <. Let (p=a,S) denote that property p has value a in state S.

Let service WS be called in state S_i, and return in state S_f.

∀ p, (input WS p) ∃ a, (p=a, S_i)

∀ p, (Output WS p a), (p=a,S_f)

(Subseqent S_i S_f): S_i < S_f

No spoiling and persistance frame assumptions:
(p=a,S_k) ⇐ (p=a,S_i) ∧ (S_i < S_k) ∧ ¬ ∃ S_j, (p=b,S_j), S_i < S_j ≤ S_k.

Constraints: Service-specific or global conditions restrict property values and service calls in state sequences.
Preferences: Some property values and service calls in some state sequences are preferred.
Meta-Constraint: ¬ ( (p=a, S) ∧ (p=b, S)) .
I.e., properties are single-valued in a state.