Model checking of pushdown systems for projection temporal logic

DOI10.1016/j.tcs.2016.06.031zbMath1423.68297OpenAlexW2461667266MaRDI QIDQ2424879

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

complexityalgorithmmodel checkingpushdown systemprojection temporal logicfull regular expressiveness

Mathematics Subject Classification ID

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

Uses Software

• SPIN
• CESAR
• LTL2BA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A practical decision procedure for propositional projection temporal logic with infinite models
• The temporal semantics of concurrent programs
• Pushdown processes: Games and model-checking
• Expressiveness of propositional projection temporal logic with star
• Temporal logic can be more expressive
• SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR
• Graph-Based Algorithms for Boolean Function Manipulation
• Alternation
• Logic Programming
• Reachability analysis of pushdown automata: Application to model-checking