Operator precedence temporal logic and model checking

DOI10.1016/J.TCS.2020.08.034MaRDI QIDQ2215961zbMATH OpenOpenAlexFDO

Authors Michele Chiari, Matteo Pradella, Dino Mandrioli

Publication date 15 December 2020

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/11311/1150413

zbMATH Keywords

model checkingtemporal logic\(\omega\)-languagesvisibly pushdown languagesoperator precedence languagesinput driven languages

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Recommendations

• Operator precedence languages: their automata-theoretic and logic characterization
• Precedence automata and languages
• Verification of programs with exceptions through operator precedence automata
• Operator precedence and the visibly pushdown property
• Model-checking structured context-free languages

Cites work

• 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 3876636 (Why is no real title available?)
• scientific article; zbMATH DE number 7447741 (Why is no real title available?)
• scientific article; zbMATH DE number 747023 (Why is no real title available?)
• scientific article; zbMATH DE number 522865 (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 1903366 (Why is no real title available?)
• scientific article; zbMATH DE number 3368555 (Why is no real title available?)
• A theory of timed automata
• Adding nesting structure to words
• Algebraic properties of operator precedence languages
• An axiomatic basis for computer programming
• Characterizing derivation trees of context-free grammars through a generalization of finite automata theory
• Colored Nested Words
• First-Order and Temporal Logics for Nested Words
• First-order properties of trees, star-free expressions, and aperiodicity
• Formal languages and compilation
• Generalizing input-driven languages: theoretical and practical benefits
• Marrying Words and Trees
• Model checking LTL with regular valuations for pushdown systems
• Operator precedence languages: their automata-theoretic and logic characterization
• Operator precedence and the visibly pushdown property
• 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
• Tools and Algorithms for the Construction and Analysis of Systems
• Weak Second‐Order Arithmetic and Finite Automata

Cited in

(5)

• Model-checking structured context-free languages
• Aperiodicity, Star-freeness, and First-order Logic Definability of Operator Precedence Languages
• scientific article; zbMATH DE number 7577575 (Why is no real title available?)
• Verification of programs with exceptions through operator precedence automata
• Temporal logics with language parameters

This page was built for publication: Operator precedence temporal logic and model checking

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