Expand description
Restricted version of LTL expressions without negations and implications.
This module contains the logic to convert general LTL expressions into a more restricted form, which does not contain negations and implications.
Negations are pushed down to the atomic expressions, and implications are transformed into disjunctions.
This type is a more restricted version of LTL expressions, yet is equally expressive. Therefore, it is easier to work with and to implement algorithms for.
Enumsยง
- NonNegatedELTL
Expression - LTL Expression without negations and implications