How to translate LTL formula to Kripke or Omega using tool

Question

I am solving some satisfiability questions from exam where one LTL formula should satisfy and other shouldn't or vice versa.

I know how I can check the satisfiability using LTL tool (TemporalLogicProver) by using phi -> (S1 & !S2) or vice versa.

Q Is there any possibility using tool so that I can find a Kripke structure corresponding to that LTL formula or LTL formula to Kripke structure (or Omega Automata) to check whether my understanding is correct ?

For e.g. if I want to get the LTL formula for the below Kripke structure:

Answer 1

Do you mean the following formula?

(a&!b) & G( ((a&!b)->X(!a&b)) & ((!a&b)->X(a&!b)) ) ?

For structures with a single cycle that is not that difficult, there is such a pattern. In general, however, there is the problem that LTL is not as powerful as automata are, so there is no algorithm that could translate any automaton to an LTL formula.

Comments

Thank you for the above formula.
Yes like above formula.
So got your point regarding no algorithm for translation of automaton to an LTL.

So I have to do this intuitively and verify it using the LTL tool. Is it right ?

---

In general, yes, you have to do that intuitively, but in most cases, a simple pattern as the one above will do.

---

Totally understood your point.
Thanks a lot :)