Skip to content

new LTL simplification rules

the following two rules generalize the two rules in the rightmost column of section 5.4.2

f M u = Ff & u
f W e = Gf | e

the following two rules are new

q R Xf = X(q R f)
q U Xf = X(q U f)