A Hybrid Clock System Related to STeC Language. - Yixiang Chen 001; Yuanrui Zhang 001 (SERE (Companion), 2014)

Timed Automata Semantics of Spatial-Temporal Consistency Language STeC. - Yuanrui Zhang 001; Frédéric Mallet; Yixiang Chen 001 (TASE, 2014)

A Framework for Data-Driven Automata Design. - Yuanrui Zhang 001; Yixiang Chen 001; Yujing Ma (APRES, 2015)

PSTEP - A Novel Probabilistic Event Processing Language for Uncertain Spatio-temporal Event Streams of Internet of Vehicles. - Huiyong Li; Yuanrui Zhang 001; Yixiang Chen 001 (QRS Companion, 2015)

PSTeC: A Location-Time Driven Modelling Formalism for Probabilistic Real-Time Systems. - Kangli He; Yixiang Chen 001; Min Zhang 007; Yuanrui Zhang 001 (MMB/DFT, 2016)

A Self-Adaptive Traffic Light Control System Based on Speed of Vehicles. - Jinyang Li; Yuanrui Zhang 001; Yixiang Chen 001 (QRS Companion, 2016)

A UTP Refinement Model of the STeC Language. - Yuanrui Zhang 001; Yujing Ma; Yixiang Chen 001 (QRS Companion, 2016)

Embedding CCSL into Dynamic Logic: A Logical Approach for the Verification of CCSL Specifications. - Yuanrui Zhang 001; Hengyang Wu; Yixiang Chen 001; Frédéric Mallet (FTSCS, 2018)

A Logical Approach for the Schedulability Analysis of CCSL. - Yuanrui Zhang 001; Frédéric Mallet; Huibiao Zhu; Yixiang Chen 001 (TASE, 2019)

A Process Algebra With Qualitative Calculus for Modeling Spatio-Temporal Behaviour. - Yuanrui Zhang 001; Yixiang Chen 001; Hengyang Wu (IEEE Access, 2019)

A verification framework for spatio-temporal consistency language with CCSL as a specification language. - Yuanrui Zhang 001; Frédéric Mallet; Yixiang Chen 001 (Frontiers Comput. Sci., 2020)

A survey of model-driven techniques and tools for cyber-physical systems. - Bo Liu 033; Yuanrui Zhang 001; Xuelian Cao; Yu Liu; Bin Gu; Tiexin Wang (Frontiers Inf. Technol. Electron. Eng., 2020)

A clock-based dynamic logic for schedulability analysis of CCSL specifications. - Yuanrui Zhang 001; Frédéric Mallet; Huibiao Zhu; Yixiang Chen 001; Bo Liu 033; Zhiming Liu 001 (Sci. Comput. Program., 2021)

A clock-based dynamic logic for the verification of CCSL specifications in synchronous systems. - Yuanrui Zhang 001; Hengyang Wu; Yixiang Chen 001; Frédéric Mallet (Sci. Comput. Program., 2021)

A dynamic logic for verification of synchronous models based on theorem proving. - Yuanrui Zhang 001; Frédéric Mallet; Zhiming Liu 001 (Frontiers Comput. Sci., 2022)

A dynamic logic with branching modalities. - Yuanrui Zhang 001; Zhiming Liu 001 (J. Log. Algebraic Methods Program., 2024)

Specification and Verification of Multi-Clock Systems Using a Temporal Logic with Clock Constraints. - Yuanrui Zhang 001; Frédéric Mallet; Min Zhang 002; Zhiming Liu 001 (Formal Aspects Comput., 2024)

A Generic Dynamic Logic for Program Reasoning Based on Operational Semantics. - Yuanrui Zhang 001; Zhibin Yang (SETTA, 2025)

Image reflection on process graphs of 1-free regular expressions modulo bisimilarity. - Yuanrui Zhang 001; Xinxin Liu 009 (Theor. Comput. Sci., 2026)