Author name cluster

Chaofeng Yu

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

1 author row

TCS Journal 2025 Journal Article

SAT-based bounded model checking for propositional projection temporal logic

Zhenhua Duan
Cong Tian
Nan Zhang
Chaofeng Yu
Mengfei Yang
Jia He

This paper presents a bounded model checking (BMC) approach for propositional projection temporal logic (PPTL). To this end, first PPTL is briefly introduced. Then, bounded semantics of PPTL is defined according to its semantics in logic theory. Further, a reduction method from BMC to SAT is given in detail. In addition, an example is presented to illustrate how the approach works. Finally, miniSAT is employed to solve the SAT based BMC problem by means of verifying RMS algorithm in detail. Our experience shows that SAT based BMC approach for PPTL proposed in the paper is useful and feasible.

Details DOI

TCS Journal 2023 Journal Article

A proof system for unified temporal logic

Nan Zhang
Chaofeng Yu
Zhenhua Duan
Cong Tian

Unified Temporal Logic (UTL) combines all characteristics of traditional Linear Temporal Logic (LTL) and Propositional Projection Temporal Logic (PPTL). It can be used to describe full regular and omega-regular properties, which are often encountered in the field of formal verification. To support formal verification with UTL, this paper proposes a proof system for UTL. First, the syntax and semantics of UTL are briefly introduced. Further, axioms and inference rules are formalized. Besides, a number of theorems are derived and proved to refine the system. Moreover, the soundness and completeness of the proof system are proved in detail. To facilitate the completeness proof, some auxiliary lemmas are introduced and proved in advance. Finally, an example is given to illustrate how to use this proof system for verifying properties of a system.

Details DOI