Re: LTL vs. CTL

On 28 Jan., 20:15, sasha mal <sashaDOT...@xxxxxxxxxxxxx> wrote:
Let f be a CTL formula ang g an LTL formula (both without past
modalities). Assume that there is an infinite transition system T (in
which each state has a successor) that separates f and g, i.e. T is a
model of f, but not of g, or T is a model of g, but not of f. Is there a
finite transition system (in which each state has a successor) that
separates g and f?
Are you talking about propositional LTL/CTL? Or first order LTL? Is a
finite transition system finite wrt. the number of distinct states?
For first order LTL, f := \forall x \in IN. [](s = x => <> s = x+1)
and g := false should do the trick. (I am a bit rusted in in FOLTL, so
f should be "whenever s has the value x, it will at some point in the
future have the value x+1" - by some induction argument this can only
work with infinite many states.) For propositional LTL, what would a
infinite transition system look like?
.

Relevant Pages

  • LTL vs. CTL
    ... Let f be a CTL formula ang g an LTL formula (both without past ... Assume that there is an infinite transition system T (in ... which each state has a successor) that separates f and g, ... separates g and f? ...
    (comp.theory)
  • LTL vs. CTL
    ... Let f be a CTL formula ang g an LTL formula (both without past ... Assume that there is an infinite transition system T (in ... which each state has a successor) that separates f and g, ... separates g and f? ...
    (sci.math)
  • LTL vs. CTL
    ... Let f be a CTL formula ang g an LTL formula (both only with future ... Assume that there is an infinite transition system T (in ... which each state has a successor) that separates f and g, ... separates g and f? ...
    (sci.logic)