English

Assume-guarantee contract algebras are dp-algebras

Logic in Computer Science 2025-09-23 v3 Rings and Algebras

Abstract

In [Incer Romeo, I. X., \textit{The Algebra of Contracts}. Ph.D. Thesis, UC Berkeley (2022)] an algebraic perspective on assume-guarantee contracts is proposed. This proposal relies on a construction involving Boolean algebras. However, the structures thus proposed lack a clearly prescribed set of basic operations, necessary if we want to see them as a class of algebras (in the sense of Universal Algebra). In this article, by prescribing a suitable set of basic operations on contracts, we manage to describe these algebras as (a generating set of members of) well-known varieties.

Keywords

Cite

@article{arxiv.2402.12514,
  title  = {Assume-guarantee contract algebras are dp-algebras},
  author = {Jose Luis Castiglioni and Rodolfo Ertola-Biraben},
  journal= {arXiv preprint arXiv:2402.12514},
  year   = {2025}
}

Comments

We've changed the category equivalent to AGC to one equivalent to three odd Sugihara monoids. This allows us to provide a direct, less overworked, and self-contained proof of the results from version 1. We've changed the title to fit the new presentation. New citations have been added