Chennai Mathematical Institute


An automata-theoretic approach to Constraint LTL
Dr. Deepak D'Souza
Chennai Mathematical Institute.


We consider an extension of linear-time temporal logic (LTL) with constraints interpreted over a concrete domain like the natural numbers. We use a new automata-theoretic technique to show PSPACE decidability of the logic for the constraint systems (Z,<,=) and (N,<,=), where Z and N are the integers and natural numbers respectively. We also give an automata-theoretic proof of a recent decidability result of Balbiani and Condotta for the logic over constraints which satisfy a "completion" property.

This is joint work with Stephane Demri (LSV, ENS-Cachan).