A practical decision procedure for propositional projection temporal logic with infinite models

DOI10.1016/j.tcs.2014.02.011zbMath1358.68188OpenAlexW2020639449MaRDI QIDQ744099

Cong Tian, Zhenhua Duan

Publication date: 6 October 2014

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

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

zbMATH Keywords

algorithmautomatadecision procedureBüchi accepting conditionpropositional projection temporal logic

Mathematics Subject Classification ID

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

Related Items

Model Checking MSVL Programs Based on Dynamic Symbolic Execution ⋮ A canonical form based decision procedure and model checking approach for propositional projection temporal logic ⋮ A complete axiom system for propositional projection temporal logic with cylinder computation model ⋮ Verifying a scheduling protocol of safety-critical systems ⋮ A temporal logic programming approach to planning ⋮ Model checking of pushdown systems for projection temporal logic ⋮ Efficient decision procedure for propositional projection temporal logic ⋮ A sound and complete proof system for a unified temporal logic ⋮ A decision procedure and complete axiomatization for projection temporal logic ⋮ Model checking Petri nets with MSVL ⋮ Translating Xd-C programs to MSVL programs ⋮ Satisfiability of Linear Time Mu-Calculus on Finite Traces ⋮ Index set expressions can represent temporal logic formulas

Cites Work

• A decision procedure for propositional projection temporal logic with infinite models
• The Büchi Complementation Saga
• Unnamed Item
• Unnamed Item