Periodic Preconditions for Activities

Periodic Preconditions for Activities

Extension Name: periodic.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

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

Definitional Extensions Required by this Extension: occ_precond.def, time_precond.def, precond.def

Grammar: periodic.bnf

Definitions

Definition 1 An activity is periodic if and only if legal occurrences depend on the timepoints at which other activities occur. In particular, activity occurrences that are in the same orbit of occurrence tree endormorphisms are also in the same orbit of timeline automorphisms. 
(forall (?a) (iff (periodic ?a)
(forall (?s1 ?s2)
	(if	  (and	(occurrence_of ?s1 ?a)
			(occurrence_of ?s2 ?a)
			(begin_equiv ?s1 ?s2)
			(tree_equiv ?s1 ?s2))
		  (legal_equiv ?s1 ?s2)))))
Definition 2 An activity is intermittent if and only if legal occurrences depend on the timepoints at which other activities occur. In particular, there exist activity occurrences that are in the same orbit of occurrence tree endormorphisms and that are also in the same orbit of timeline automorphisms. 
(forall (?a) (iff (intermittent ?a)
(exists (?s1)
	(and	(occurrence_of ?s1 ?a)
		(forall (?s2)
			(if	  (and	(occurrence_of ?s2 ?a)
					(begin_equiv ?s1 ?s2)
					(tree_equiv ?s1 ?s2))
				  (legal_equiv ?s1 ?s2)))))))
Definition 3 An activity is aperiodic if and only if there is no relationship between legal occurrences and the timepoints at which other activities occur. In particular, the only occurrence tree endomorphism that preserves the beginof other activity occurrences is the trivial one. 
(forall (?a) (iff (aperiodic ?a)
(forall (?s1)
	(if	  (occurrence_of ?s1 ?a)
		  (exists (?s2)
			(and	(occurrence_of ?s2 ?a)
				(begin_equiv ?s1 ?s2)
				(tree_equiv ?s1 ?s2)
				(not (legal_equiv ?s1 ?s2))))))))