Formal Verification of the Correctness and Soundness of a Pomset-to-LTS Transformation Algorithm

Abstract

In this paper, we present a comprehensive proof of the correctness and soundness of our previously published algorithm for transforming partially ordered multisets (Pomsets) into labeled transition systems (LTS). Our approach rigorously ensures that the transformation algorithm preserves the behavioral semantics of the original Pomset, ensuring that the resulting LTS accurately represents the concurrent and sequential dependencies inherent in the Pomset. We employ Hoare logic to formally verify the correctness of the algorithm, proving that every valid Pomset is transformed into a corresponding LTS without loss of information. Additionally, we provide detailed proofs of soundness, showing that the algorithm produces an LTS if and only if the input is a valid Pomset. This algorithm was initially proposed as part of our new refinement proof approach, which has already been published. However, the correctness of the algorithm had not been formally proven until now. These results confirm the reliability and robustness of our transformation algorithm, making it a valuable tool for modeling and analyzing concurrent systems.

Keywords