Present-Future Form of Linear Time $$ mu $$ -Calculus. - Yao Liu 010; Zhenhua Duan; Cong Tian; Bo Liu (SOFL+MSVL, 2013)

An Improved Recursive Algorithm for Parity Games. - Yao Liu 010; Zhenhua Duan; Cong Tian (TASE, 2014)

An Improved Decision Procedure for Linear Time Mu-Calculus. - Yao Liu 010; Zhenhua Duan; Cong Tian (CoRR, 2015)

Satisfiability of Linear Time Mu-Calculus on Finite Traces. - Yao Liu 010; Zhenhua Duan; Cong Tian; Bin Cui 001 (COCOON, 2016)

A Decision Procedure for a Fragment of Linear Time Mu-Calculus. - Yao Liu 010; Zhenhua Duan; Cong Tian (IJCAI, 2016)