First-Order and Temporal Logics for Nested Words

Rajeev Alur; Marcelo Arenas; Pablo Barcelo; Kousha Etessami; Neil Immerman; Leonid Libkin

doi:10.2168/LMCS-4(4:11)2008

Rajeev Alur ; Marcelo Arenas ; Pablo Barcelo ; Kousha Etessami ; Neil Immerman ; Leonid Libkin - First-Order and Temporal Logics for Nested Words

lmcs:782 - Logical Methods in Computer Science, November 25, 2008, Volume 4, Issue 4 - https://doi.org/10.2168/LMCS-4(4:11)2008

First-Order and Temporal Logics for Nested WordsArticle

Authors: Rajeev Alur ; Marcelo Arenas ; Pablo Barcelo ; Kousha Etessami ; Neil Immerman ; Leonid Libkin

Nested 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 (RSMs). The other logic, NWTL, is based on the notion of a summary path that uses both the linear and nesting structures. For NWTL we show that satisfiability is EXPTIME-complete, and that model-checking can be done in time polynomial in the size of the RSM model and exponential in the size of the NWTL formula (and is also 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.

Comment: revised and corrected version of Mar 03, 2011

https://doi.org/10.2168/LMCS-4(4:11)2008

Source: arXiv.org:0811.0537

Volume: Volume 4, Issue 4

Secondary volumes: Selected Papers of the 22nd IEEE Symposium on Logic in Computer Science (LICS 2007)

Published on: November 25, 2008

Imported on: January 17, 2008

Keywords: Computer Science - Logic in Computer Science, F.1.1, F.3.1, F.4.1

Licence: arXiv.org - Non-exclusive license to distribute

Funding:

Source : OpenAIRE Graph

Synaptic Mechanisms for the Processing of Temporal Codes; Funder: National Science Foundation; Code: 1050701
Variables versus Size: Tradeoffs in Descriptive Complexity; Funder: National Science Foundation; Code: 0830174
Behavioral Interfaces for Software Components; Funder: National Science Foundation; Code: 0541149
Collaborative Research: Advanced Static-Analysis Techniques for Ensuring Reliable Software; Funder: National Science Foundation; Code: 0541018

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

33 Documents citing this article

Michele Chiari;Luca Geatti;Nicola Gigante;Matteo Pradella, 2024, SMT-Based Symbolic Model-Checking for Operator Precedence Languages, Lecture notes in computer science, pp. 387-408, 10.1007/978-3-031-65627-9_19, https://doi.org/10.1007/978-3-031-65627-9_19.

Michele Chiari;Dino Mandrioli;Francesco Pontiggia;Matteo Pradella, 2023, A Model Checker for Operator Precedence Languages, ACM Transactions on Programming Languages and Systems, 45, 3, pp. 1-66, 10.1145/3608443, https://doi.org/10.1145/3608443.

Roman Lakenbrink;Markus Müller-Olm;Christoph Ohrem;Jens Gutsfeld, 2023, A Navigation Logic for Recursive Programs with Dynamic Thread Creation, Lecture notes in computer science, pp. 48-70, 10.1007/978-3-031-50521-8_3.

Michele Chiari, 2022, Temporal Logic and Model Checking for Operator Precedence Languages: Theory and Applications, SpringerBriefs in applied sciences and technology, pp. 67-78, 10.1007/978-3-031-15374-7_6, https://doi.org/10.1007/978-3-031-15374-7_6.

Francesco Pontiggia;Michele Chiari;Matteo Pradella, 2021, Verification of Programs with Exceptions Through Operator Precedence Automata, Virtual Community of Pathological Anatomy (University of Castilla La Mancha), pp. 293-311, 10.1007/978-3-030-92124-8_17, https://link.springer.com/chapter/10.1007/978-3-030-92124-8_17.

Dino Mandrioli;Matteo Pradella;Stefano Crespi Reghizzi, 2020, Star-Freeness, First-Order Definability and Aperiodicity of Structured Context-Free Languages, Virtual Community of Pathological Anatomy (University of Castilla La Mancha), pp. 161-180, 10.1007/978-3-030-64276-1_9, http://hdl.handle.net/11311/1156727.

Michele Chiari;Dino Mandrioli;Matteo Pradella, 2020, Operator precedence temporal logic and model checking, Virtual Community of Pathological Anatomy (University of Castilla La Mancha), 848, pp. 47-81, 10.1016/j.tcs.2020.08.034, http://hdl.handle.net/11311/1150413.

Emmanuel Filiot;Jean-François Raskin;Pierre-Alain Reynier;Frédéric Servais;Jean-Marc Talbot, 2018, Visibly pushdown transducers, 97, pp. 147-181, 10.1016/j.jcss.2018.05.002, https://hal.science/hal-02093318.

Jens Oliver Gutsfeld;Markus Müller-Olm;Benedikt Nordhoff, 2018, A Branching Time Variant of CaRet, Lecture notes in computer science, pp. 153-170, 10.1007/978-3-319-94111-0_9.

Michele Chiari;Dino Mandrioli;Matteo Pradella, 2018, Temporal Logic and Model Checking for Operator Precedence Languages, Electronic Proceedings in Theoretical Computer Science, 277, pp. 161-175, 10.4204/eptcs.277.12, https://doi.org/10.4204/eptcs.277.12.

Yuki Satake;Hiroshi Unno, 2018, Propositional Dynamic Logic for Higher-Order Functional Programs, Lecture notes in computer science, pp. 105-123, 10.1007/978-3-319-96145-3_6, https://doi.org/10.1007/978-3-319-96145-3_6.

Dino Mandrioli;Matteo Pradella, 2017, Generalizing input-driven languages: Theoretical and practical benefits, arXiv (Cornell University), 27, pp. 61-87, 10.1016/j.cosrev.2017.12.001, http://arxiv.org/abs/1705.00984.

I. De Crescenzo;S. La Torre;Y. Velner, 2016, Visibly pushdown modular games,, Information and Computation, 253, pp. 204-223, 10.1016/j.ic.2016.07.007.

Manfred Droste;Stefan Dück, 2016, Weighted automata and logics for infinite nested words, Information and Computation, 253, pp. 448-466, 10.1016/j.ic.2016.06.010.

Stefano Crespi Reghizzi;Violetta Lonati;Dino Mandrioli;Matteo Pradella, 2016, Toward a theory of input-driven locally parsable languages, Virtual Community of Pathological Anatomy (University of Castilla La Mancha), 658, pp. 105-121, 10.1016/j.tcs.2016.05.003, http://hdl.handle.net/11311/999581.

Fu Song;Tayssir Touili, 2015, Model-checking software library API usage rules, Software & Systems Modeling, 15, 4, pp. 961-985, 10.1007/s10270-015-0473-1.

Violetta Lonati;Dino Mandrioli;Federica Panella;Matteo Pradella, 2015, First-Order Logic Definability of Free Languages, Virtual Community of Pathological Anatomy (University of Castilla La Mancha), pp. 310-324, 10.1007/978-3-319-20297-6_20, http://hdl.handle.net/11311/964071.

Ilaria De Crescenzo;Salvatore La Torre;Yaron Velner, 2014, Visibly Pushdown Modular Games, Electronic Proceedings in Theoretical Computer Science, 161, pp. 260-274, 10.4204/eptcs.161.22, https://doi.org/10.4204/eptcs.161.22.

Manfred Droste;Stefan Dück, 2014, Weighted Automata and Logics for Infinite Nested Words, arXiv (Cornell University), pp. 323-334, 10.1007/978-3-319-04921-2_26, http://arxiv.org/abs/1506.07031.

Benedikt Bollig;Dietrich Kuske;Roy Mennicke, 2013, The Complexity of Model Checking Multi-stack Systems, pp. 163-172, 10.1109/lics.2013.22.

Benedikt Bollig;Paul Gastin;Benjamin Monmege, 2013, Weighted Specifications over Nested Words, pp. 385-400, 10.1007/978-3-642-37075-5_25, https://hal.science/hal-00909035.

Benjamin Aminof;Fabio Mogavero;Aniello Murano, 2013, Synthesis of hierarchical systems, Science of Computer Programming, 83, pp. 56-79, 10.1016/j.scico.2013.07.001.

Normann Decker;Martin Leucker;Daniel Thoma, 2013, Impartiality and Anticipation for Monitoring of Visibly Context-Free Properties, Lecture notes in computer science, pp. 183-200, 10.1007/978-3-642-40787-1_11.

Benjamin Aminof;Fabio Mogavero;Aniello Murano, 2012, Synthesis of Hierarchical Systems, Lecture notes in computer science, pp. 42-60, 10.1007/978-3-642-35743-5_4.

Salvatore La Torre;Margherita Napoli, 2012, A Temporal Logic for Multi-threaded Programs, pp. 225-239, 10.1007/978-3-642-33475-7_16, https://inria.hal.science/hal-01556217.

Benedikt Bollig;Aiswarya Cyriac;Paul Gastin;Marc Zeitoun, 2011, Temporal Logics for Concurrent Recursive Programs: Satisfiability and Model Checking, pp. 132-144, 10.1007/978-3-642-22993-0_15, https://hal.science/hal-00591139.

Christian Dax;Felix Klaedtke, 2011, Alternation Elimination for Automata over Nested Words, Repository for Publications and Research Data (ETH Zurich), pp. 168-183, 10.1007/978-3-642-19805-2_12, http://hdl.handle.net/20.500.11850/69583.

Laura Bozzelli;Ruggero Lanotte, 2011, Hybrid and First-Order Complete Extensions of CaRet, Lecture notes in computer science, pp. 58-72, 10.1007/978-3-642-22119-4_7.

M. Shoaran;A. Thomo, 2011, Evolving schemas for streaming XML, Theoretical Computer Science, 412, 35, pp. 4545-4557, 10.1016/j.tcs.2011.04.037.

Yoad Lustig;Moshe Vardi, 2011, Synthesis from Recursive-Components Libraries, Electronic Proceedings in Theoretical Computer Science, 54, pp. 1-16, 10.4204/eptcs.54.1, https://doi.org/10.4204/eptcs.54.1.

Christian Mathissen, 2010, Weighted Logics for Nested Words and Algebraic Formal Power Series, Logical Methods in Computer Science, Volume 6, Issue 1, 10.2168/lmcs-6(1:5)2010, https://doi.org/10.2168/lmcs-6(1:5)2010.

Marcelo Arenas;Pablo Barceló;Leonid Libkin, 2010, Regular Languages of Nested Words: Fixed Points, Automata, and Synchronization, Americanae (AECID Library), 49, 3, pp. 639-670, 10.1007/s00224-010-9292-5, http://americanae.aecid.es/americanae/es/registros/registro.do?tipoRegistro=MTD&idBib=3303877.

Maryam Shoaran;Alex Thomo, 2010, Evolving Schemas for Streaming XML, Lecture notes in computer science, pp. 266-285, 10.1007/978-3-642-11829-6_18.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3941 times.

This article's PDF has been downloaded 600 times.