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 
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
