[Solved]: Transition systems that satisfy LTL but not CTL, and vice versa

Problem Detail: 

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, when one is in LTL and one is in CTL. For example:

• Find a transition system that satisfies only one of the following two properties: $FGp$, $AFEGp$
• Find a transition system that satisfies only one of the following two properties: $FGp$, $EFEGp$
• Find a transition system that satisfies only one of the following two properties: $GFp$, $AGEFp$

How should I begin when trying to reason about these types of problems? In general, is it easier to design transition systems for LTL properties or CTL properties? Or does it depend on the situation?

Any insight would be appreciated!

Asked By : KJ50

Answered By : Shaull

Technically, LTL and CTL are incomparable in their differentiating power over Kripke structures. So intuitively, it shouldn't be easier to design one or the other.

However, most people tend to find it easier to think in linear time. Making sure a certain property holds for all paths is easier than studying a branching-time property. In particular, this is because a counter-example for the satisfaction of an LTL formula is a path, whereas a counterexample for a CTL formula may be a tree.

To demonstrate how to approach the questions at hand, let's consider the first one. First, consider what the formulas mean:

$FGp$ means "in every path, after a finite prefix, $p$ always holds".

$AFEGp$ means "in every path, after a finite prefix, a state is reached from which there exists a path in which $p$ is always true."

Now, if $FGp$ holds, then $AFEGp$ must also hold, because in every path, eventually a state is reached from which $Gp$ holds. Thus, our search should restrict to finding a system which satisfies $AFEGp$, but not $FGp$.

To achieve this, we need to at least have a state that satisfies $Gp$, so let's start with that. Take the state $A$ to have the transition $A\to A$, and $A$ is labeled with $p$. Let's also have $A$ as the initial state (this is arbitrary). So far, this system also satisfies $FGp$, so now we fix that by adding a "bad path": we add a state $B$, labeled by $\neg p$ with the transitions $A\to B$ and $B\to A$.

The path $A,B,A,B,...$ does not satisfy $FGp$, so this is good. However, every path eventually reaches $A$, in which $EGp$ is true, so $AFEGp$ holds, and we are done.

Best Answer from StackOverflow

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

3.2K people like this

 Download Related Notes/Documents