Time-based Effects of Activities

Time-based Effects of Activities

Extension Name: time_effects.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

Theories Required by this Extension: disc_state.th, occtree.th, psl_core.th

Definitional Extensions Required by this Extension: effects.def, start.def, state_precond.def

Grammar: time_effects.bnf

Definitions

Definition 1 An activity is a temporal effect activity iff whenever any two occurrences of the activity agree on their beginof timepoints, then they agree on the effects (i.e. the states that hold after the occurrence. 
 
(forall (?a) (iff (temporal_effects ?a)
(forall (?s1 ?s2)
	(if	  (and	(occurrence_of ?s1 ?a)
			(occurrence_of ?s2 ?a)
			(begin_equiv ?s1 ?s2))
		  (effects_equiv ?a ?s1 ?s2)))))
Definition 2 An activity is a partially time effects activity if and only if there exist effect-preserving timeline automorphisms. 
(forall (?a) (iff (partial_temporal ?a)
(and    (exists (?s1)
                (forall (?s2)
                        (if	  (begin_equiv ?s1 ?s2)
				  (effects_equiv ?a ?s1 ?s2))))
        (exists (?s3 ?s4)
                (and    (begin_equiv ?s3 ?s4)
                        (not (effects_equiv ?a ?s3 ?s4)))))))
Definition 3 An activity is a rigid time effects activity if and only if the only effects-preserving timeline automorphism is the trivial one. 
(forall (?a) (iff (nontemporal ?a)
(forall (?s1)
        (exists (?s2)
                (and    (begin_equiv ?s1 ?s2)
                        (not (effects_equiv ?a ?s1 ?s2)))))))