On Decidability of LTL+Past Model Checking for Process Rewrite Systems

The paper [Bozzelli, L., M. Křetínský, V. Řehák and J. Strejček, On decidability of LTL model checking for process rewrite systems, in: FSTTCS 2006, LNCS 4337 (2006), pp. 248–259] shows that the model checking problem for (weakly extended) Process Rewrite Systems and properties given by LTL formulae with temporal operators strict eventually and strict always is decidable. The same paper contains an open question whether the problem remains decidable even if we extend the set of properties by allowing also past counterparts of the mentioned operators. The current paper gives a positive answer to this question.