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

1.6k comments

524 users

0 votes
August 2021 - 8a - A small clarification

[a U GF(b)]

= (a SU b) V Gb

= (a SU b) V (true SU a)

I tried to write this as solution. Is it also valid solution?If not please explain.

From lecture i understand LTL has  only pure path formulas state formulas:  P ::= VΣ  I was trying to satisfy.
in # Study-Organisation (Master) by (850 points)

1 Answer

0 votes

Your solution is not correct. You are right that LTL formulas must not have path quantifiers, so your formulas are LTL formulas. However, the formulas are not equivalent to each other:

Just consider a transition system with a single state with a self-loop where a holds but where b is false. Then, [a WU G F b] holds on the single path of that structure while both [a SU b] and G b are false.

Also for the second equivalence, [true SU a] is equivalent to F a, but not to G b. You can check the equivalence of LTL formulas with https://es.cs.uni-kl.de/tools/teaching/TemporalLogicProver.html

by (165k points)

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
asked Aug 25, 2022 in * TF "Emb. Sys. and Rob." by CS_E (2.9k points)
Imprint | Privacy Policy
...