# Questions tagged [computation-tree-logic]

The tag has no usage guidance.

39 questions
Filter by
Sorted by
Tagged with
127 views

### Can CTL* express every model's behaviour

CTL* as in https://en.wikipedia.org/wiki/CTL*, is a logic that combines CTL and LTL. I know that CTL* can express everything expressible in these two languages and more. My question is whether we can ...
• 90
1 vote
39 views

### How do I prove relations of two CTL formulas?

If I have two CTL equations, how do I prove they're equivalent or that one implies the other? What's the general approach? Disproving is obvious, but I am unable to figure out how to prove the ...
• 324
28 views

### Is there a CTL* formula that translates into mu-calculus formula 𝜇Y.νZ.(...) with alternation depths 2,1 for Y,Z?

A CTL* formula EFG p is equivalent to mu-calculus formula 𝜇Y.(<>Y | νZ.(<>Z & p)). In this formula, the ...
• 1,085
423 views

### Difference between CTL and CTL*

I am wondering what exactly the difference between CTL and CTL* is. I know that CTL* is strictly more expressive than CTL, but it is not clear to me how the "restrictions" to CTL accomplish ...
57 views

### CTL trouble translating text into formula

I have an excercise where I have to translate verbally formulated statements into CTL formulas. I have particularly trouble with this one: On every path q is true at least once and p was true ...
• 135
34 views

• 268
699 views

### LTL globally implies

I have got confused in undressing the informal definition of LTL below: $$G(\phi \Longrightarrow\psi)\Longrightarrow(G\phi \Longrightarrow G\psi)$$ in many literatures I have seen implies is said as ...
• 268
1 vote
114 views

### CTL satisfied by Kripke Structure

given a Kripke Structure I want to check if a CTL formula is satisfied or not. the CTL is: $$AG(c \vee AX\neg E((a\vee b)Uc))$$ I have read that it is better to write to CTL in terms of $\wedge$ ...
• 268
1 vote
78 views

### Understanding a Single Step in the Model Checking Algorithm

This answer explains roughly how to convert a nested boolean function into a Binary Decision Diagram (BDD). This question is about how to structure the states for the BDD. Now in this question I am ...
• 2,275