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 et al. - 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.

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

Source: arXiv.org:0811.0537

Volume: Volume 4, Issue 4

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

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
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

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

32 Documents citing this article

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, Lecture notes in computer science, A Navigation Logic for Recursive Programs with Dynamic Thread Creation, pp. 48-70, 2023, 10.1007/978-3-031-50521-8_3.

Michele Chiari, SpringerBriefs in applied sciences and technology, Temporal Logic and Model Checking for Operator Precedence Languages: Theory and Applications, pp. 67-78, 2022, 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, Virtual Community of Pathological Anatomy (University of Castilla La Mancha), Verification of Programs with Exceptions Through Operator Precedence Automata, pp. 293-311, 2021, 10.1007/978-3-030-92124-8_17, http://hdl.handle.net/11311/1199461.

Dino Mandrioli;Matteo Pradella;Stefano Crespi Reghizzi, Virtual Community of Pathological Anatomy (University of Castilla La Mancha), Star-Freeness, First-Order Definability and Aperiodicity of Structured Context-Free Languages, pp. 161-180, 2020, 10.1007/978-3-030-64276-1_9, https://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, Journal of Computer and System Sciences, 97, pp. 147-181, 10.1016/j.jcss.2018.05.002, https://doi.org/10.1016/j.jcss.2018.05.002.

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

Michele Chiari;Dino Mandrioli;Matteo Pradella, 2018, Temporal Logic and Model Checking for Operator Precedence Languages, arXiv (Cornell University), 277, pp. 161-175, 10.4204/eptcs.277.12.

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

Dino Mandrioli;Matteo Pradella, 2017, Generalizing input-driven languages: Theoretical and practical benefits, Virtual Community of Pathological Anatomy (University of Castilla La Mancha), 27, pp. 61-87, 10.1016/j.cosrev.2017.12.001, http://hdl.handle.net/11311/1046282.

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, https://doi.org/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, https://doi.org/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, Theoretical Computer Science, 658, pp. 105-121, 10.1016/j.tcs.2016.05.003, https://doi.org/10.1016/j.tcs.2016.05.003.

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, Virtual Community of Pathological Anatomy (University of Castilla La Mancha), First-Order Logic Definability of Free Languages, pp. 310-324, 2015, 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, arXiv (Cornell University), 161, pp. 260-274, 10.4204/eptcs.161.22.

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

Benedikt Bollig;Dietrich Kuske;Roy Mennicke, CiteSeer X (The Pennsylvania State University), The Complexity of Model Checking Multi-stack Systems, pp. 163-172, 2013, New Orleans, LA, USA, 10.1109/lics.2013.22, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.378.9468.

Benedikt Bollig;Paul Gastin;Benjamin Monmege, Lecture notes in computer science, Weighted Specifications over Nested Words, pp. 385-400, 2013, 10.1007/978-3-642-37075-5_25, https://doi.org/10.1007/978-3-642-37075-5_25.

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, https://doi.org/10.1016/j.scico.2013.07.001.

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

Benjamin Aminof;Fabio Mogavero;Aniello Murano, CiteSeer X (The Pennsylvania State University), Synthesis of Hierarchical Systems, pp. 42-60, 2012, 10.1007/978-3-642-35743-5_4, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.419.4106.

Salvatore La Torre;Margherita Napoli, Lecture notes in computer science, A Temporal Logic for Multi-threaded Programs, pp. 225-239, 2012, 10.1007/978-3-642-33475-7_16, https://doi.org/10.1007/978-3-642-33475-7_16.

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

Christian Dax;Felix Klaedtke, Lecture notes in computer science, Alternation Elimination for Automata over Nested Words, pp. 168-183, 2011, 10.1007/978-3-642-19805-2_12, https://doi.org/10.1007/978-3-642-19805-2_12.

Laura Bozzelli;Ruggero Lanotte, Lecture notes in computer science, Hybrid and First-Order Complete Extensions of CaRet, pp. 58-72, 2011, 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, https://doi.org/10.1016/j.tcs.2011.04.037.

Yoad Lustig;Moshe Vardi, 2011, Synthesis from Recursive-Components Libraries, arXiv (Cornell University), 54, pp. 1-16, 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, Edinburgh Research Explorer (University of Edinburgh), 49, 3, pp. 639-670, 10.1007/s00224-010-9292-5, https://www.pure.ed.ac.uk/ws/files/17831446/Arenas_Barcelo_ET_AL_2011_Regular_Languages_of_Nested_Words_Fixed_Points_Automata_and_Synchronization.pdf.

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

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 2102 times.

This article's PDF has been downloaded 404 times.