
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy 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 12November 14
ISBN: 0769508502
ASCII Text  x  
M. Maidi, "The common fragment of CTL and LTL," 2013 IEEE 54th Annual Symposium on Foundations of Computer Science, pp. 643, 41st Annual Symposium on Foundations of Computer Science, 2000.  
BibTex  x  
@article{ 10.1109/SFCS.2000.892332, author = {M. Maidi}, title = {The common fragment of CTL and LTL}, journal ={2013 IEEE 54th Annual Symposium on Foundations of Computer Science}, volume = {0}, year = {2000}, issn = {02725428}, pages = {643}, doi = {http://doi.ieeecomputersociety.org/10.1109/SFCS.2000.892332}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  CONF JO  2013 IEEE 54th Annual Symposium on Foundations of Computer Science TI  The common fragment of CTL and LTL SN  02725428 SP EP A1  M. Maidi, PY  2000 KW  temporal logic; trees (mathematics); decidability; computational complexity; finite automata; CTL; actionbased computation tree logic; LTL; linear time logic; common fragment; expressive power; inductive definition; ACTL formulas; PSPACEcomplete problem; path quantifiers; negation; 1weak Buchi automaton; automaton size; formula size VL  0 JA  2013 IEEE 54th Annual Symposium on Foundations of Computer Science ER   
It is wellknown 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 (Actionbased 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 PSPACEcomplete. 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 1weak 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; actionbased computation tree logic; LTL; linear time logic; common fragment; expressive power; inductive definition; ACTL formulas; PSPACEcomplete problem; path quantifiers; negation; 1weak 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.