An automata-theoretic approach to Constraint LTL
Stephane Demri and Deepak D'Souza
IISc-CSA-TR-2003-1
(August 2003) Available formats: [ps] [ps.gz]
Filed on May 3, 2004
Updated on May 13, 2004
We consider an extension of linear-time temporal logic (LTL)
with constraints interpreted over a concrete domain.
We use a new automata-theoretic technique to show
PSPACE decidability of the logic for the constraint systems
(Z,<,=) and (N,<,=).
Along the way, we give an automata-theoretic proof of
a result of [BC02] when the constraint system
satisfies the completion property.
Our decision procedures extend easily to handle extensions of the
logic with past operators and constants, as well as an extension
of the temporal language itself to monadic second
order logic.
Finally we show that the logic becomes undecidable
when one considers constraint systems that allow a counting mechanism.
Please bookmark this technical report as http://aditya.csa.iisc.ernet.in/TR/2003/1/.Problems ? Contact techrep@csa.iisc.ernet.in
[Updated at 2009-10-22T06:42Z]