[Solved]: Some slight confusion with the UNTIL operator in CTL (e.g. a U b)

Problem Detail: 

I've sketched a very small transition system in paint that I'll use as an example.

I want to see if $A(aUb)$ holds for this transition system. From my understanding, this CTL formula is asking if ALL paths satisfy $aUb$. The only path we can take in this example is S0S1S0S1S0S1S0S1...

This path produces the output (1) $aaaaaaaaaaaaaaaaa...$ or (2) $aaaaaaaaaaaaaaab...$

(2) definitely holds - however it's (1) that I'm unsure about. Am I correct in saying that $aUb$ doesn't hold for (1)? Since we can continue looping over a infinitely without eventually reaching b (and because (1) doesn't satisfy the formula, $A(aUb)$ doesn't hold for this transition system).

Have I understood this correctly? I guess the main confusion for me is that there is 1 path but more than 1 possible output.

Any help is much appreciated.

edit: This is the transition system I'm referring to in the comments below

Asked By : eyes enberg

Answered By : Shaull

You have some misconception regarding transition systems: The alphabet of the system is $2^P$ for some set $P$, and paths induce words over $2^P$. In the first system, there is a single path: $(S_0,S_1)^\omega$, and it induces a single word: $(\{a\},\{a,b\})^\omega$.

Now, this word satisfies $aUb$, since $a$ holds until the secod letter, in which $b$ holds.

The $\forall$ quantifier here is somewhat useless, since there is a single path.

The second system is problematic, since there is nowhere to go to from $S_2$...

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/36014

 Ask a Question

 Download Related Notes/Documents