Aperiodicity, Star-freeness, and First-order Logic Definability of Operator Precedence Languages
From MaRDI portal
Publication:6137830
DOI10.46298/LMCS-19(4:12)2023arXiv2006.01236MaRDI QIDQ6137830FDOQ6137830
Stefano Crespi Reghizzi, Matteo Pradella, Dino Mandrioli
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
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A Proof of Kamp's theorem
- Adding nesting structure to words
- Parenthesis Grammars
- Weak Second‐Order Arithmetic and Finite Automata
- Decision Problems of Finite Automata Design and Related Arithmetics
- Characterizing derivation trees of context-free grammars through a generalization of finite automata theory
- Counter-Free Input-Determined Timed Automata
- FINE HIERARCHY OF REGULAR APERIODIC ω-LANGUAGES
- On ω-regular sets
- First-Order and Temporal Logics for Nested Words
- Parsing Techniques
- Piecewise testable tree languages
- Synchronization of Pushdown Automata
- Syntactic Analysis and Operator Precedence
- Operator precedence and the visibly pushdown property
- Operator Precedence Languages: Their Automata-Theoretic and Logic Characterization
- Algebraic properties of operator precedence languages
- The use of grammatical inference for designing programming languages
- Generalizing input-driven languages: theoretical and practical benefits
- Star-freeness, first-order definability and aperiodicity of structured context-free languages
- Operator precedence temporal logic and model checking
- Visibly Linear Temporal Logic
- Model-checking structured context-free languages
- First-order logic on finite trees
- A descriptive characterisation of linear languages
- First-order properties of trees, star-free expressions, and aperiodicity
- Modulo-counting quantifiers over finite trees
- Noncounting Context-Free Languages
- Aperiodicity in Tree Automata
- Colored Nested Words
- First-Order Logic Definability of Free Languages
- Height-Deterministic Pushdown Automata
- Operator Precedence Grammars and the Noncounting Property
- Beyond operator-precedence grammars and languages
- A decidable characterization of locally testable tree languages
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)
