A canonical form based decision procedure and model checking approach for propositional projection temporal logic
DOI10.1016/J.TCS.2015.08.039zbMATH Open1370.68200OpenAlexW1835747325MaRDI QIDQ896152FDOQ896152
Zhenhua Duan, Nan Zhang, Cong Tian
Publication date: 11 December 2015
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2015.08.039
Recommendations
- An efficient decision procedure for propositional projection temporal logic
- A decision procedure for propositional projection temporal logic with infinite models
- Efficient decision procedure for propositional projection temporal logic
- A practical decision procedure for propositional projection temporal logic with infinite models
- Complexity of propositional projection temporal logic with star
model checkinginterval temporal logicspecificationdecision procedureautomatic verification[https://portal.mardi4nfdi.de/w/index.php?title=+Special%3ASearch&search=B%EF%BF%BD%EF%BF%BDchi+automata&go=Go B��chi automata]linear-time temporal logicpropositional projection temporal logic
Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)
Cites Work
- Counterexample-guided abstraction refinement for symbolic model checking
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A decision procedure for propositional projection temporal logic with infinite models
- Complexity of propositional projection temporal logic with star
- Title not available (Why is that?)
- Expressiveness of propositional projection temporal logic with star
- A practical decision procedure for propositional projection temporal logic with infinite models
- Title not available (Why is that?)
- Bounded model checking of traffic light control system
- Propositional Projection Temporal Logic, B $\ddot{u}$ chi Automata and ω-Regular Expressions
Cited In (7)
- An approach to agent path planning under temporal logic constraints
- A decision procedure and complete axiomatization for projection temporal logic
- Efficient decision procedure for propositional projection temporal logic
- PPTL specification mining based on LNFG
- Index set expressions can represent temporal logic formulas
- Temporal logic specification mining of programs
- Verifying a scheduling protocol of safety-critical systems
Uses Software
This page was built for publication: A canonical form based decision procedure and model checking approach for propositional projection temporal logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q896152)
