A Fixpoint Semantics of Event Systems with and without Fairness Assumptions
Logic in Computer Science
2007-05-23 v1
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.
Keywords
Cite
@article{arxiv.cs/0512082,
title = {A Fixpoint Semantics of Event Systems with and without Fairness Assumptions},
author = {Hector Ruiz Barradas and Didier Bert},
journal= {arXiv preprint arXiv:cs/0512082},
year = {2007}
}