On the decidability of linear Z-temporal logic and the monadic second order theory of the integers

The authors extend the monadic theory of the natural numbers and compare the weak monadic theory and the full monadic theory of the integers using automata on bi-infinite words. They also extend linear temporal logic (i.e. N-temporal logic) to Z-temporal logic and then compare Z-temporal logic with the first order monadic theory of the integers. This extension is obtained by using the classical modalities (i.e. X, F, G, U, S), by adding the existential and the universal past operators (i.e. X¯, F¯), and by interpreting formulas over Z-words instead of ω-words