|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
 Digg  Furl  Spurl  Blink  Simpy  Google  Del.icio.us  Y!MyWeb | ||
| Search | ||
| ||
| ASCII Text | x | ||
| Rajeev Alur, Marcelo Arenas, Pablo Barcel?, Kousha Etessami, Neil Immerman, Leonid Libkin, "First-Order and Temporal Logics for Nested Words," Logic in Computer Science, Symposium on, pp. 151-160, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), 2007. | |||
| BibTex | x | ||
| @article{ 10.1109/LICS.2007.19, author = {Rajeev Alur and Marcelo Arenas and Pablo Barcel? and Kousha Etessami and Neil Immerman and Leonid Libkin}, title = {First-Order and Temporal Logics for Nested Words}, journal ={Logic in Computer Science, Symposium on}, volume = {0}, year = {2007}, issn = {1043-6871}, pages = {151-160}, doi = {http://doi.ieeecomputersociety.org/10.1109/LICS.2007.19}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - CONF JO - Logic in Computer Science, Symposium on TI - First-Order and Temporal Logics for Nested Words SN - 1043-6871 SP151 EP160 A1 - Rajeev Alur, A1 - Marcelo Arenas, A1 - Pablo Barcel?, A1 - Kousha Etessami, A1 - Neil Immerman, A1 - Leonid Libkin, PY - 2007 KW - null VL - 0 JA - Logic in Computer Science, Symposium on ER - | |||
We provide new temporal logics for finite and infinite nested words, which are natural extensions of LTL, and prove that these logics are first-order expressively-complete. One of them is based on adding a "within" modality, evaluating a formula on a subword, to a logic CaRet previously studied in the context of verifying properties of recursive state machines. The other logic is based on the notion of a summary path that combines the linear and nesting structures. For that logic, both model-checking and satisfiability are shown to be EXPTIME-complete.
Finally, we prove that first-order logic over nested words has the three-variable property, and we present a temporal logic for nested words which is complete for the twovariable fragment of first-order.