Re: LTL vs. CTL

Achim Blumensath wrote:
sasha mal wrote:
Achim Blumensath wrote:
sasha mal wrote:
Let f be a CTL formula ang g an LTL formula [...]. Assume that there
is an infinite transition system T [...] that separates f and g [...].
Is there a finite transition system [...] that separates g and f?
Yes. You can translate f and g into MSO-formulae. If (f and not g) has a
model then it also has a tree model. Hence, the corresponding
MSO-formula has a tree model and, therefore, also a model that is a
regular tree. Take the finite transition system whose unravelling is
this model. Since f and g are bisimulation invariant you get a finite
model of (f and not g).
1. In what logic do you write the formulas "f and not g", "g and not f"?

In MSO. You could also use the mu-calculus instead.

Could you please give a reference on translating formulas of this
logic into MSO?

I know no good reference. The following survey looks good, but I haven't
read it yet:

http://www.cs.rice.edu/~vardi/papers/wal07.pdf

2. For "g and not f", the situation is more complicated. Let T be a
model of g, but not a model of f. It is not necessarily the case that T
is a model of "not f". It may happen that T is neither a model of f nor
a model of "not f" (remember that f is a CTL formula and T may have more
than one initial state). So it may happen that T is not a model of "g
and not f".

You seem to have a strange notion of a "model". Usually, one considers
transition systems with a designated initial state. Anyway, once you
have translated everything in MSO you can just add a universal
quantifier over the initial state. Then negation is straightforward.


There is nothing strange about a transition system having more than one
initial state, since programs have many; although some people prefer
having exactly one initial state for cases like this one.

Actually, I'm not familiar with MSO, so I cannot confirm your proof
without doing a bit of reading first. Nevertheless, thank you very much!

Best regards
Sasha.
.

Quantcast