Aperiodicity, Star-freeness, and First-order Logic Definability of Operator Precedence Languages
From MaRDI portal
Publication:6137830
DOI10.46298/LMCS-19(4:12)2023MaRDI QIDQ6137830FDOQ6137830
Authors: Dino Mandrioli, Matteo Pradella, Stefano Crespi Reghizzi 
Publication date: 16 January 2024
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Abstract: A classic result in formal language theory is the equivalence among noncounting, or aperiodic, regular languages, and languages defined through star-free regular expressions, or first-order logic. Together with first-order completeness of linear temporal logic these results constitute a theoretical foundation for model-checking algorithms. Extending these results to structured subclasses of context-free languages, such as tree-languages did not work as smoothly: for instance W. Thomas showed that there are star-free tree languages that are counting. We show, instead, that investigating the same properties within the family of operator precedence languages leads to equivalences that perfectly match those on regular languages. The study of this old family of context-free languages has been recently resumed to enhance not only parsing (the original motivation of its inventor R. Floyd) but also to exploit their algebraic and logic properties. We have been able to reproduce the classic results of regular languages for this much larger class by going back to string languages rather than tree languages. Since operator precedence languages strictly include other classes of structured languages such as visibly pushdown languages, the same results given in this paper hold as trivial corollary for that family too.
Full work available at URL: https://arxiv.org/abs/2006.01236
aperiodicityfirst-order logicvisibly pushdown languagesinput-driven languagesoperator precedence languagesstar-free expressionsstructured languages
Cites Work
- scientific article; zbMATH DE number 3888931 (Why is no real title available?)
- scientific article; zbMATH DE number 3876636 (Why is no real title available?)
- scientific article; zbMATH DE number 3639163 (Why is no real title available?)
- scientific article; zbMATH DE number 1304310 (Why is no real title available?)
- scientific article; zbMATH DE number 1142314 (Why is no real title available?)
- scientific article; zbMATH DE number 2079028 (Why is no real title available?)
- scientific article; zbMATH DE number 1860667 (Why is no real title available?)
- scientific article; zbMATH DE number 7577575 (Why is no real title available?)
- scientific article; zbMATH DE number 3368555 (Why is no real title available?)
- scientific article; zbMATH DE number 3413820 (Why is no real title available?)
- A Proof of Kamp's theorem
- A decidable characterization of locally testable tree languages
- A descriptive characterisation of linear languages
- Adding nesting structure to words
- Algebraic properties of operator precedence languages
- Aperiodicity in Tree Automata
- Beyond operator-precedence grammars and languages
- Characterizing derivation trees of context-free grammars through a generalization of finite automata theory
- Colored Nested Words
- Counter-Free Input-Determined Timed Automata
- Decision Problems of Finite Automata Design and Related Arithmetics
- FINE HIERARCHY OF REGULAR APERIODIC ω-LANGUAGES
- First-Order and Temporal Logics for Nested Words
- First-order definable languages
- First-order logic definability of free languages
- First-order logic on finite trees
- First-order properties of trees, star-free expressions, and aperiodicity
- Generalizing input-driven languages: theoretical and practical benefits
- Height-Deterministic Pushdown Automata
- Model-checking structured context-free languages
- Modulo-counting quantifiers over finite trees
- Noncounting Context-Free Languages
- On ω-regular sets
- Operator Precedence Grammars and the Noncounting Property
- Operator Precedence Languages: Their Automata-Theoretic and Logic Characterization
- Operator precedence and the visibly pushdown property
- Operator precedence temporal logic and model checking
- Parenthesis Grammars
- Parsing Techniques
- Piecewise testable tree languages
- Star-freeness, first-order definability and aperiodicity of structured context-free languages
- Synchronization of Pushdown Automata
- Syntactic Analysis and Operator Precedence
- The use of grammatical inference for designing programming languages
- Visibly linear temporal logic
- Weak Second‐Order Arithmetic and Finite Automata
This page was built for publication: Aperiodicity, Star-freeness, and First-order Logic Definability of Operator Precedence Languages
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6137830)
