A Cut-Free Sequent Calculus for the Analysis of Finite-Trace Properties in Concurrent Systems
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914181670764544 |
|---|---|
| author | Fusco, Ludovico Aldini, Alessandro |
| author_facet | Fusco, Ludovico Aldini, Alessandro |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_03164 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Cut-Free Sequent Calculus for the Analysis of Finite-Trace Properties in Concurrent Systems Fusco, Ludovico Aldini, Alessandro Logic in Computer Science Logic 03B45, 03F05, 03F52, 03G10, 06A15, 06F05, 20M35, 68Q85 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. |
| title | A Cut-Free Sequent Calculus for the Analysis of Finite-Trace Properties in Concurrent Systems |
| topic | Logic in Computer Science Logic 03B45, 03F05, 03F52, 03G10, 06A15, 06F05, 20M35, 68Q85 |
| url | https://arxiv.org/abs/2512.03164 |