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

543 users

+1 vote
I have this que from Feb 2018 Prob 8.2

[Fa U b] and [Gb SU a]

Fa U b => fa........b / Gfa

So should not bother whether b occurs or not but focus on Fa.

What if in t=0 a holds and t=1 it a doesn't hold, Is this equal to Fa. Finally a should hold atleast once and this final point of time is in t=0 itself.  Does it still satisfy Fa.

Can some one please explain this problem

Thanks
in * TF "Emb. Sys. and Rob." by (870 points)

1 Answer

+3 votes

If a holds at t=0, but not afterwards, then Fa holds at t=0, but also no more at t>0, so it is no longer true then. F-properties are always of that kind. If they hold at t=0, then they also may hold for some time, and then switch to false for the rest of time (or keep true forever). The point of time where Fφ will switch to false is the last point of time where φ holds (if there is such a point  of time). If φ holds infinitely often, then Fφ is always true. If φ holds never, then Fφ is always false.

A general remark to answer these kinds of questions: You can draw a Kripke structure with a single infinite path so that the distinction on E and A quantifiers does not matter. Then you can check even the LTL properties by adding E/A quantifiers in front of every temporal operator so that you can use our CTL model checker to answer the questions you have. 

For your example, I would have drawn the following structure:

Input for the CTL model checker would be as follows:

vars a,b;
init 0;
labels 0:a; 1:a; 2:; 3:; 
transitions 0->1; 1->2; 2->3; 3->3;

 and here you may let the model checker compute the following for you:

  • 〖E F a〗= {s0;s1} =〖a〗
  • 〖E[(E F a) WU b]〗= E[a WU b]〗= {}
  • 〖E G b〗= {}
  • 〖E[false SU a] =〖a〗= {s0;s1}

Please note that in general, the formulas checked here are not the same, but on structures with only a single infinite path, there is no distinction between CTL/CTL*/LTL and neither between E and A. For past operators, that is however not the case. Still, in many cases single paths are sufficient to distinguish between formulas, and then the above approach gives you quickly reliable answers. 

by (166k points)
edited by
Imprint | Privacy Policy
...