We int
roduce an LTL-like logic with atomic fo
rmulae built ove
r a const
raint language inte
rp
reting va
riables in
![]()
rc="http://sp
ringe
rlink.lib.tsinghua.edu.cn/media/images/cont
ributions/5/1/8/G/518GUF8UT3PNBLWV_html/MediaObjects/InlineFigu
re2.png" alt="MediaObjects/InlineFigu
re2.png" align="middle">. The const
raint language includes pe
riodicity const
raints, compa
rison const
raints of the fo
rm
x =
y and
x <
y, it is closed unde
r Boolean ope
rations and it admits a
rest
ricted fo
rm of existential quantification.
This is the la
rgest set of qualitative const
raints ove
r ![]()
rc="http://sp
ringe
rlink.lib.tsinghua.edu.cn/media/images/cont
ributions/5/1/8/G/518GUF8UT3PNBLWV_html/MediaObjects/InlineFigu
re3.png" alt="MediaObjects/InlineFigu
re3.png" align="middle"> known so fa
r, shown to admit a decidable LTL extension. Such const
raints a
re those used fo
r instance in calenda
r fo
rmalisms o
r in abst
ractions of counte
r automata by using cong
ruences modulo some powe
r of two. Indeed, va
rious p
rog
ramming languages pe
rfo
rm a
rithmetic ope
rato
rs modulo some intege
r. We show that the satisfiability and model-checking p
roblems (with
respect to an app
rop
riate class of const
raint automata) fo
r this logic a
re decidable in polynomial space imp
roving significantly known
results about its st
rict f
ragments. As a by-p
roduct, LTL model-checking ove
r integ
ral
relational automata is p
roved complete fo
r polynomial space which cont
rasts with the known undecidability of its CTL counte
rpa
rt.