Questions tagged [computation-tree-logic]
The computation-tree-logic tag has no usage guidance.
39
questions
2
votes
1
answer
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
0
answers
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
0
votes
1
answer
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
2
votes
1
answer
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 ...
- 23
3
votes
1
answer
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
0
votes
1
answer
34
views
$Sat(EG^2\alpha)$ as a fixpoint of an operator
Currently I am studying CTL model checking. I found this exercise:
Consider the CTL formula $EG^2(\alpha)$ which means that there exists a path that satisfies $\alpha$ at every even position. Define $...
user128868
0
votes
1
answer
190
views
CTL formula for "for every computation it is always possible to return to the initial state"
In the book 'Principles of Model Checking' by Christel Baier and Joost-Pieter Katoen they state that the CTL formula for " for every computation it is always possible to return to the initial state" ...
- 165
0
votes
2
answers
94
views
Semantics of E and A operators in CTL*
I'm referring to a book where E and A were defined in text as follows
The formula $A \phi$ states that all the executions out of the current state satisfy property $\phi$ whereas $E\phi$ states ...
- 131
1
vote
1
answer
224
views
Validity of CTL formula $s_0 \models EG\ AF\ p$ in given model
I have been learning Verification by model checking recently and I get the following question:
Is the CTL formula $s_{0} \models EG\ AF\ p$ valid in the following model?
I think it is ...
- 135
2
votes
1
answer
349
views
How do you correctly write this sentence as a CTL formula?
Sentence: From every reachable state it is possible to reach a state where $p$ is true.
How do you write this sentence as a CTL formula? So far I only dealt with CTL syntax and trees but maybe it ...
- 133
1
vote
1
answer
126
views
Reduce the running by using doubly logarithmic tree
I have two algorithms $A$ and $B$ to solve a problem $P$ of size $n$. Algorithm $A$ takes $O(\log n)$ time on the PRAM using $O(n \log n)$ operations (done in parallel). Algorithm $B$ reduces the size ...
- 23
2
votes
2
answers
125
views
How to express the existence of winning strategy of the starter of a game in temporal logic?
Consider a two-player game. A winning strategy of a player is a strategy following which the player can always beat his opponent, no matter how his opponent responds.
A game can be unfolded to a ...
- 9,611
1
vote
1
answer
2k
views
Proving the equivalence of an LTL and a CTL formula
For a lecture I am attending, we have to prove that
$$\forall \big(a \textsf{U} (b \land \forall \square a)\big) \equiv \big(a \textsf{U} (b \land \square a)\big).$$
That is, we need to prove that ...
- 13
3
votes
1
answer
386
views
Least fix point of CTL formula
In the book Logic in Computer Science on page 244, there is a proof that $[[E(\phi U\psi)]]$ is the least fixed point of $G(X)=[[\psi]] \cup ([[\phi]]\cap\mathop{\textrm{pre}}_\exists(X))$. I don't ...
- 198
0
votes
1
answer
240
views
Linear Temporal Logic, Idempotent law
in many lecture notes, I have seen the LTL idempotent law for until and its equivalence is described as $\phi U(\phi U \psi) \equiv \phi U\psi$ and also $(\phi U \...
- 268
0
votes
1
answer
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
0
answers
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
0
answers
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
2
votes
1
answer
72
views
Why is $AF \phi \lor \varphi$ not equivalent to $AF \phi \lor AF \varphi$?
Can someone explain to me (perhaps with an example) why $AF (\phi \lor \varphi)$ is not equivalent to $AF \phi \lor AF \varphi$. This seems counter-intuitive, because in any path where $\phi$ (or $\...
2
votes
1
answer
2k
views
Intuition behind straight-line programs
Wikipedia defines straight-line programs in the following manner:
In mathematics, more specifically in computational algebra[disambiguation needed], a straight-line program (SLP) for a finite group ...
- 919
3
votes
1
answer
153
views
CTL* query evaluation order
I'm currently trying to evaluate a CTL* expression and am not sure how to stepwisely evaluate the queries.
For example I have EFG p. This means something like 'there is a path where eventually there ...
- 33
3
votes
1
answer
897
views
What does "AF AX p" mean in CTL?
Both Logic in Computer Science (Huth and Ryan, 2004) and Branching vs. Linear Time: Final Showdown (Vardi, 2002), state something to this effect (paraphrased):
In LTL, X F p and F X p are ...
- 131
1
vote
1
answer
349
views
How to verify a property about a certain order of events in TCTL / UPPAAL?
I'd like to check if a certain order of events happens if another property holds true using UPPAAL and TCTL.
...
- 145
1
vote
1
answer
126
views
An algorithm to compute a set of states that satisfy a specific CTL formula
Working through a past exam question and I'm unsure where to start or what form they want the answer in:
Define an algorithm that receives as input a finite transition
system TS defined over the set ...
- 303
1
vote
1
answer
419
views
CTL - model checking for formula $A [a \cup b]$
I'm trying to verify if the following model satisfy $A [a \cup b]$:
The algorithm I'm using is taken from "Concepts, Algorithms, and Tools for Model Checking", Joost-Pieter Katoen. In particular I ...
- 155
2
votes
1
answer
1k
views
CTL vs LTL - when a formula satisfy a model
I'm trying to understand the difference between LTL and CTL. In particular, i'm trying to understand when a model (a transition system eg. Kripke structure) satisfy a formula.
This is my point of view:...
- 155
0
votes
1
answer
170
views
Defining a new operator in CTL
Lets consider a new operator $B$ where $a B b$ means "in every execution, if $b$ holds some time, then $a$ does so before it" and we're asked to define it in CTL.
My working: the system can only ...
- 303
0
votes
1
answer
91
views
Defining a new (informal) operator in CTL
If you were given a "new operator" Wh and a formula a Wh b meaning that a holds for at least as long as b does (in all executions). How would you define this operator in CTL? This is an exercise ...
- 303
1
vote
2
answers
820
views
Some slight confusion with the UNTIL operator in CTL (e.g. a U b)
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 ...
- 303
0
votes
1
answer
1k
views
Difference between equivalence and implication
In terms of CTL formulae, what is the difference between equivalence and implication?
(prop = some proposition, && = conjunction, AG = CTL syntax for "globally holds")
E.g. AG (prop1 &&...
- 137
1
vote
1
answer
433
views
Determining set of states that satisfy a CTL formulae
I'm trying to understand CTL formulae, and until now I've understood everything (or at least I thought I did). I have the following Kripke strucure:
Now given the following CTL formulae ...
- 137
1
vote
1
answer
599
views
Computation tree logic and Kripke structures
Specifications in Kripke structures are verified by Computation tree logic (CTL). However, refering to this Wikipedia article the CTL-operators are relative to a current state. So, when we want to ...
- 217
2
votes
1
answer
628
views
Transition systems that satisfy LTL but not CTL, and vice versa
I am learning about temporal logic and model checking systems. One conceptual exercise that I am struggling with is how to create a transition system which satisfies only one of two given properties, ...
- 131
2
votes
0
answers
104
views
Is there any open-source tools for verifying TCTL formulae over timed automata can be imported into my project?
In my project, there is one important step to automatically verify a timed automata with TCTL formulae. I briefly surveyed the tool UPPAAL that provides a GUI to construct a timed automata and to ...
- 21
1
vote
1
answer
809
views
Techniques (tools) to convert temporal logic (CTL,CTL* or LTL) to μ-calculus formulae
Suppose one wants to use a μ-calculus model checker, but specify things in temporal logics, which is easier (more intuitive). Is there a technique (even better, a tool) that automatically translates ...
- 129
11
votes
3
answers
3k
views
Why use $\mu$-calculus and not LTL,CTL,CTL*?
It is known that the temporal logics LTL,CTL,CTL* can be translated/embedded into the $\mu$-calculus. In other words, the (modal) $\mu$-calculus subsumes these logics,
(i.e. it is more expressive.)
...
- 129
1
vote
1
answer
317
views
applying CTL/LTL model-checking on some system
I apologies if my title is vague, I'm trying to apply CTL/LTL model-checking on some system written in java, however, I still don't understand how to reach a result using either of the approaches ...
- 111
2
votes
1
answer
434
views
Convert CTL* formula to CTL
I have a CTL* formula: $\mathsf{EF}[p\land \mathsf{AX}[q\ \mathsf{U}\ r]]$ but in my application, I am limited to CTL. To my understanding, this formula is no valid CTL and I wonder whether I can ...
user13397
8
votes
4
answers
1k
views
How can I decide manually whether two CTL formulae are equivalent?
Assume I have two formulae $\Phi$ and $\Psi$ (over the same set of atomic propositions $AP$) in CTL. We have that $\Phi \equiv \Psi$ iff $Sat_{TS}(\Phi) = Sat_{TS}(\Psi)$ for all transition systems $...
- 1,765