Smaller abstractions for ∀CTL* without next

The success of applying model-checking to large systems depends crucially on the choice of good abstractions. In this work we present an approach for constructing abstractions when checking Next-free universal CTL* properties. It is known that functional abstractions are safe and that Next-free universal CTL* is insensitive to finite stuttering. We exploit these results by introducing a safe Next-free abstraction that is typically smaller than the usual functional one while at the same time more precise, i.e., it has less spurious counter-examples.