A linear_temporal_logic formula is used to specify behavioral properties about a system. (see Temporal_logic_in_finite-state_verification).

See also HowToParseLtlFormulae written using the LtlSyntax in Spot.

LtlFormula (last edited 2012-06-02 09:55:26 by AlexandreDuretLutz)

All text is available under the terms of the GNU Free Documentation License, see SpotWikiLicense for details.