Graphical Piecewise-Linear Algebra
Guillaume Boisseau, Robin Piedeleu

TL;DR
Graphical Piecewise-Linear Algebra is a new, fully axiomatized diagrammatic language for reasoning about piecewise-linear subsets of vector spaces, extending previous graphical algebra frameworks and enabling modeling of electronic circuits.
Contribution
It introduces the most expressive member of Graphical Algebra family, with a complete axiomatisation for piecewise-linear subsets, and demonstrates its application to electronic circuit modeling.
Findings
Complete axiomatisation achieved with a single extension
Extension is minimal to capture relevant constructs
Successfully models stateless electronic circuits
Abstract
Graphical (Linear) Algebra is a family of diagrammatic languages allowing to reason about different kinds of subsets of vector spaces compositionally. It has been used to model various application domains, from signal-flow graphs to Petri nets and electrical circuits. In this paper, we introduce to the family its most expressive member to date: Graphical Piecewise-Linear Algebra, a new language to specify piecewise-linear subsets of vector spaces. Like the previous members of the family, it comes with a complete axiomatisation, which means it can be used to reason about the corresponding semantic domain purely equationally, forgetting the set-theoretic interpretation. We show completeness using a single axiom on top of Graphical Polyhedral Algebra, and show that this extension is the smallest that can capture a variety of relevant constructs. Finally, we showcase its use by modelling…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Model-Driven Software Engineering Techniques · Logic, programming, and type systems
