What is the complexity of model checking Process Logic (LTL fragment)?
More along the "related formalisms" direction.


PDL with intersection and converse: satisfiability and infinite-state model checking, Stefan Göller, Markus Lohrey, and Carsten Lutz, 2009
The Effects of Bounding Syntactic Resources on Presburger LTL, Stéphane Demri and Régis Gascon


The introduction section of the first paper has an extensive discussion of complexity results for PDL fragments and extensions. I include the second mainly because you may be be able to encode some parts of your problem as a Presburger extension and transfer some results.