Process Logic is a modal logic allowing to reason about temporal properties of programs. Its formulae take the form similar to (Propositional) Dynamic Logic $[P]\phi$, with $P$ being a program (think regular expression) and $\phi$ being another process logic formula, however unlike PDL, it can contain temporal LTL-style modalities. Unlike LTL, the formulae are read as follows "along traces resulting from execution of $P$, $\phi$ holds", or plainly "during execution of $P$, $\phi$ holds". Temporal modalities correspond to an extension of LTL with a chop and slice operators.
I am interested in a fragment of Process Logic where $\phi$ wouldn't be a full PL formula, but rather a plain LTL formula without modalities of the form $[P]$.
Question: Are there complexity analysis results relevant to model-checking formulae of Process Logic, or related formalisms? I am interested in both, the the complexity analysis, as well as some ideas for algorithms for doing it.