Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers


546 users

0 votes

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:

in * TF "Emb. Sys. and Rob." by (2.9k points)

1 Answer

+1 vote
Best answer
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.
by (166k points)
selected by
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 :)
Imprint | Privacy Policy