Model checking of pushdown systems for projection temporal logic

DOI10.1016/J.TCS.2016.06.031MaRDI QIDQ2424879zbMATH OpenOpenAlexFDO

Authors Yanyan Li

Publication date 25 June 2019

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

Full work available at URL https://doi.org/10.1016/j.tcs.2016.06.031

zbMATH Keywords

algorithmcomplexityfull regular expressivenessmodel checkingprojection temporal logicpushdown system

Mathematics Subject Classification ID

Temporal logic (03B44) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A symbolic model checker for propositional projection temporal logic
• Bounded model checking for propositional projection temporal logic
• Verification, Model Checking, and Abstract Interpretation
• scientific article; zbMATH DE number 2080197
• Symbolic model checking for alternating projection temporal logic
• Model checking open systems with alternating projection temporal logic
• Model-checking timed temporal logics
• Model-Checking HyperLTL for Pushdown Systems

Cites work

• A practical decision procedure for propositional projection temporal logic with infinite models
• Alternation
• Expressiveness of propositional projection temporal logic with star
• Graph-Based Algorithms for Boolean Function Manipulation
• scientific article; zbMATH DE number 438994 (Why is no real title available?)
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 4076583 (Why is no real title available?)
• scientific article; zbMATH DE number 1142314 (Why is no real title available?)
• scientific article; zbMATH DE number 2080197 (Why is no real title available?)
• scientific article; zbMATH DE number 1517989 (Why is no real title available?)
• scientific article; zbMATH DE number 1796123 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Logic Programming
• Pushdown processes: Games and model-checking
• Reachability analysis of pushdown automata: Application to model-checking
• SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR
• Temporal logic can be more expressive
• The temporal semantics of concurrent programs

Cited in

(8)

• Natural projection as partial model checking
• Complexity results on branching-time pushdown model checking
• Model checking open systems with alternating projection temporal logic
• scientific article; zbMATH DE number 2080197 (Why is no real title available?)
• From Model Checking to a Temporal Proof for Partial Models
• Model-Checking HyperLTL for Pushdown Systems
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation

Describes a project that uses

Uses Software

• CESAR
• SPIN
• LTL2BA

This page was built for publication: Model checking of pushdown systems for projection temporal logic

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