A Cut-Free Sequent Calculus for the Analysis of Finite-Trace Properties in Concurrent Systems

TL;DR

This paper introduces a new proof system, $ extsf{LMC}$, for analyzing finite-trace properties in concurrent systems using a novel algebraic framework called closure $ extit{ extbf{ extltilde}}$-monoids, enabling compositional and cut-free reasoning.

Contribution

It develops a cut-free Gentzen-style calculus for finite-trace properties based on closure $ extit{ extltilde}}$-monoids, linking algebraic structures with proof-theoretic methods.

Findings

The calculus is sound and complete for closure $ extit{ extltilde}}$-monoids.

The proof system admits cut elimination.

Provides a logical framework for finite-trace property analysis.

Abstract

We address the problem of identifying a proof-theoretic framework that enables a compositional analysis of finite-trace properties in concurrent systems, with a particular focus on those specified via prefix-closure. To this end, we investigate the interaction of a prefix-closure operator and its residual (with respect to set-theoretic inclusion) with language intersection, union, and concatenation, and introduce the variety of closure $\ell$-monoids as a minimal algebraic abstraction of finite-trace properties to be conveniently described within an analytic proof system. Closure $\ell$-monoids are division-free reducts of distributive residuated lattices equipped with a forward diamond/backward box residuated pair of unary modal operators, where the diamond is a topological closure operator satisfying $\Diamond(x \cdot y) \leq \Diamond x \cdot \Diamond y$. As a logical counterpart to these structures, we present $\mathsf{LMC}$, a Gentzen-style system based on the division-free fragment of the Distributive Full Lambek Calculus. In $\mathsf{LMC}$, structural terms are built from formulas using Belnap-style structural operators for monoid multiplication, meet, and diamond. The rules for the modalities and the structural diamond are taken from Moortgat's system $\mathsf{NL}(\Diamond)$. We show that the calculus is sound and complete with respect to the variety of closure $\ell$-monoids and that it admits cut elimination.