The Temporal Formula Editor

The editor for Temporal formulae is just a single-line text editing field. The QPTL is first advocated by Sistla in 1983. A QPTL formula is a PTL formula with propositional quantifiers. PTL here refers to the pure propositional version of linear temporal logic (LTL) as defined in Manna and Pnueli's book [1992]. Currently GOAL can handle a subset of the full QPTL formulae, namely those with quantifiers that do not fall in the scope of temporal operators. This subset is as expressive as the full set of QPTL formulae [Gabbay, Pnueli, Shelah, and Stavi, On the temporal analysis of fairness, POPL '80] [Gabbay, The declarative past and imperative future: Executable temporal logic for interactive systems, Temporal Logic in Specification, Springer, 1987]. To avoid excessive parentheses, every operator has a corresponding precedence. At the end of this help page are a few examples that show you how to specify a QPTL formula.

Quantifiers

Boolean Operators

Temporal Operators

There are two kinds of temporal operators: future operators and past operators.
Their input formats are shown below:

Future Operators

	Format 1	Format 2
Next	()	X
Eventually (Sometime)	<>	F
Henceforth (Always)	[]	G
Wait-for (Unless)	W
Until	U
Release	R

Past Operators

	Format 1	Format 2
Previous	(-)	Y
Before	(~)	Z
Once	<->	O
So-for	[-]	H
Since	S
Back-to	B

Operator Precedence

GOAL assumes the following binding precedence:
Unary Operator > Temporal Binary Operator > Boolean Binary Operator

Examples

• <> p or Fp
• []<> p or GFp or G(Fp)
• [](p--> <> q) or G(p-->Fq) or G(p--> (Fq))
• [](p--> <-> q) or G(p-->Oq) or G(p--> (Oq))
• [](~p \/ ()q) or G(~p \/ Xq) or G(~p \/ (Xq))
• []pSq or GpSq or (Gp)Sq
• [](p-->pSq) or G(p-->pSq) or G(p-->(pSq))
• E t : t /\ [] ((t --> p) /\ (t <--> () (~ t)))