Temporal logic and model checking for operator precedence languages

MaRDI QIDQ3384888zbMATH OpenFDO

Authors Michele Chiari, Dino Mandrioli, Matteo Pradella

Publication date 17 December 2021

Full work available at URL https://arxiv.org/abs/1809.03100, http://eptcs.web.cse.unsw.edu.au/paper.cgi?GandALF18.12

zbMATH Keywords

input driven languageslinear temporal logicmodel checkingoperator precedence languagesvisibly pushdown languages

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Applications of game theory (91A80)

Recommendations

• Operator precedence temporal logic and model checking
• Operator precedence languages: their automata-theoretic and logic characterization
• A first-order complete temporal logic for structured context-free languages
• Operator precedence and the visibly pushdown property
• Model-checking structured context-free languages

Cites work

• A theory of timed automata
• 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
• First-Order and Temporal Logics for Nested Words
• Generalizing input-driven languages: theoretical and practical benefits
• scientific article; zbMATH DE number 3876636 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 2079028 (Why is no real title available?)
• scientific article; zbMATH DE number 3368555 (Why is no real title available?)
• Operator precedence and the visibly pushdown property
• Operator precedence languages: their automata-theoretic and logic characterization
• Parenthesis Grammars
• Parsing Techniques
• Pushdown processes: Games and model-checking
• Reachability analysis of pushdown automata: Application to model-checking
• Syntactic Analysis and Operator Precedence
• The complexity of first-order and monadic second-order logic revisited
• Weak Second‐Order Arithmetic and Finite Automata

Cited in

(6)

• Loop-check specification for a sequent calculus of temporal logic
• Operator precedence temporal logic and model checking
• scientific article; zbMATH DE number 7020139 (Why is no real title available?)
• Model Theoretic Syntax and Parsing
• A first-order complete temporal logic for structured context-free languages
• Model-checking structured context-free languages

This page was built for publication: Temporal logic and model checking for operator precedence languages

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