A first-order complete temporal logic for structured context-free languages

MaRDI QIDQ5101344zbMATH OpenFDO

Authors Michele Chiari, Dino Mandrioli, Matteo Pradella

Publication date 30 August 2022

Full work available at URL https://arxiv.org/abs/2105.10740, https://lmcs.episciences.org/9863

zbMATH Keywords

first-order completenessinput-driven languagelinear temporal logicmodel checkingoperator-precedence languagesvisibly pushdown languages

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Recommendations

• Model-checking structured context-free languages
• Operator precedence temporal logic and model checking
• Temporal logic and model checking for operator precedence languages
• Tools and Algorithms for the Construction and Analysis of Systems
• First-Order and Temporal Logics for Nested Words

Cites work

• Adding nesting structure to words
• Algebraic properties of operator precedence languages
• Characterizing derivation trees of context-free grammars through a generalization of finite automata theory
• Colored Nested Words
• Constrained properties, semilinear systems, and Petri nets
• Finite model theory and its applications.
• First-Order and Temporal Logics for Nested Words
• First-order properties of trees, star-free expressions, and aperiodicity
• Generalizing input-driven languages: theoretical and practical benefits
• scientific article; zbMATH DE number 1670555 (Why is no real title available?)
• scientific article; zbMATH DE number 1670780 (Why is no real title available?)
• scientific article; zbMATH DE number 3888931 (Why is no real title available?)
• scientific article; zbMATH DE number 4027441 (Why is no real title available?)
• scientific article; zbMATH DE number 747023 (Why is no real title available?)
• scientific article; zbMATH DE number 3696500 (Why is no real title available?)
• scientific article; zbMATH DE number 3639163 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 1980931 (Why is no real title available?)
• scientific article; zbMATH DE number 2079028 (Why is no real title available?)
• scientific article; zbMATH DE number 1852915 (Why is no real title available?)
• scientific article; zbMATH DE number 3368555 (Why is no real title available?)
• scientific article; zbMATH DE number 3079563 (Why is no real title available?)
• Limiting Until in ordered tree query languages
• Model checking LTL with regular valuations for pushdown systems
• Model checking procedural programs
• Model-checking structured context-free languages
• Operator precedence and the visibly pushdown property
• Operator precedence languages: their automata-theoretic and logic characterization
• Operator precedence temporal logic and model checking
• Parenthesis Grammars
• Parsing Techniques
• Predicate abstraction for program verification
• Reachability analysis of pushdown automata: Application to model-checking
• Reasoning about XML with temporal logics and automata
• Star-freeness, first-order definability and aperiodicity of structured context-free languages
• Syntactic Analysis and Operator Precedence
• Timed context-free temporal logics
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Visibly linear temporal logic
• Visibly pushdown languages

Cited in

(2)

• Temporal logic and model checking for operator precedence languages
• Aperiodicity, Star-freeness, and First-order Logic Definability of Operator Precedence Languages

Describes a project that uses

Uses Software

• Bebop

This page was built for publication: A first-order complete temporal logic for structured context-free languages

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5101344)