Precedence Property Pattern

Intent

To describe relationships between a pair of events/states where the occurrence of the first is a necessary pre-condition for an occurrence of the second. We say that an occurrence of the second is enabled by an occurrence of the first.

Example Mappings

In these mappings P is the consequent and S is the enabling state/event.

CTL

S precedes P :

Globally	A[!P U (S | AG(!P))]
Before R	A[!P U (S | R | AG(!P) | AG(!R))]
After Q	A[!Q U (AG(!Q) | (Q & A[!P U (S | AG(!P))]))]
Between Q and R	AG(Q -> A[!P U (S | R | AG(!P) | AG(!R))])
After Q until R	AG(Q -> !E[(!R & !S) U (!R & P)])

LTL

S precedes P:

Globally	<>P -> (!P U (S & !P))
Before R	<>R -> (!P U (S | R))
After Q	[]!Q | <>(Q & (!P U (S | []!P)))
Between Q and R	[]((Q & <>R) -> (!P U (S | R)))
After Q until R	[](Q -> ((!P U (S | R)) | []!P))

Quantified Regular Expressions

Let "." be the set of all events symbols, let [- P,Q,R] denote the expression that matches any symbol except P Q and R and let e? denote zero or one instance of expression e.
S precedes P:

Globally	[-P]* | ([-S,P]*; S; .*)
Before R	[-R]* | ([-P,R]*; R; .*) | ([-S,P,R]*; S; .*)
After Q	[-Q]*; (Q; ([-P]* | ([-S,P]*; S; .*)) )?
Between Q and R	[-Q]*;
	(Q; [-P,R]* | ([-S,P,R]*; S; [-R]*) R; [-Q]*)*;
	(Q; [-R]*)?
After Q until R	[-Q]*;
	(Q; [-P,R]* | ([-S,P,R]*; S; [-R]*) R; [-Q]*)*;
	(Q; ([-P,R]* | ([-S,P,R]*; S; [-R]*)) )?

Examples and Known Uses

Precedence properties occur quite commonly in specifications of concurrent systems. One common example is in describing a requirement that a resource is only granted in response to a request.

Relationships

Note that a Precedence property is like a converse of a Response property. Precedence says that some cause precedes each effect, and Response says that some effect follows each cause. They are not equivalent, because a Response allows effects to occur without causes (Precedence similarly allows causes to occur without subsequent effects).

Note that this pattern does not require that each occurrence of a consequent will have its own occurrence of an enabling condition.