Proceedings 41st Annual Symposium on Foundations of Computer Science (2000)
Redondo Beach, California
Nov. 12, 2000 to Nov. 14, 2000
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.
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
M. Maidi, "The common fragment of CTL and LTL," Proceedings 41st Annual Symposium on Foundations of Computer Science(FOCS), Redondo Beach, California, 2000, pp. 643.