END fairctlops
Fair versions of CTL operators where fairAG(N, f)(Ff)(s) means f always holds along every N-path from s along which the fairness predicate Ff holds infinitely often. This is different from the usual linear-time notion of fairness where the strong form asserts that if an action A is enabled infinitely often, it is taken infinitely often, and the weak form asserts that if any action that is continuously enabled is taken infinitely often.
fairctlops
[state:TYPE]
:
THEORY
BEGIN
u:
VAR
state
v:
VAR
state
w:
VAR
state
CONVERSION+
K
conversion
fairEG(N,
f)(Ff):
pred[state]
=
nu(LAMBDA
P
:
EU(N,
f,
f
AND
Ff
AND
EX(N,
P)));
fairAF(N,
f)(Ff):
pred[state]
=
NOT
fairEG(N,
NOT
f)(Ff);
fair?(N,
Ff):
pred[state]
=
fairEG(N,
LAMBDA
u
:
TRUE)(Ff);
fairEX(N,
f)(Ff):
pred[state]
=
EX(N,
f
AND
fair?(N,
Ff));
fairEU(N,
f,
g)(Ff):
pred[state]
=
EU(N,
f,
g
AND
fair?(N,
Ff));
fairEF(N,
f)(Ff):
pred[state]
=
EF(N,
f
AND
fair?(N,
Ff));
fairAX(N,
f)(Ff):
pred[state]
=
NOT
fairEX(N,
NOT
f)(Ff);
fairAG(N,
f)(Ff):
pred[state]
=
NOT
fairEF(N,
NOT
f)(Ff);
fairAU(N,
f,
g)(Ff):
pred[state]
=
NOT
fairEU(N,
NOT
g,
NOT
f
AND
NOT
g)(Ff)
AND
fairAF(N,
g)(Ff);
CONVERSION-
K
conversion
END
fairctlops