Operational and Algebraic Approaches to the Two-Run Relational System

Relational Hoare logic extends the applicability of modular deductive verification to encompass the verification of crucial 2-run properties. Most of the current research mainly focuses on the practical applications of relational Hoare logic. However, incorporating parallel programs into the logic may further complicate the system design, which is an aspect that most research has overlooked. Therefore, this paper updates the system, referred to as the relational system, by incorporating parallel composition. In this paper, we formalize an operational semantics (called relational operational semantics) for the system, which provides a precise understanding of the language and further explores the implications of 2-runs from the formal methods perspective. In order to investigate program equivalence, bisimulation is introduced for the relational system based on the operational semantics. Furthermore, a set of algebraic laws is studied, which includes the conditional construct and parallel composition. The correctness of these algebraic laws is proved via the defined bisimulation. This reflects that our bisimulation is a practical approach to exploring program equivalence for the system.