Go backward to Rigid Variables and Quantifiers Go up to Top Go forward to Simple Temporal Logic

The Enabled Predicate

• Enabled A
  • True for s iff it is possible to take an A step starting in s.
  • s[[Enabled A]] <=> exists t in St: s[[A]]t
• Syntactic definition
  • v_i all (flexible) variables in A.
  • Enabled A <=>
       exists c₁, ..., c_n: A(c₁/v'₁, ..., c_n/v'_n).
  • Enabled(y = (x')²+n) =
       exists c: y = c²+n
• If A represents actomic operation, Enabled A is true for those states in which it is possible to perform the operation.