A Fixpoint Semantics of Event Systems with and without Fairness Assumptions

TL;DR

This paper develops a general fixpoint semantics for event systems, applicable with or without fairness assumptions, and provides proof rules for 'leads-to' properties that are sound and complete within this framework.

Contribution

It introduces a unified fixpoint semantics for event systems that encompasses fairness considerations and establishes proof rules with proven soundness and completeness.

Findings

Derived sufficient conditions for 'leads-to' under minimal progress

Proved soundness of proof obligations without state-trace reasoning

Unified semantics applicable to different fairness assumptions

Abstract

We present a fixpoint semantics of event systems. The semantics is presented in a general framework without concerns of fairness. Soundness and completeness of rules for deriving "leads-to" properties are proved in this general framework. The general framework is instantiated to minimal progress and weak fairness assumptions and similar results are obtained. We show the power of these results by deriving sufficient conditions for "leads-to" under minimal progress proving soundness of proof obligations without reasoning over state-traces.