This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
41st Annual Symposium on Foundations of Computer Science
The common fragment of CTL and LTL
Redondo Beach, California
November 12-November 14
ISBN: 0-7695-0850-2
M. Maidi, Siemens Corp. Technol., Munchen, Germany
It is well-known that CTL (computation tree logic) and LTL (linear time logic) have incomparable expressive power. In this paper, we give an inductive definition of those ACTL (Action-based CTL) formulas that can be expressed in LTL. In addition, we obtain a procedure to decide whether an ACTL formula lies in LTL, and show that this problem is PSPACE-complete. By omitting path quantifiers, we get an inductive definition of the LTL formulas that are expressible in ACTL. We can show that the fragment defined by our logic represents exactly those LTL formulas the negation of which can be represented by a 1-weak Bu/spl uml/chi automaton and that, for this fragment, the representing automaton can be chosen to be of size linear in the size of the formula.
Index Terms:
temporal logic; trees (mathematics); decidability; computational complexity; finite automata; CTL; action-based computation tree logic; LTL; linear time logic; common fragment; expressive power; inductive definition; ACTL formulas; PSPACE-complete problem; path quantifiers; negation; 1-weak Buchi automaton; automaton size; formula size
Citation:
M. Maidi, "The common fragment of CTL and LTL," focs, pp.643, 41st Annual Symposium on Foundations of Computer Science, 2000
Usage of this product signifies your acceptance of the Terms of Use.