<p>So I'm trying to solve some CTL formulas on a given system using model-checking.</p>
<p>I'm trying several different solvers; some of them only accept LTL as input, but have some nice partial-order reductions built-in that I would like to use and should perform well on my systems that feature heavy interleaving.</p>
<p>We know the intersection of LTL and CTL is non-empty (e.g. invariants lie there) but do you know of an algorithm to determine if a CTL formula can also be expressed in LTL, and to translate it if so ?</p>

CC BY-SA 4.0
2020-12-11T15:36:38.523Z
This question actually has a close duplicate here : https://cstheory.stackexchange.com/questions/36626/syntactic-characterisation-of-the-intersection-of-ctl-and-ltl?rq=1 that I didn't find before
Yann TM
CC BY-SA 4.0
2020-12-11T18:14:30.543Z
Doesn't it fully answer your question?
Shaull
CC BY-SA 4.0
2020-12-11T23:35:10.647Z
It does, although there does not seem to be an implementation and the algorithm is more costly than I hoped. But I'm not sure how to close my question. I don't have rep enough on this stack to "mark as duplicate" and kill the question outright.
Yann TM
<temporal-logic><linear-temporal-logic>
Algorithm to decide if a CTL formula can also be expressed in LTL and translate it?
Yann TM
# Algorithm to decide if a CTL formula can also be expressed in LTL and translate it?

(Asked by: username_0 on 2020-12-11)

So I'm trying to solve some CTL formulas on a given system using model-checking.

I'm trying several different solvers; some of them only accept LTL as input, but have some nice partial-order reductions built-in that I would like to use and should perform well on my systems that feature heavy interleaving.

We know the intersection of LTL and CTL is non-empty (e.g. invariants lie there) but do you know of an algorithm to determine if a CTL formula can also be expressed in LTL, and to translate it if so ?

**Tags:** temporal-logic, linear-temporal-logic
> **Comments:**
> **username_0**: This question actually has a close duplicate here : https://cstheory.stackexchange.com/questions/36626/syntactic-characterisation-of-the-intersection-of-ctl-and-ltl?rq=1 that I didn't find before  
> **username_1**: Doesn't it fully answer your question?  
> **username_0**: It does, although there does not seem to be an implementation and the algorithm is more costly than I hoped. But I'm not sure how to close my question. I don't have rep enough on this stack to "mark as duplicate" and kill the question outright.  

---

## 0 answers

