Temporal Logic

Topics
	Environment classes for atomic propositions
	Essential Temporal Logic Types
	Input and Output of Formulas
	Rewriting Algorithms for Formulas
	Algorithms related to the temporal hierarchy
	Miscellaneous Algorithms for Formulas

Detailed Description

Spot supports the future-time fragment of LTL, and the linear-time fragment of and PSL formulas. The former is included in the latter. Both types of formulas are represented by instances of the spot::formula class.