Since 1994, the RAMiCS conference series has been the main
venue for research on relation algebras, Kleene algebras and
similar algebraic formalisms, and their applications as
conceptual and methodological tools in computer science and
beyond.
Theoretical aspects include semigroups, residuated lattices,
semirings, Kleene algebras, relation algebras, quantales and
other algebras; their connections with program logics and
other logics; their use in the theories of automata,
concurrency, formal languages, games, networks and programming
languages; the development of algebraic, algorithmic,
category-theoretic, coalgebraic and proof-theoretic methods
for these theories; their formalisation with theorem
provers.
Applications include tools and techniques for program
correctness, specification and verification; quantitative and
qualitative models and semantics of computing systems and
processes; algorithm design, automated reasoning, network
protocol analysis, social choice, optimisation and
control.
RAMiCS 2023 will take place at the Technologiezentrum Augsburg, as a
physical conference. There are no conference fees but, due to limited
resources, participation is subject to approval by the conference organisers. Please
apply for participation by February 28, 2023, by
sending an email to roland.glueck@dlr.de.
Please use this email template.
.
To get to the
from Augsburg central station use the tramway line 3 in the direction of
"Inninger Straße/Königsbrunn" and leave at "Innovationspark/LfU". The venue is on the right in the direction of travel of the tramway.
The following hotels are close to the venue:
The venue is located a little distance outside the center of Augsburg.
However, the center is easily reachable via tramway.
Simply enter line 3 at "Innovationspark/LfU" in direction "Königsplatz" and leave there.
For the ride you can use a single ticket of price-level 2 or - if you plan to ride more often - you can buy a so-called "Streifenkarte" (strip card)
in which case you have to use two strips.
Both the single tickets and the strip cards can be purchased at vending machines at every station and have to be devaluated by stamping either inside the tramway
or at the station.
Of course, the price function is symmetric.
The last tramway from the center ("Königsplatz") departs at midnight.
Unfortunately, the web page of the
All times in CEST (UTC+2). Speakers are underlined; click on titles to see abstracts.
| Monday April 03, 2023 |
|---|
| 09:45 |
Welcome |
| 10:00 | Session 1. Systems. |
| 10:00 |
Alexander Knapp |
Specifying Event/Data-based Systems (invited talk)
Abstract: Event/data-based systems are controlled by events, their local data state may change in reaction to events.
Numerous methods and notations for specifying such reactive systems have been designed,
though with varying focus on the different development steps and their refinement relations.
We first briefly review some of such methods, like temporal/modal logic, TLA, UML state machines, symbolic transition systems, CSP, synchronous languages,
and Event-B with their support for parallel composition and refinement.
We then present E↓-logic for covering a broad range of abstraction levels of event/data-based systems from abstract requirements
to constructive specifications in a uniform foundation. E↓-logic uses diamond and box modalities over structured events adopted from dynamic logic,
for recursive process specifications it offers (control) state variables and binders from hybrid logic.
The semantic interpretation relies on event/data transition systems; specification refinement is defined by model class inclusion.
Constructive operational specifications given by state transition graphs can be characterised by a single E↓-sentence.
Also a variety of implementation constructors is available in E↓-logic to support, among others, event refinement and parallel composition.
Thus the whole development process can rely on E↓-logic and its semantics as a common basis.
|
| 11:00 |
Roland Glück |
Compatibility of Refining and Controlling Plant Automata with Bisimulation Quotients (contributed talk)
Abstract: This paper is concerned with the refinement and control of a certain class of labelled transition systems, called plant automata, via bisimulation quotients.Refinement means that arbitrary transitions may be removed whereas control allows only removing edges with the same edge label.The goal is to ensure given LTL properties in the resulting plant automaton.We give a hardness result for refinement and control and investigate, in particular, the question whether refineability and controllability can be decided by looking at bisimulation quotients.
|
| 11:30 |
Nasos Evangelou-Oost, Callum Bannister and Ian Hayes |
Contextuality in distributed systems (contributed talk)
Abstract: We present a lattice of distributed program specifications, whose ordering represents implementability/refinement.Specifications are modelled by families of subsets of relative execution traces, which encode the local orderings of state transitions, rather than their absolute timing according to a global clock.This is to overcome fundamental physical difficulties with synchronisation.The lattice of specifications is assembled and analysed with several established mathematical tools.Sets of nondegenerate cells of a simplicial set model relative traces, presheaves model the parametrisation of these traces by a topological space of variables, and information algebras reveal novel constraints on program correctness.The latter aspect brings the enterprise of program specification under the widening umbrella of contextual semantics introduced by Abramsky et al.In this model of program specifications, contextuality manifests as a failure of a consistency criterion comparable to Lamport's definition of sequential consistency.The theory of information algebras also suggests efficient local computation algorithms for the verification of this criterion.The novel constructions in this paper have been verified in the proof assistant Isabelle/HOL.
|
| 12:00 |
Lunch |
| 13:30 | Session 2. Representability. |
| 13:30 |
Wesley Fussner and Peter Jipsen |
Poset Product Representations Over Simple Residuated Lattices (short talk)
|
| 13:50 |
Rudolf Berghammer and Michael Winter |
A General Method for Representing Sets of Relations by Vectors (contributed talk)
Abstract: We present a general method for computing vector representations $\Fr$ of sets of relations. This method is used for obtaining $\Fr$ from an inclusion $\FR \subseteq \FS$, where $\FR$ and $\FS$ are relation-algebraic expressions over a relation rather than its vector representation. The core of the method is a theorem that shows how $\Fr$ can be obtained from $\FR \subseteq \FS$ in one step. As applications we consider some problems concerning kernels of relations.
|
| 14:20 |
Peter Jipsen and Jas Semrl |
Representable and diagonally representable weakening relation algebras (contributed talk)
Abstract: Weakening relations are all binary relations defined on a poset such that the partial order acts as a both-sided compositional identity. This is motivated by the weakening rule in sequent calculi and closely related to models of relevance logic. For a fixed poset the collection of weakening relations is a subreduct of the full relation algebra on the underlying set of the poset. We present a two-player game for the class of representable weakening relation algebras akin to that for the class of representable relation algebras. This enables us to define classes of abstract weakening relation algebras that approximate the quasivariety of representable weakening relation algebras. We give explicit finite axiomatisations for some of these classes. We define the class of diagonally representable weakening relation algebras and prove that it is a discriminator variety. We also provide explicit representations for several small weakening relation algebras.
|
| 14:50 |
Coffee break |
| 15:20 | Session 3. Categories |
| 15:20 |
Luigi Santocanale and Cédric de Lacroix |
Prenuclear vs. Nuclear Objects in ⋆-Autonomous Categories (short talk)
|
| 15:40 |
Jesse Sigal and Chris Heunen |
Duoidally enriched Freyd categories (contributed talk)
Abstract: Freyd categories provide a semantics for first-order effectful programming languages by capturing the two different orders of evaluation for products. We enrich Freyd categories in a duoidal category, which provides a new, third choice of parallel composition. Duoidal categories have two monoidal structures which account for the sequential and parallel compositions. The traditional setting is recovered as a full coreflective subcategory for a judicious choice of duoidal category. We give several worked examples of this uniform framework, including the parametrised state monad, basic separation semantics for resources, and interesting cases of change of enrichment.
|
| 16:10 |
Coffee break |
| 16:40 | Session 4. Counting and Enumeration. |
| 16:40 |
Ambroise Baril, Miguel Couceiro, and Victor Lagerkvist |
Recent Results on Component Twin-Width and Clique-Width with Algorithmic Applications to Counting Graph Colorings (short talk)
|
| 17:00 |
Arman Shamsgovara |
Enumerating, Cataloguing and Classifying all Quantales on up to Nine Elements (contributed talk)
Abstract: Using computer software, every quantale on up to nine elements has been enumerated up to isomorphism, catalogued and classified with respect to various properties. In order to achieve this the enumeration was branched by partitioning the search space based on various isomorphic invariants of quantales.
|
| Tuesday April 04, 2023 |
|---|
| 09:00 | Session 5. Kleene Algebra. |
| 09:00 |
Tobias Kappé |
Completeness and the Finite Model Property for Kleene Algebra, Reconsidered (contributed talk)
Abstract: Kleene Algebra (KA) is the algebra of regular expressions. Central to the study of KA is Kozen's (1994) completeness result, which says that any equivalence valid in the language model of KA follows from the axioms of KA. Also of interest is the finite model property (FMP), which says that false equivalences always have a finite counterexample. Palka (2005) showed that, for KA, the FMP is equivalent to completeness.We provide a unified and elementary proof of both properties. In contrast with earlier completeness proofs, this proof does not rely on minimality or bisimilarity techniques for deterministic automata. Instead, our approach avoids deterministic automata altogether, and uses Antimirov's derivatives and the well-known transition monoid construction.Our results are fully verified in the Coq proof assistant.
|
| 09:30 |
Igor Sedlár |
On the Complexity of *-Continuous Kleene Algebra With Domain (contributed talk)
Abstract: We prove that the equational theory of *-continuous Kleene algebra with domain is EXPTIME-complete. Our proof makes essential use of Hollenberg's equational axiomatization of program equations valid in relational test algebra.
|
| 10:00 |
Coffee break |
| 10:40 | Session 6. Algebras and Varieties. |
| 10:40 |
Stefano Aguzzoli and Matteo Bianchi |
Amalgamation property for some varieties of BL-algebras generated by one finite set of BL-chains with finitely-many components (contributed talk)
Abstract: BL-algebras are the algebraic semantics of Basic logic BL, the logic of all continuous t-norms and their residua. In a previous work, we provided the classification of the amalgamation property (AP) for the varieties of BL-algebras generated by one BL-chain with finitely-many components. As an open problem, we left the analysis of the AP for varieties of BL-algebras generated by one finite set of BL-chains with finitely-many components. In this paper we provide a partial solution to this problem. We provide a classification of the AP for the varieties of BL-algebras generated by one finite set of BL-chains with finitely-many components, which are either cancellative hoops or finite Wajsberg hoops. We also discuss the difficulties to generalize this approach to the more general case.
|
| 11:10 |
Hans Leiß |
An Algebraic Representation of the Fixed-Point Closure of *-Continuous Kleene Algebras (short talk)
|
| 11:30 |
Mark Hopkins and Hans Leiß |
Normal Forms for Elements of the *-Continuous Kleene Algebras K (x) C2' (contributed talk)
Abstract: The tensor product (K (x) C2') of the *-continuous Kleene algebra K with the polycyclic *-continuous Kleene algebra C2' of two bracket pairs contains a copy of the fixed-point closure of K: the centralizer of C2' in (K (x) C2'). We prove a representation of elements of (K (x) C2') by automata a la Kleene and refine it by normal form theorems that restrict the occurrences of brackets on paths through the automata. This is the basis for a calculus of context-free expressions.
|
| 12:00 |
Lunch |
| 13:30 | Session 7. |
| 13:30 |
Valeria Vignudelli |
Equational Theories and Distances for Computational Effects (invited talk)
Abstract: Computational effects such as nondeterminism and probabilities can be abstractly modelled in category theory as monads, and can be syntactically described in universal algebra via equational theories. Equational theories allow us to reason on the equivalence of programs with computational effects. In recent years, much work has been devoted to the development of techniques to reason not only on program equivalence, but also on program distances. The correspondence between monads and equational theories has been extended to capture such notions of distances, via the framework of quantitative equational theories. In this talk, I will present such correspondence between monads and equational theories, as well as recent results applying the framework of quantitative equational theories to computational effects and distances on them. I will show several examples of axiomatizations, including more involved cases such as the combination of nondeterminism, probabilities and termination.
|
| 14:30 |
Coffee break |
| 15:00 | Session 8. Algebraic Structures. |
| 15:00 |
José Gil-Férez, Peter Jipsen and Siddhartha Lodhia |
The structure of locally integral involutive po-monoids and semirings (contributed talk)
Abstract: We show that every locally integral involutive partially ordered monoid (ipo-monoid) $\mathbf A = (A,\le, \cdot, 1, \sim, -)$, and in particular every locally integral involutive semiring, decomposes in a unique way into a family $\{\mathbf A_p : p\in A^+\}$ of integral ipo-monoids, which we call its \emph{integral components}. In the semiring case, the integral components are semirings. Moreover, we show that there is a family of monoidal homomorphisms $\Phi = \{\varphi_{pq}\colon \mathbf A_p\to \mathbf A_q : p\leq q\}$, indexed on the positive cone $(A^+,\leq)$, so that the structure of $\mathbf A$ can be recovered as a glueing $\int_\Phi \mathbf A_p$ of its integral components along $\Phi$. Reciprocally, we give necessary and sufficient conditions so that the P\l{}onka sum of any family of integral ipo-monoids $\{\mathbf A_p : p\in D\}$, indexed on a lower-bounded join-semilattice $(D,\vee, 1)$, along a family of monoidal homomorphisms $\Phi$ is an ipo-monoid.
|
| 15:30 |
Jeremy F. Alm, David Andrews and Michael Levet |
Comer Schemes, Relation Algebras, and the Flexible Atom Conjecture (contributed talk)
Abstract: In this paper, we consider relational structures arising from Comer's finite field construction, where the cosets need not be sum free. These Comer schemes generalize the notion of a Ramsey scheme and may be of independent interest. As an application, we give the first finite representation of $34_{65}$. We complement our upper bounds with some lower bounds. Using a SAT solver, we establish that $33_{65}$ is not representable on fewer than $24$ points and $34_{65}$ is not representable on fewer than $24$ points.
|
| 16:00 |
Andrew Lewis-Smith and Jas Semrl |
Implication Algebras and Implication Semigroups of Binary Relations (contributed talk)
Abstract: Implication algebras are known to be axiomatised by a finite number of equations (making the representation and finite representation problems decidable in that case). We show that this also holds in the context of unary (and binary) relations and present a Stone-style representation theorem. We then show that the (finite) representation decision problem is undecidable for implication semigroups, in stark contrast with implication algebras.
|
| 16:30 |
Break |
| 17:30 |
Social event |
Guided tour through Augsburg, meeting point at town hall Augsburg
|
| 19:00 |
Dinner |
Dinner at Wirtshaus am Dom (location)
|
| Wednesday April 05, 2023 |
|---|
| 09:10 | Session 9. Models and Programs. |
| 09:10 |
Laura Kovács and Anton Varonka |
What Else is Undecidable about Loops? (contributed talk)
Abstract: We address algebraic aspects of invariant generation and proving termination, two central questions of program analysis, for non-deterministic loops with polynomial updates. Our focus is sketching the boundary of (un-)decidability for both problems between different classes of programs. The first main contribution of this work is related to the question raised by Braverman in 2006: ``How much non-determinism can be introduced in a linear loop before termination becomes undecidable?'' We show that termination of loops with a purely non-deterministic choice between linear updates is undecidable in the presence of linear inequality loop conditions. In the context of invariants, an algorithm is known that computes all polynomial relations among variables of loops with multiple linear updates. At the same time, allowing polynomial assignments of higher degrees was shown to result in algorithmic unsolvability. We highlight that negative results in fact do not exploit general polynomial updates. We show that no algorithm can find all polynomial relations for programs as soon as quadratic updates or updates guarded by affine equalities are involved.
|
| 09:40 |
Yannick Chevalier |
Model Synthesis based on Experience (short talk)
|
| 10:00 |
Martin E. Bidlingmaier |
Datalog with Equality: Semantics and Evaluation (short talk)
|
| 10:20 |
Coffee break |
| 11:00 | Session 10. |
| 11:00 |
John Stell |
Algebra and Logic in Granularity (invited talk)
Abstract: Conceptually, a relation on a set can be understood as a lens through which subsets are seen in different ways. For example, at different levels of detail. This idea underlies some basic operations in mathematical morphology as used in image processing. In a more abstract setting, the idea also fits one view of quantale modules, where a quantale acting on a complete lattice models the operation of observing elements of the lattice by means of the elements of quantale. This talk will consider the role of relations, and their generalizations, in the development of a theory of granularity, or level of detail. Starting from basic mathematical morphology, algebraic and logical structures motivated by extensions of this will be discussed. To explain the starting point, mathematical morphology is a body of techniques used in image processing since the 1960s. The algebraic basis of these techniques is already well-known through the work of Serra, Heijmans, Ronse, and others. A black and white image can be seen as a subset of a set of pixels. Operations mapping subsets to subsets provide ways of modifying images. Such operations arise from relations on the underlying set. Algebraically, a binary relation induces an adjunction yielding the dilation (left, or lower, adjoint) and erosion (right, or upper, adjoint) operations used in image processing. From these are derived openings and closings. Families of openings and closings are used to build ''alternating sequential filters'', ''granulometries'' and further practically useful operations. Mathematical morphology was extended from sets of pixels to graphs and subgraphs. The appropriate notion of relation to deal with this was identified, and these can be seen as quantale-enriched distributors. A quite separate application of quantales to mathematical morphology was developed by Russo. The talk will discuss connections between these accounts.
|
| 12:00 |
Lunch |
| 13:50 |
Business meeting |
| 15:50 |
Coffee break |
| 16:30 |
Interdisciplinary event |
Guided tour through the facilities of the
Center for Leightweight Production Technology, with discussions
|
| Thursday April 06, 2023 |
|---|
| 09:10 | Session 11. Relation Algebra. |
| 09:10 |
Anthony Brogni and Sebastiaan J. C. Joosten |
Translating First-Order Predicate Logic to Relation Algebra, an Implementation (short talk)
|
| 09:30 |
Walter Guttmann |
Dependences between Domain Constructions in Heterogeneous Relation Algebras (contributed talk)
Abstract: We show the following dependences between relational domain constructions in the framework of heterogeneous relation algebras. If all power sets and subsets exist and objects are comparable, then all sums exist. If all sums exist and atoms are rectangular, then all products exist. If all atoms are rectangular, then all subsets exist if and only if all quotients exist. We give models with rectangular atoms which rule out further dependences between these constructions.
|
| 10:00 |
Michael Winter |
Relational Algebraic Approach to the Real Numbers - The Additive Group (contributed talk)
Abstract: In this paper we start the investigation of an object representing the real numbers in categories of relations. Our axiomatization uses the construction of a relation power, i.e., an abstract version of power sets within the category. This allows us to utilize a relation algebraic version of Tarski's axioms of the real numbers as a first-order definition of a real number object. The current paper focuses on the addition operation of the real number object. It is shown that addition forms a densely and linearly ordered abelian group.
|
| 10:30 |
Coffee break |
| 11:10 | Session 12. Relations and Reality. |
| 11:10 |
Roland Glück and Florian Krebs |
Toward Ontology-based Production - Relations building Airplanes (short talk)
|
| 11:30 |
Baltasar Trancón Y Widemann and Markus Lepper |
Towards a Theory of Conversion Relations for Prefixed Units of Measure (contributed talk)
Abstract: Units of measure with prefixes and conversion rules are given a formal semantic model in terms of categorial group theory. Basic structures and both natural and contingent semantic operations are defined. Conversion rules are represented as a class of ternary relations with both group-like and category-like properties. A hierarchy of subclasses is explored, with increasingly benign algebraic behavior, culminating in a direct efficient conversion-by-rewriting algorithm.
|
| 12:00 |
Lunch |
| 13:40 |
Farewell |
All papers will be peer-reviewed by at least three
referees. The proceedings will be published in an LNCS volume
by Springer, ready at the conference. Submissions must not be
published or under review for publication
elsewhere. Submissions must be in English using a PDF not
exceeding 16 pages in LNCS style.
Submissions must provide sufficient information to judge
their merits. Additional material may be provided in a clearly
marked appendix or by a reference to a manuscript on a web
site. Experimental data, software or mathematical components
for theorem provers must be available in sufficient detail for
referees. Deviation from these requirements may lead to
rejection.
One author of each accepted paper is expected to present the
paper at the conference. Accepted papers must be produced with
LaTeX. Formatting instructions and LNCS style files are
available
at http://www.springer.de/comp/lncs/authors.html.
As for earlier RAMiCS conferences, we intend to publish a
journal special issue with revised and extended versions of a
selection of the best papers.
