Incompleteness of States w.r.t. Traces in Model Checking

Roberto Giacobazzi, Francesco Ranzato

Cousot and Cousot introduced and studied a general past/future-time specification language, called mu*-calculus, featuring a natural time-symmetric trace-based semantics. The stand…