A proof system for unified temporal logic

DOI10.1016/j.tcs.2023.113702OpenAlexW4317473253MaRDI QIDQ2686105

Zhenhua Duan, Nan Zhang, Cong Tian, Chaofeng Yu

Publication date: 24 February 2023

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

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

zbMATH Keywords

formal verificationinference ruleproof systemaxiomunified temporal logic

Mathematics Subject Classification ID

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

Uses Software

• CESAR

Cites Work

• A complete proof system for propositional projection temporal logic
• Efficient SAT-based bounded model checking for software verification
• Symbolic model checking: \(10^{20}\) states and beyond
• Expressiveness and completeness of an interval tense logic
• Unified temporal logic
• Counterexample-guided abstraction refinement for symbolic model checking
• A Hierarchical Completeness Proof for Propositional Interval Temporal Logic with Finite Time
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• A propositional modal logic of time intervals
• Complete Proof System for QPTL
• An axiomatic basis for computer programming
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A proof system for unified temporal logic