2
$\begingroup$

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!

$\endgroup$
  • 2
    $\begingroup$ Even though you ask how to begin trying, it would be helpful if you detailed some attempts (even failed ones). $\endgroup$ – Shaull Jan 17 '14 at 8:47
5
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.