Here is Michael Kifer's example:
 	     To buy a product, pay a fee to the broker and the cost of the
             product to the seller. These steps can be done in parallel:

                transfer(Fee,Buyer,Broker) | transfer(Cost,Buyer,Seller)

             This can be regarded as a composition where the same service
             (money transfer) is invoked twice. We can elaborate on this
             service as follows (where "," denotes sequential composition):

                transfer(Amount,Account1,Account2) :-
                     withdraw(Amount,Account1), deposit(Amount,Account2).
                     balance(Account,Balance), Balance >= Amount, % Precondition
                deposit(Amount,Account) :-
                     balance(Account,Balance), Amount >= 0, % Precondition
                change_balance(Account,Balance1,Balance2) :-
What follows is an equivalent set of process descriptions using PSL.

These activities are specified as terms:

(forall (?x) (activity (buy_product ?x)))
(forall (?x ?y ?z) (activity (transfer ?x ?y ?z)))
(forall (?x ?y) (activity (withdraw ?x ?y)))
(forall (?x ?y) (activity (deposit ?x ?y)))
(forall (?x ?y ?z) (subactivity (transfer ?x ?y ?z) (buy_product ?y)))
(forall (?x ?y ?z) (subactivity (withdraw ?x ?y) (transfer ?x ?y ?z)))
(forall (?x ?y ?z) (subactivity (deposit ?x ?z) (transfer ?x ?y ?z)))
The process description for buy_product is:
(forall (?occ)
	(implies  (occurrence_of ?occ (buy_product ?Buyer))
		  (exists (?occ1 ?occ2 ?Fee ?Cost ?broker ?Seller)
			(and	(occurrence_of (transfer ?Fee ?Buyer ?Broker))
				(occurrence_of (transfer ?Cost ?Buyer ?Seller))
				(subactivity_occurrence ?occ1 ?occ)
				(subactivity_occurrence ?occ2 ?occ)))))
The process description for transfer is:
(forall (?occ)
	(implies  (occurrence_of ?occ (transfer ?Amount ?Account1 ?Account2))
		  (exists (?occ1 ?occ2 ?occ3)
			(and	(occurrence_of ?occ1 (withdraw ?Amount ?Account1))
				(occurrence_of ?occ2 (deposit ?Amount ?Account2))
				(subactivity_occurrence ?occ1 ?occ)
				(subactivity_occurrence ?occ2 ?occ)
				(leaf_occ ?occ3 ?occ1)
				(min_precedes ?occ3 (root_occ ?occ2))))))
The axiomatization of the next set of activities requires a little more information, since there is some ambiguity about which activities are subactivities of others.

Option 1:

(forall (?x ?y ?z) (activity (change_balance ?x ?y ?z)))

(subactivity (change_balance ?Account ?Balance1 ?Balance2)
	     (deposit ?Amount ?Account))

(subactivity (change_balance ?Account ?Balance1 ?Balance2)
	     (withdraw ?Amount ?Account))
In this case, deposit and withdraw are conditional activities:
(forall (?occ)
   (implies  (and	(occurrence_of ?occ (withdraw ?Amount ?Account))
			(prior (balance ?account ?Balance) (root_occ ?occ))
			(greaterEq ?Balance ?amount))
	     (exists (?occ1)
		(and	(occurrence_of ?occ1 (change_balance ?account ?Balance 
					     (plus ?Balance ?Amount)))
			(subactivity_occurrence ?occ1 ?occ))))
The effects of change_balance are:
(forall (?occ)
   (implies  (and   (occurrence_of ?occ (change_balance ?Account ?Amount1 ?Amount2))
		    (leaf_occ ?occ1 ?occ))
	     (and   (holds (balance ?Account ?Amount2))
		    (not (holds (balance ?Account ?Amount1))))))

Option 2:

Changing the balance is actually an effect rather than a subactivity.
(forall (?occ)
	(implies  (and	(occurrence_of ?occ (withdraw ?Amount ?Account))
			(legal ?occ))
		  (and	(prior (balance ?account ?Balance) (root_occ ?occ))
			(greaterEq ?Balance ?amount))))
(forall (?occ ?occ1)
	(implies  (and	(occurrence_of ?occ (withdraw ?Amount ?Account))
			(leaf_occ ?occ1 ?occ))
		  (and	(holds (balance ?account (minus ?Balance ?Amount))
			(not (holds (balance ?account ?Balance)))))