Verification of qualitative Z constraints

10 years 4 months ago
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, comparison constraints of the form x = y and x < y, is closed under Boolean operations and admits a restricted form of existential quantification. Such constraints are used for in calendar formalisms or abstractions of counter automata by using congruences modulo some power of two. Indeed, various programming languages perform arithmetic operators modulo some integer. We show that the satisfiability and model-checking problems (with respect to an appropriate class of constraint automata) for this logic are decidable in polynomial space improving significantly known results about its strict fragments. This is the largest set of qualitative constraints over Z known so far, shown to admit a decidable LTL extension.
Stéphane Demri, Régis Gascon
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2008
Where TCS
Authors Stéphane Demri, Régis Gascon
Comments (0)