Monday April 03, 2023 
09:45 
Welcome 
10:00  Session 1. Systems. 
10:00 
Alexander Knapp 
Specifying Event/Databased Systems (invited talk)
Abstract: Event/databased 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 EventB with their support for parallel composition and refinement.
We then present E^{↓}logic for covering a broad range of abstraction levels of event/databased 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 EvangelouOost, 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 relationalgebraic 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 bothsided 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 twoplayer 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 firstorder 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 TwinWidth and CliqueWidth 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 wellknown 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 EXPTIMEcomplete. 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 BLalgebras generated by one finite set of BLchains with finitelymany components (contributed talk)
Abstract: BLalgebras are the algebraic semantics of Basic logic BL, the logic of all continuous tnorms and their residua. In a previous work, we provided the classification of the amalgamation property (AP) for the varieties of BLalgebras generated by one BLchain with finitelymany components. As an open problem, we left the analysis of the AP for varieties of BLalgebras generated by one finite set of BLchains with finitelymany components. In this paper we provide a partial solution to this problem. We provide a classification of the AP for the varieties of BLalgebras generated by one finite set of BLchains with finitelymany 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 FixedPoint 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 fixedpoint 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 contextfree 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é GilFérez, Peter Jipsen and Siddhartha Lodhia 
The structure of locally integral involutive pomonoids and semirings (contributed talk)
Abstract: We show that every locally integral involutive partially ordered monoid (ipomonoid) $\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 ipomonoids, 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 ipomonoids $\{\mathbf A_p : p\in D\}$, indexed on a lowerbounded joinsemilattice $(D,\vee, 1)$, along a family of monoidal homomorphisms $\Phi$ is an ipomonoid.

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 LewisSmith 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 Stonestyle 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 nondeterministic 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 nondeterminism can be introduced in a linear loop before termination becomes undecidable?'' We show that termination of loops with a purely nondeterministic 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 wellknown 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 quantaleenriched 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 FirstOrder 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 firstorder 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 Ontologybased 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 grouplike and categorylike properties. A hierarchy of subclasses is explored, with increasingly benign algebraic behavior, culminating in a direct efficient conversionbyrewriting algorithm.

12:00 
Lunch 
13:40 
Farewell 