Operator precedence temporal logic and model checking

DOI10.1016/j.tcs.2020.08.034zbMath1464.68197OpenAlexW3083113755MaRDI QIDQ2215961

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)

Related Items (6)

Model-checking structured context-free languages ⋮ Verification of programs with exceptions through operator precedence automata ⋮ Aperiodicity, Star-freeness, and First-order Logic Definability of Operator Precedence Languages ⋮ Model Checking Temporal Properties of Recursive Probabilistic Programs ⋮ Temporal logics with language parameters ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A theory of timed automata
• Generalizing input-driven languages: theoretical and practical benefits
• Operator precedence and the visibly pushdown property
• Pushdown processes: Games and model-checking
• The complexity of first-order and monadic second-order logic revisited
• Model checking LTL with regular valuations for pushdown systems
• Characterizing derivation trees of context-free grammars through a generalization of finite automata theory
• Colored Nested Words
• Operator Precedence Languages: Their Automata-Theoretic and Logic Characterization
• Weak Second‐Order Arithmetic and Finite Automata
• Adding nesting structure to words
• Marrying Words and Trees
• First-Order and Temporal Logics for Nested Words
• First-order properties of trees, star-free expressions, and aperiodicity
• Algebraic properties of operator precedence languages
• Tools and Algorithms for the Construction and Analysis of Systems
• Syntactic Analysis and Operator Precedence
• Parsing Techniques
• Parenthesis Grammars
• An axiomatic basis for computer programming
• Formal languages and compilation
• Reachability analysis of pushdown automata: Application to model-checking

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