# What is the complexity of model checking Process Logic (LTL fragment)?

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.

-
I am confused. Could you give a definition of the fragment you're interested in? Would complexity results about LTL answer your question? –  Vijay D Jan 18 '13 at 19:36
@VijayD: No, complexity results for LTL won't help here much. PL is more akin to CTL* with programs serving as "selectors" of paths on which temporal formulae are evaluated. The note about the fragment is secondary, to move on with this problem, I am interested in complexity results on model-checking for logics which are mixing dynamic logic features with temporal modalities. –  walkmanyi Jan 18 '13 at 21:18