5 papers
Labelled Process Logic
Yuanrui Zhang
This paper develops a cyclic labelled proof-theoretic framework for process logic -- an extension of dynamic logic in which formulas specify properties of execution traces rather t…
On A Parameterized Theory of Dynamic Logic for Operationally-based Programs
Yuanrui Zhang
Applying dynamic logics to program verifications is a challenge, because their axiomatic rules for regular expressions can be difficult to be adapted to different program models. W…
Parameterized Dynamic Logic -- Towards A Cyclic Logical Framework for General Program Specification and Verification
Yuanrui Zhang
We present a theory of parameterized dynamic logic, namely DLp, for specifying and reasoning about a rich set of program models based on their transitional behaviours. Different fr…
Image Reflection on Process Graphs -- A Novel Approach for the Completeness of an Axiomatization of 1-Free Regular Expressions Modulo Bisimilarity
Yuanrui Zhang, Xinxin Liu
We analyze a phenomenon called ``image reflection'' on a type of characterization graphs -- LLEE charts -- of 1-free regular expressions. Due to the correspondence between 1-free r…
A Dynamic Logic for Verification of Synchronous Models based on Theorem Proving
Yuanrui Zhang
Synchronous model is a type of formal models for modelling and specifying reactive systems. It has a great advantage over other real-time models that its modelling paradigm support…