The Coarsest Precongruences Respecting Safety and Liveness Properties
Rob van Glabbeek
TL;DR
This paper characterizes the broadest refinement preorders on labelled transition systems that are compatible with key process operators and uphold safety and liveness properties, advancing formal verification methods.
Contribution
It introduces the coarsest precongruences that respect safety and liveness properties, extending the theoretical understanding of process refinement.
Findings
Identifies the coarsest precongruences for safety properties.
Identifies the coarsest precongruences for liveness properties.
Provides a formal framework for process refinement respecting key properties.
Abstract
This paper characterises the coarsest refinement preorders on labelled transition systems that are precongruences for renaming and partially synchronous interleaving operators, and respect all safety, liveness, and conditional liveness properties, respectively.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.