First-Order and Temporal Logics for Nested Words

Simple item page
dc.contributor.authorAlur, R.
dc.contributor.authorArenas Saavedra, Marcelo Alejandro
dc.contributor.authorBarcelo, P.
dc.contributor.authorEtessami, K.
dc.contributor.authorImmerman, N.
dc.contributor.authorLibkin, L.
dc.date.accessioned2022-05-16T20:30:52Z
dc.date.available2022-05-16T20:30:52Z
dc.date.issued2007
dc.description.abstractNested words are a structured model of execution paths in procedural programs, reflecting their call and return nesting structure. Finite nested words also capture the structure of parse trees and other tree-structured data, such as XML. 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 two- variable fragment of first-order.
dc.fuente.origenIEEE
dc.identifier.doi10.1109/LICS.2007.19
dc.identifier.issn1043-6871
dc.identifier.urihttps://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=4276560
dc.identifier.urihttps://doi.org/10.1109/LICS.2007.19
dc.identifier.urihttps://repositorio.uc.cl/handle/11534/64016
dc.information.autorucEscuela de ingeniería ; Arenas Saavedra, Marcelo Alejandro ; S/I ; 81488
dc.language.isoes
dc.nota.accesoContenido parcial
dc.publisherIEEE
dc.relation.ispartofIEEE Symposium on Logic in Computer Science (LICS 2007) (22° : 2007 : Wroclaw, Polonia)
dc.rightsacceso restringido
dc.subjectBoolean functions
dc.subjectXML
dc.subjectNavigation
dc.subjectAutomata
dc.subjectInspection
dc.subjectComputer science
dc.subjectLogic design
dc.titleFirst-Order and Temporal Logics for Nested Wordses_ES
dc.typecomunicación de congreso
sipa.codpersvinculados81488
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
First-Order and Temporal Logics for Nested Words.pdf
Size:
2.74 KB
Format:
Adobe Portable Document Format
Description:
Download
Collections
Artículos de conferencia