<p>More along the "related formalisms" direction.</p>

<ol>
<li><a href="http://www.informatik.uni-leipzig.de/~lohrey/08-JSL.pdf" rel="nofollow">PDL with intersection and converse: satisfiability and infinite-state model checking</a>, Stefan Göller, Markus Lohrey, and Carsten Lutz, 2009</li>
<li><a href="http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-jlc09.pdf" rel="nofollow">The Effects of Bounding Syntactic Resources on Presburger LTL</a>, Stéphane Demri and Régis Gascon</li>
</ol>

<p>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.</p>

CC BY-SA 3.0
2013-01-19T04:31:08.530Z
2013-01-19T04:31:08.530Z
Vijay D
<p><a href="http://www.wisdom.weizmann.ac.il/~harel/SCANNED.PAPERS/ProcessLogic.pdf">Process Logic</a> 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 "<em>along traces resulting from execution of $P$, $\phi$ holds</em>", or plainly "<em>during execution of $P$, $\phi$ holds</em>". Temporal modalities correspond to an extension of LTL with a <em>chop</em> and <em>slice</em> operators.</p>

<p>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]$.</p>

<p><strong>Question:</strong> <em>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.</em></p>

CC BY-SA 3.0
2013-01-18T19:36:28.033Z
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
CC BY-SA 3.0
2013-01-18T21:18:40.413Z
@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
<time-complexity><model-checking><linear-temporal-logic><temporal-logic>
What is the complexity of model checking Process Logic (LTL fragment)?
walkmanyi
# What is the complexity of model checking Process Logic (LTL fragment)?

(Asked by: username_0 on 2013-01-18)

[Process Logic](http://www.wisdom.weizmann.ac.il/~harel/SCANNED.PAPERS/ProcessLogic.pdf) 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.*

**Tags:** time-complexity, model-checking, linear-temporal-logic, temporal-logic

> **Comments:**
> **username_1**: I am confused. Could you give a definition of the fragment you're interested in? Would complexity results about LTL answer your question?  
> **username_0**: @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.  

---

## 1 answers

### Answer by username_1 on 2013-01-19. Score: 2 | Accepted answer

More along the "related formalisms" direction.

1. [PDL with intersection and converse: satisfiability and infinite-state model checking](http://www.informatik.uni-leipzig.de/~lohrey/08-JSL.pdf), Stefan Göller, Markus Lohrey, and Carsten Lutz, 2009
2. [The Effects of Bounding Syntactic Resources on Presburger LTL](http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-jlc09.pdf), 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.


---

