Verification of qualitative Z constraints

We introduce an LTL-like logic with atomic formulae built over a constraint language interpreting variables in Z. The constraint language includes periodicity constraints and comparison constraints of the form x=y and x