LTL vs. CTL

From: sasha mal <sashaDOTmal@xxxxxxxxxxxxx>
Date: Mon, 28 Jan 2008 20:13:59 +0100

Dear all,

Let f be a CTL formula ang g an LTL formula (both only with future
operators). 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?

Any ideas are welcome.
Thanks and best regards
Sasha.
.

Follow-Ups:
- Re: LTL vs. CTL
  - From: Achim Blumensath

Prev by Date: Re: Some answers to Aatu Koskensilta
Next by Date: Re: What's the weakest metatheory in which Goedel's theorem can be proved?
Previous by thread: What's the weakest metatheory in which Goedel's theorem can be proved?
Next by thread: Re: LTL vs. CTL
Index(es):
- Date
- Thread

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? ...
(sci.math)
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)
Re: LTL vs. CTL
... 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)