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.
All times in CET; click on time to convert to other time zones.
Speakers are underlined, click on titles to see abstracts.
The program is also available as a
| Monday November 1, 2021 |
|---|
| 19:30 | Dinner |
| Tuesday November 2, 2021 |
|---|
| 7:00 | Breakfast |
| 8:50 | Opening |
| 9:00 |
|
Session 1. Chair Roland Glück |
| 9:00 |
Christophe Lucas and Matteo Mio |
Free Modal Riesz Spaces are Archimedean: a Syntactic Proof
We prove, using syntactical proof–theoretic methods, that free modal Riesz spaces are Archimedean. Modal Riesz spaces are Riesz spaces (real vector lattices) endowed with a positive linear 1–decreasing operator, and have found application in the development of probabilistic temporal logics in the field of formal verification. All our results have been formalised using the Coq proof assistant.
|
Slides |
| 9:30 |
Wesley Fussner and William Zuluaga Botero |
Some modal and temporal translations of generalized basic logic
We introduce a family of modal expansions of Łukasiewicz logic that are designed to accommodate modal translations of generalized basic logic (as formulated with exchange, weakening, and falsum). We further exhibit algebraic semantics for each logic in this family, in particular showing that all of them are algebraizable in the sense of Blok and Pigozzi. Using this algebraization result, we establish that each of the introduced modal Łukasiewicz logics has a local deduction detachment theorem. By applying Jipsen and Montagna's poset product construction, we give two translations of generalized basic logic with exchange, weakening, and falsum in the style of the celebrated Gödel-McKinsey-Tarski translation. The first of these interprets generalized basic logic in a modal Łukasiewicz logic in the spirit of classical S4, whereas the second interprets generalized basic logic in a temporal variant of the latter.
|
Slides |
| 10:00 |
Willem Conradie, Valentin Goranko and Peter Jipsen |
Algorithmic correspondence for relevance logics, bunched implication logics, and relation algebras via an implementation of the algorithm PEARL
The theory and methods of algorithmic correspondence theory for modal logics, developed over the past 20 years, have recently been extended to the language RL of relevance logics with respect to their standard Routley-Meyer relational semantics. As a result, the non-deterministic algorithmic procedure PEARL (acronym for 'Propositional variables Elimination Algorithm for Relevance Logic') has been developed for computing first-order equivalents of formulae of the language RL in terms of that semantics. PEARL is an adaptation of the previously developed algorithmic procedures SQEMA (for normal modal logics) and ALBA (for distributive and non-distributive modal logics). It succeeds on all inductive formulae in the language RL, in particular on all previously studied classes of Sahlqvist formulae for relevance logic. In the present work, we re-interpret the algorithm PEARL from an algebraic perspective with its rewrite rules seen as manipulating quasi-inequalities interpreted over Urquhart's relevant algebras. This enables us to complete the part of the Sahlqvist theorem still outstanding from the previous work, namely the fact that all inductive RL formulas are canonical, i.e., are preserved under canonical extensions of relevant algebras. Via the discrete duality between perfect relevant algebras and Routley-Meyer frames, this establishes the fact that all inductive RL formulas axiomatise logics which are complete with respect to first-order definable classes of Routley-Meyer frames. This generalizes the "canonicity via correspondence" result in [Urquhart, 1996] for (what we can now recognise as) a certain special subclass of Sahlqvist formulas in the "groupoid" sublanguage of RL where fusion is the only connective. By extending RL with a unary connective for converse and adding the necessary axioms, our results can also be applied to bunched implication algebras and relation algebras. We then present an optimised and deterministic version of PEARL, which we have recently implemented in Python and applied to verify the first-order equivalents of a number of important axioms for relevance logics known from the literature, as well as on several new types of formulae. In the paper, we report on the implementation and on some testing results.
|
Slides |
| 10:30 | Coffee break |
| 11:00 |
|
Session 2. Chair Sam van Gool |
| 11:00 |
Frank Valencia, Sergio Ramírez, Santiago Quintero and Carlos Pinzón |
Computing Aggregated Knowledge as the Greatest Lower Bound of Knowledge
In economics and multi-agent systems, aggregated (or distributed) knowledge of a group is the knowledge of someone who knows exactly what every member of the group knows. This notion can be used to analyse the implications of the knowledge of a community if they were to combine their knowledge. In this paper we use fundamental tools from the theory of distributive lattice to characterize and compute aggregate knowledge.We prove that for distributive lattices of size $n$, (1) the meet of join-endomorphisms can be computed in time $O(n)$. Previous upper bound was $O(n^2)$. We show that (2) aggregated knowledge of given group can be viewed as the meet of the knowledge of each member of the group. We also show that for state sets of size $n$, (3) aggregated knowledge can be computed in time $O(n^2)$ in the general case and (4) for $S5$ knowledge (or Aumman structures), it can be computed in time $O(n\alpha(n))$ where $\alpha(n)$ is the inverse of the Ackermann function.
|
Slides |
| 11:30 |
Cameron Calk, Uli Fahrenberg, Christian Johansen, Georg Struth and Krzysztof Ziemiański |
lr-Multisemigroups, Modal Quantales and the Origin of Locality
We introduce lr-multisemigroups as duals of modal quantales and study correspondences between equations in these multisemigroups and the domain and codomain axioms of modal quantales. Our results yield construction principles for modal powerset quantales that cover a wide range of models and applications.
|
Slides |
| 12:00 |
Jérémie Marquès |
Polyadic spaces and profinite monoids
Hyperdoctrines are an algebraization of first-order logic introduced by Lawvere. Joyal proposed to apply pointwise Stone duality to get what he called a polyadic space. He also proposed the idea of Stirling kernels of a polyadic space that we generalize here in order to adapt the notion of polyadic space to certain special classes of first-order theories. We will see how these ideas can be applied to establish a correspondence between equidivisible profinite semigroups with open multiplication and some first-order theories with a linear order symbol.
|
Slides |
| 12:30 | Lunch |
| 14:00 |
|
Session 3. Chair Silvio Ghilardi |
| 14:00 |
Dmitriy Zhuk |
Quantified Constraint Satisfaction Problem: towards the classification of complexity (invited talk)
The Quantified Constraint Satisfaction Problem (QCSP) is
the generalization of the Constraint Satisfaction problem (CSP) where
we are allowed to use
both existential and universal quantifiers.
Formally, the QCSP over a constraint language $\Gamma$ is
the problem
to evaluate
a sentence of the form $$\forall x_1 \exists y_1\forall x_2 \exists y_2 \dots \forall x_n \exists y_n \ (R_{1}(\dots)\wedge\dots
\wedge R_{s}(\dots)),$$
where $R_1,\dots,R_s$ are relations from $\Gamma$.
While CSP remains in NP for any $\Gamma$, QCSP$(\Gamma)$ can be PSpace-hard, as witnessed by Quantified 3-Satisfiability or Quantified Graph 3-Colouring.
For many years there was a hope that
for any constraint language the QCSP is either in P,
NP-complete, or PSpace-complete. Moreover,
a very simple conjecture describing the complexity
of the QCSP was suggested by Hubie Chen.
However,
in 2018 together with Mirek Ol\u{s}\'ak and Barnaby Martin
we discovered constraint languages
for which the QCSP is coNP-complete, DP-complete,
and even $\Theta_{2}^{P}$-complete, which refutes
the Chen conjecture.
Despite the fact that we described the complexity for
each constraint language on a 3-element domain with constants,
we did not hope to obtain a complete classification.
This year I obtained several results
that make me believe that
such a classification is closer than it seems.
First, I obtained an elementary proof of the
PGP reduction, which allows to reduce the QCSP to the CSP.
Second, I showed that there is a gap between
$\Pi_{2}^{P}$ and PSpace, and found a criterion for the
QCSP to be PSpace-hard.
In the talk I will discuss the above and some other results.
|
Slides |
| 15:00 |
Natanael Alpay, Peter Jipsen and Melissa Sugimoto |
Unary-determined distributive l-magmas and bunched implication algebras
A distributive lattice-ordered magma ($d\ell$-magma) $(A,\wedge,\vee,\cdot)$ is a distributive lattice with a binary operation $\cdot$ that preserves joins in both arguments, and when $\cdot$ is associative then $(A,\vee,\cdot)$ is an idempotent semiring. A $d\ell$-magma with a top $\top$ is unary-determined if $x\cdot y=(x\top\wedge y)\vee(x\wedge \top y)$. These algebras are term-equivalent to a subvariety of distributive lattices with $\top$ and two join-preserving unary operations $p,q$. We obtain simple conditions on $p,q$ such that $x\cdot y=(px\wedge y)\vee(x\wedge qy)$ is associative, commutative, idempotent and/or has an identity element. This generalizes previous results on the structure of doubly idempotent semirings and, in the case when the distributive lattice is a Heyting algebra, it provides structural insight into unary-determined algebraic models of bunched implication logic. We also provide Kripke semantics for the algebras under consideration, which leads to more efficient algorithms for constructing finite models.
|
Slides |
| 15:30 | Coffee break |
| 16:00 |
|
Session 4. Chair Uli Fahrenberg |
| 16:00 |
Wolfgang Poiger |
Many-valued modal logic over a semi-primal algebra (short talk)
Since semi-primal algebras behave similarly to the two-element Boolean algebra, it makes sense to consider many-valued logic over a semi-primal algebra of truth values. Our interest lies in modal extensions of such logics. Through their respective dual categories we explore the relationship between the variety HSP(L) generated by a semi-primal algebra L and the variety BA of Boolean algebras. As an example, we utilize this relationship to prove a many-valued analogue of the Goldblatt-Thomason Theorem. Furthermore, we discuss the underlying coalgebraic picture and discuss how one may lift results from the classical case to the many-valued case.
|
Slides |
| 16:20 |
Stefano Aguzzoli and Matteo Bianchi |
Amalgamation property for varieties of BL-algebras generated by one chain with finitely many components
BL-algebras are the algebraic semantics for Hajek's Basic Logic BL, the logic of all continuous t-norms and their residua. In this paper we study the amalgamation property for the varieties of BL-algebras generated by one BL-chain with finitely many components.
|
Slides |
| 16:50 |
Claudia Muresan |
Subreducts and Subvarieties of PBZ*–lattices (short talk)
PBZ∗–lattices are the paraorthomodular Brouwer–Zadeh lattices whose pairs of elements with their Kleene complements satisfy the Strong De Morgan condition; more precisely, they are bounded lattices endowed with two unary operations:
• an involution ·′, called Kleene complement, which satisfies the Kleene condition: x ∧ x′ ≤ y ∨ y′, as well as paraorthomodularity ((x ≤ y & x′ ∧ y ≈ 0) → x ≈ y, which becomes an equational condition under the other axioms of PBZ∗–lattices) – so the bounded involution lattice reduct of any PBZ∗–lattice is a paraorthomodular pseudo–Kleene algebra, but it turns out that not all paraorthomodular pseudo–Kleene algebras are reducts of PBZ∗–lattices,
• and the Brouwer complement, which reverses order, is smaller than the Kleene complement, which it only equals on the sharp elements (i.e. the elements having their Kleene complement as a bounded lattice complement), and satisfies only one of the De Morgan laws, along with condition (∗), which is obtained from the other De Morgan law (called Strong De Morgan) by replacing one of the variables with the Kleene complement of the other.
These algebras arise in the study of Quantum Logics and they include orthomodular lattices with an
extended signature (with the two complements coinciding), as well as antiortholattices (whose Brouwer
complements are trivial). From the other abstractions of the sets of quantum events within the unsharp
approach to quantum theory, PBZ∗–lattices present the advantage of forming a variety, that we denote ∗
by PBZL .
Antiortholattices turn out to have directly irreducible lattice reducts and, under distributivity, no
nontrivial elements with bounded lattice complements.
We establish a lattice isomorphism between the lattice of subvarieties of the variety SAOL generated
by the antiortholattices with the Strong De Morgan property and the ordinal sum of the three–element chain with the lattice of subvarieties of the variety PKA of pseudo–Kleene algebras, which also gives us axiomatizations for all subvarieties of SAOL from those of the subvarieties of PKA.
The form of this lattice isomorphism proves that the variety PKA is generated by the class of the bounded involution lattice reducts of the members of SAOL, thus also by the quasivariety of paraortho- modular pseudo–Kleene algebras and by the class of the bounded involution lattice reducts of the members of PBZL∗, which also shows that neither of these classes is a variety.
We obtain an infinite ascending chain of varieties of distributive PBZ∗–lattices, which, along with the well–known infinite ascending chain of varieties of modular ortholattices and its image through the lattice isomorphism mentioned above, give us an infinity of pairwise disjoint infinite ascending chains of varieties of PBZ∗–lattices.
|
Slides |
| 17:10 |
Khyodeno Mozhui and K. V. Krishna |
On the Representation Number of Bipartite Graphs (short talk)
A word-representable graph is a simple graph G which can be represented by a word w over the vertices of G such that any two vertices are adjacent in G if and only if they alternate in w. It is known that the class of comparability graphs – the graphs which admit a transi- tive orientation – is precisely the class of graphs that can be represented by a concatenation of permutations of vertices. The class of bipartite graphs is a subclass of comparability graphs. While it is an open prob- lem to determine the representation number of comparability graphs, it was conjectured that the representation number of bipartite graphs on n vertices is at most n/4. In this paper, we propose a polynomial time relabeling algorithm to produce a word representing a given bipartite graph which is a concatenation of permutations of the graph’s vertices. Thus we obtain an upper bound for the representation number of bipar- tite graphs, which in turn gives us an upper bound for the dimension of the posets corresponding to bipartite graphs.
|
Slides |
| 19:30 | Dinner |
| Wednesday November 3, 2021 |
|---|
| 7:00 | Breakfast |
| 9:00 |
|
Session 5. Chair Peter Jipsen |
| 9:00 |
Callum Bannister, Peter Höfner and Georg Struth |
Effect Algebras, Girard Quantales and Complementation in Separation Logic
We study convolution and residual operations within convolution quantales of maps from partial abelian semigroups and effect algebras into value quantales, thus generalising separating conjunction and implication of separation logic to quantitative settings. We show that effect algebras lift to Girard convolution quantales, but not the standard partial abelian monoids used in separation logic. This shows that the standard assertion quantales of separation logic do not admit a linear negation relating convolution and its right adjoint. We consider alternative dualities for these operations on convolution quantales using boolean negations, some old, some new, relate them with properties of the underlying partial abelian semigroups and outline potential uses.
|
Slides |
| 9:30 |
Luigi Santocanale |
Skew metrics valued in Sugihara semigroups
We consider skew metrics (equivalently, transitive relations that are tournaments, linear orderings) valued in Sugihara semigroups on autodual chains. We prove that, for odd chains and chains without a unit, skew metrics classify certain tree-like structures that we call perfect augmented plane towers. When the chain is finite and has cardinality $2K+1$, skew metrics on a set $X$ give rise to plane rooted trees of height $K$ whose frontier is a linear preorder of $X$.Any linear ordering on $X$ gives rise to an ordering on the set of its skew metrics valued on an arbitrary involutive residuated lattice $Q$. If $Q$ satisfies the mix rule, then this poset is most often a lattice. We study this lattice for $X = \{1,\ldots ,n\}$ and $Q$ the Sugihara monoid on the chain of cardinality $2K+1$. We give a combinatorial model of this lattice by describing its covers as moves on a appropriate space of words coding perfect augmented plane trees. Using the combinatorial model, we develop enumerative considerations on this lattice.
|
Slides |
| 10:00 |
George Metcalfe, Sam van Gool, Adrien Guatto and Simon Santschi |
Time Warps, from Algebra to Algorithms
Graded modalities have been proposed in recent work on programming languages as a general framework for refining type systems with intensional properties. In particular, continuous endomaps of the discrete time scale, or time warps, can be used to quantify the growth of information in the course of program execution. Time warps form a complete residuated lattice, with the residuals playing an important role in potential programming applications. In this paper, we study the algebraic structure of time warps, and prove that their equational theory is decidable, a necessary condition for their use in real-world compilers. We also describe how our universal-algebraic proof technique lends itself to a constraint-based implementation, establishing a new link between universal algebra and verification technology.
|
Slides |
| 10:30 | Coffee break |
| 11:00 |
|
Session 6. Chair Stepan Kuznetsov |
| 11:00 |
Roland Glück |
Isolated Sublattices and their Application to Counting Closure Operators
This paper is dedicated to the investigation of the interplay between isolated sublattices and closure operators.Isolated sublattices are a special kind of sublattices which can serve to diminuish the number of elements of a lattice by means of a quotient lattice.At the same time, there are simple formulae for the relationship between the number of closure operators in the original lattice and its quotient.This connection can be used to derive an algorithm for counting closure operators, provided the lattice contains suitable isolated sublattices.
|
Slides |
| 11:30 |
Chad Nester |
A Variety Theorem for Relational Universal Algebra
We consider an analogue of universal algebra in which generating symbols are interpreted as relations. We prove a variety theorem for these relational algebraic theories, in which we find that their categories of models are precisely the definable categories. The syntax of our relational algebraic theories is string-diagrammatic, and can be seen as an extension of the usual term syntax for algebraic theories.
|
Slides |
| 12:00 |
Cameron Calk, Philippe Malbos and Eric Goubault |
Abstract Strategies and Coherence
Normalisation strategies give a categorical interpretation of the notion of contracting homotopies via confluent and terminating rewriting. This approach relates standardisation to coherence results in the context of higher dimensional rewriting systems. On the other hand, globular 2-Kleene algebras provide a formal setting for reasoning about coherence proofs in abstract rewriting systems. In this work, we formalise the notion of normalisation strategy in this setting. In such structures, normalisation strategies allow us to prove a formal coherence theorem via convergent abstract rewriting.
|
Slides |
| 12:30 | Lunch |
| 13:30 | Business meeting |
| 14:30 |
|
Session 7. Chair Georg Struth |
| 14:30 |
Marcelo Frias |
Relational Tight Field Bounds for Distributed Analysis of Programs (invited talk)
Relational tight field bounds are an abstraction of the
semantics of data structures. In the presence of appropriate
symmetry-breaking predicates, these bounds can be computed
automatically and allow to dramatically speed up bug-finding using
SAT-solving. In this lecture, after giving an introduction to tight
field bounds and symmetry-breaking predicates, I will present a
general technique for distributing program analyses. As examples, I
will show how the technique allows one to distribute SAT-based
bug-finding as well as symbolic execution over
complex data types.
|
Slides |
| 15:30 | Coffee break |
| 16:00 |
|
Session 8. Chair Rudolf Berghammer |
| 16:00 |
Michael Winter |
Change of Base using Arrow Categories
Arrow categories establish a suitable framework to reason about L-fuzzy relation abstractly. For each arrow category we can identify the Heyting algebra L that is used as the lattice of membership or truth values by the relations of the category. Therefore, arrow categories model the fixed-base approach to L-fuzziness, i.e., all relations of the given arrow category use the same membership values. In this paper we are interested in the process of changing the base, i.e., an operation that allows to switch from an L1-fuzzy relation to an L2-fuzzy relation by replacing all membership values from L1 by values from L2 . We will define and investigate this change of base between two abstract arrow categories for which component-wise reasoning cannot be performed.
|
Slides |
| 16:30 |
George Addison, Sajal Saha, and Michael Winter |
L-fuzzy Concept Analysis using Arrow Categories (short talk)
The purpose of this paper is to investigate topics in fuzzy concept analysis using the theory of arrow categories. Our approach deals with the origi- nal, fuzzy data using fuzzy subsets in order to obtain a notion of fuzzy concepts, fuzzy concept lattices, and fuzzy association rules. Our approach is general in the sense that we only require a complete Heyting algebra as the lattice of truth values instead of the unit interval r0, 1s or a substructure thereof. In addition, our approach differs from most approaches in the literature, which usually first apply some kind of defuzzyfication, e.g., α-cuts, and then apply concept analysis in the classical (crisp) sense.
|
Slides |
| 16:50 |
Alexandre Fernandez, Luidnel Maignan and Antoine Spicher |
Accretive Computation of Global Transformations
Global transformations form a categorical framework adapting graph transformations to describe fully synchronous rule systems on a given data structure. In this work we focus on data structures that can be captured as presheaves (like sets, graphs or Petri nets) and study the computational aspects of such synchronous rule systems. To obtain an online algorithm, a complete study of the sub-steps within each synchronous step is done at the semantic level. This leads to the definition of accretive rule systems and a local criterion to characterize these systems. Finally an online computation algorithm for theses systems is given.
|
Slides |
| 17:20 |
Ralph Sarkis |
Quotienting a Monad via Projective Algebras (short talk)
Quotient types are quite common in mathematics but they are rather difficult to implement in a programming language. For instance, one can easily define the type of pairs of integers $\mathsf{Int}\times \mathsf{Int}$, but in order to define the type of rational numbers, one needs to quotient $\mathsf{Int}\times \mathsf{Int}$ by the relation $(p,q) \sim (r,s) \Leftrightarrow ps = rq$, which is easier said than done. In the framework of monadic programming, datatypes are free algebras for a monad. Not all algebras for a monad are free, but they are all quotients of free algebras. An algebra for a monad is said to be projective if it is both a quotient and a subalgebra of a free algebra. We show that a natural family of projective algebras can be seen as algebras for a quotient monad. In other words, when a quotienting operation is nice enough that 1) the resulting algebra is a subalgebra of the free algebra and 2) it satisfies some naturality condition, then we obtain a monad that models the quotient type.
|
On board! |
| 17:40 |
Cédric de Lacroix |
Generalizing Girard quantale in a symmetric closed monoidal category (short talk)
The category of complete lattices and join-preserving maps is known to be star-autonomous and the semigroup of this category are called quan- tales. A Frobenius quantale is usually defined as a quantale with a du- alizing element. If this element is also cyclic, the quantale is called a Girard quantale and it can interpret the non-commutative linear logic. Two properties have motivated this work. First, the canonical quantale of endomorphism of a complete lattice is a Girard quantale if and only if this lattice is completely distributive. Secondly, completely distributive lattices have a categorical characterization: they are exactly the nuclear objects – i.e the mix arrow is an isomorphism – of the category of sup lattices. The aim of this work was to find out the kind of semigroup (we simply called them Girard semigroup) that generalize Girard quantale. With the right definition in hand we wanted to verify if the following con- jecture is satisfied: given a symetric closed monoidal category, the internal hom of an object with itself is a Girard semigroup if and only if this object is a nuclear object of the category – that is if the generalization of the above property is still true. We used a - slightly - more general definition of Frobenius and Girard quantales which led to a suitable definition of Frobenius and Girard semigroups in any symetric closed category. In this work we found several properties of these new structures and we proved that if an object is nuclear then the internal hom of this object with it- self has a structure of Girard semigroup. The converse implication of the conjecture is still to be proved.
|
Slides |
| 19:30 | Dinner |
| Thursday November 4, 2021 |
|---|
| 7:00 | Breakfast |
| 9:00 |
|
Session 9. Chair Barbara König |
| 9:00 |
Bernhard Möller, Peter O'Hearn and Tony Hoare |
On Algebra of Program Correctness and Incorrectness
Variations on the notion of Kleene algebra have been used to provide foundations of reasoning about programs, for instance by showing how Hoare Logic (HL) can be represented in algebra. This line of work has focussed on program correctness,i.e., proving the absence of bugs. Recently, Incorrectness Logic (IL) has been advanced as a reasoning formalism for the dual problem: proving the presence of bugs. IL is intended to underpin the use of logic in program testing and static bug finding. In this paper we describe an extension of Kleene algebra, an algebra with backwards diamond operators and countable joins for tests, which embeds IL, and which also is complete for reasoning about the image of the embedding. In addition to embedding IL, the algebra retains the ability to embed HL, and to make connections between IL and HL specifications: In this sense, it unifies correctness and incorrectness reasoning in one formalism.
|
Slides |
| 9:30 |
Walter Guttmann |
Second-Order Properties of Undirected Graphs
We study second-order formalisations of graph properties expressed as first-order formulas in relation algebras extended with a Kleene star. The formulas quantify over relations while still avoiding quantification over elements of the base set. We formalise the property of undirected graphs being acyclic this way. This involves a study of various kinds of orientation of graphs. We also verify basic algorithms to constructively prove several second-order properties.
|
Slides |
| 10:00 |
Walter Guttmann and Nicolas Robinson-O'Brien |
Relation-algebraic Verification of Borůvka's Minimum Spanning Tree Algorithm
Previous work introduced a relation-algebraic framework for reasoning about weighted-graph algorithms. We use this framework to prove partial correctness of Borůvka's minimum spanning tree algorithm. This is the first formal proof of correctness for this algorithm. We also discuss new abstractions that make it easier to reason about weighted graphs.
|
Slides |
| 10:30 | Coffee break |
| 11:00 |
|
Session 10. Chair Bernhard Möller |
| 11:00 |
Rudolf Berghammer and Mitja Kulczynski |
Experimental Investigation of Sufficient Criteria for Relations to Have Kernels
We investigate four well-known criteria for the existence of kernels in directed graphs/relations which efficiently can be tested, namely to be irreflexive and symmetric, to be progressively finite, to be bipartite, and to satisfy Richardson's criterion. The numerical data, obtained by the evaluation of relation-algebraic problem specifications by means of RelView, show that even the most general of them is very far away from a characterisation of the class of directed graphs having kernels.
|
Slides |
| 11:30 |
Rudolf Berghammer |
Relational Computation of Sets of Relations
We present a technique for the relational computation of sets RR of relations. It is based on a specification of a relation R to belong to RR by means of an inclusion $s \subseteq t$, where s and t are relation-algebraic expressions constructed from a vector model of R in a specific way. To get the inclusion, we apply properties of a mapping that transforms relations into their vectors models and, if necessary, point-wise reasoning. The desired computation of RR via a relation-algebraic expression r is then immediately obtained from the inclusion using a result published in the proceedings of MPC 2015. Compared with a direct development of r from a logical specification of R to belong to RR, the proposed technique is much more simple. We demonstrate its use by some classes of specific relations and also show some applications.
|
Slides |
| 12:00 |
Kangfeng Ye, Simon Foster and Jim Woodcock |
Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving
Semantics for nondeterministic probabilistic sequential programs is well studied in the past decades. In a variety of semantic models, how nondeterministic choice interacts with probabilistic choice is the most significant difference. In He, Morgan, and McIver’s relational model, probabilistic choice refines nondeterministic choice. This model is general because of its predicative-style semantics in Hoare and He’s Unifying Theories of Programming, and suitable for automated reasoning because of its algebraic feature. Previously, we gave probabilistic semantics to the RoboChart notation based on this model, and also formalised its proof, and revealed interesting details. In this paper, we present our mechanisation of the proof in Isabelle/UTP, an Isabelle/HOL based proof framework for UTP, enabling automated reasoning for probabilistic sequential programs including a subset of the RoboChart language. With mechanisation, we even reveal more interesting questions, hidden in the original model. We demonstrate several examples, including an example to illustrate the interaction between nondeterministic choice and probabilistic choice, and a RoboChart model for randomisation based on binary probabilistic choice.
|
Slides |
| 12:30 | Lunch |
| 14:00 | Free afternoon |
| 19:30 | Dinner |
| Friday November 5, 2021 |
|---|
| 7:00 | Breakfast |
| 9:00 |
|
Session 11. Chair Wesley Fussner |
| 9:00 |
Agi Kurucz, Vladislav Ryzhikov, Yury Savateev and Michael Zakharyaschev |
Deciding FO-definability of Regular Languages
We prove that, similarly to known PSpace-completeness of recognising FO(<)-definability of the language L(A) of a DFA A, deciding both FO(<,C)- and FO(<,MOD)-definability (corresponding to circuit complexity in AC0 and ACC0) are PSpace-complete. We obtain these results by first showing that known algebraic characterisations of FO-definability of L(A) can be captured by `localisable' properties of the transition monoid of A. Using our criterion, we then generalise the known proof of PSpace-hardness of FO(<)-definability, and establish the upper bounds not only for arbitrary DFAs but also for 2NFAs.
|
Slides |
| 9:30 |
Damien Pous, Jurriaan Rot and Jana Wagemaker |
On Tools for Completeness of Kleene Algebra with Hypotheses
In the literature on Kleene algebra, a number of variants have been proposed which impose additional structure specified by a theory, such as Kleene algebra with tests (KAT) and the recent Kleene algebra with observations (KAO), or make specific assumptions about certain constants, as for instance in NetKAT. Many of these variants fit within the unifying perspective offered by Kleene algebra with hypotheses, which comes with a canonical language model constructed from a given set of hypotheses. For the case of KAT, this model corresponds to the familiar interpretation of expressions as languages of guarded strings. A relevant question therefore is whether Kleene algebra together with a given set of hypotheses is complete with respect to its canonical language model. In this paper, we revisit, combine and extend existing results on this question to obtain tools for proving completeness in a modular way. We showcase these tools by reproving completeness of KAT and treat several other examples.
|
Slides |
| 10:00 |
Jas Šemrl |
Domain Range Semigroups and Finite Representations
Relational semigroups with domain and range are a useful tool for modelling nondeterministic programs. We prove that the representation class R(D,R,*) is not finitely axiomatisable, answering [JM19, Question 4.9]. We show that any signature containing D, R, ˘, ; but not - or · has the finite representation property, an extension of the result for ordered domain algebras {0,1,D,R,≤,1',˘,;} [EH13]. We survey the results in the area of the finite representation property and raise a number of open questions.
|
Slides |
| 10:30 | Coffee break |
| 11:00 |
|
Session 12. Chair Jurriaan Rot |
| 11:00 |
Amina Doumane |
The class of representable semilattice-ordered monoids is not a variety
We show a necessary and a sufficient condition for a quasi-variety to be a variety. Using this, we show that the quasi-variety of representable semilattice-ordered monoids is not a variety.
|
|
| 11:30 |
Stepan Kuznetsov |
Relational Models for the Lambek calculus with Intersection and Unit
We consider the Lambek calculus extended with intersection (meet) operation. For its variant which does not allow empty antecedents, Andreka and Mikulas (1994) prove strong completeness w.r.t.\ relational models (R-models). Without the antecedent non-emptiness restriction, however, only weak completeness w.r.t.\ R-models (so-called square ones) holds (Mikulas 2015). Our goals are as follows. First, we extend the calculus with the unit constant, introduce a class of non-standard R-models for it, and prove completeness. This gives a simpler proof of Mikulas' result. Second, we prove that strong completeness does not hold. Third, we extend our weak completeness proof to the infinitary setting, to so-called iterative divisions (Kleene star under division).
|
Slides |
| 12:00 |
Matthias Naaf |
Computing Least and Greatest Fixed Points in Absorptive Semirings
We present two methods to algorithmically compute both least and greatest solutions of polynomial equation systems over absorptive semirings (with certain completeness and continuity assumptions), such as the tropical semiring. Both methods require a polynomial number of semiring operations, including semiring addition, multiplication and an infinitary power operation.Our main result is a closed-form solution for least and greatest fixed points based on the fixed-point iteration. The proof builds on the notion of (possibly infinite) derivation trees; a careful analysis of the shape of these trees allows us to collapse the fixed-point iteration to a linear number of steps. The second method is an iterative symbolic computation in the semiring of generalized absorptive polynomials, largely based on results on Kleene algebras.
|
Slides |
| 12:30 | Lunch |
| 14:00 |
|
Session 13. Chair Dale Miller |
| 14:00 |
Barbara König |
Fixpoint Games (invited talk)
Solving fixpoint equations is a recurring problem in several domains:
the result of a dataflow analysis can be characterized as either a
least or greatest fixpoint. It is well-known that bisimilarity - the
largest bisimulation - admits a characterization as a greatest
fixpoint and furthermore mu-calculus model-checking requires to solve
systems of nested fixpoint equations.
Often, these fixpoint equations or equation systems are defined over
powerset lattices, however in several applications - such as
lattice-valued or real-valued mu-calculi - the lattice under
consideration is not a powerset.
Hence we extend the notion of fixpoint games (or unfolding games,
introduced by Venema) to games for equation systems over more general
lattices. In particular continuous lattices admit a very elegant
characterization of the solution.
We will also describe how to define progress measures which describe
winning strategies for the existential players and explain how
abstractions and up-to functions can be integrated into the
framework.
(Joint work with Paolo Baldan, Tommaso Padoan, Christina
Mika-Michalski)
.
|
Slides |
| 15:00 |
Michael Winter |
Relational Sums and Splittings in Categories of L-fuzzy Relations
Dedekind categories and similar structures provide a suitable framework to reason about binary relations in an abstract setting. Arrow categories extend this theory by certain operations and axioms so that additional aspects of L-fuzzy relations become expressible. In particular, arrow categories allow to identify crisp relations among all relations. On the other hand, the new operations and axioms in arrow categories force the category to be uniform, i.e., to be within a particular subclass of Dedekind categories. As an extension, arrow categories inherit constructions from Dedekind categories such as the definition of relational sums and splittings. However, these constructions are usually modified in arrow categories by requiring that certain relations are additionally crisp. This additional crispness requirement and the fact that the category is uniform raises a general question about these constructions in arrow categories. When can we guarantee the existence of the construction with and without the additional requirement of crispness in the given arrow category or or an extension thereof? This paper provides a complete answer to this complex question for the two constructions mentioned.
|
Slides |
| 15:30 | Coffee break |
| 16:00 |
|
Session 14. Chair Luidnel Maignan |
| 16:00 |
Michael Winter |
FuReM - A System for Visualization and Manipulation of L-Fuzzy Relations (short talk)
In this presentation we will introduce the FuReM (Fuzzy Relation Manipulator) sys- tem. This system allows to visualize and manipulate so-called L-fuzzy relations similar to the RelView system.
|
Slides |
| 16:20 |
Jas Šemrl |
Finite Representation Property for Relation Algebra Reducts (short talk)
Membership in the Class of Representable Tarskian Relation Algebra is undecidable. However, dropping some operations to obtain a reduct language may introduce some more favourable properties. The Finite Representation Property (FRP) is a great example of good algebraic behaviour. A signature is said to have the FRP if every representable finite structure in that signature can be represented over a finite base set. Some positive implications of the FRP for a signature include the decidability of membership in the representation class for finite structures, as well as the decidability of membership in equational theory generated by the representation class. Although the property fails for the language of Relation Algebras, it remains an open question for many of its reduct languages. We examine the conjecture that a reduct language of Relation Algebra has the FRP if and only if it does not include negation and composition, nor meet and composition. Here we prove that any signature containing composition and negation fails to have the FRP. This preliminary result, together with FRP failing for any signature containing composition and meet [Neu16], proves the right to left implication of the conjecture. For the left to right implication, the FRP is known to hold for composition-free signatures as well as a handful of those containing composition. Furthermore, we show here that in any reduct signature with composition but neither meet nor negation a [finite] representable structure has a [finite] representation if and only if it embeds into a [finite] Relation Algebra (not necessarily representable). This suggests that well known counterexamples to FRP in other signatures, like the Point Algebra will have a finite base representation in signatures conjectured to have the FRP. Finally, we look at signatures, like that of join-lattice semigroups, where embedding a finite representable structure into a finite relation algebra appears to be especially difficult and look at examples of some of the more interesting known such embeddings.
|
Slides |
| 16:40 |
Roland Glück |
On the Computation of Isolated Sublattices (short talk)
In this short notice
we give some ideas how to compute isolated sublattices which can be used to derive a recursive algorithm for the computation of the number of closure operators on a finite lattice. We give an asymptotically optimal algorithm for deciding the existence and - in the case of existence - the computation of useful nontrivial isolated summit sublattices. The general case (i.e., an optimal algorithm for the computation of general nontrivial useful isolated sublattices) remains unsolved, however, we try to give some ideas and hints for future research.
|
Slides |
| 17:00 |
Manfred Droste, Sven Dziadek, and Werner Kuich |
Greibach Normal Form and Simple Automata for Weighted ω-Context-Free Languages (short talk)
In weighted automata theory, many classical results on formal languages have been ex- tended into a quantitative setting. Here, we investigate weighted context-free languages of infinite words, a generalization of ω-context-free languages (Cohen, Gold 1977) and an extension of weighted context-free languages of finite words (Chomsky, Schützenberger 1963). As in the theory of formal grammars, these weighted context-free languages, or ω-algebraic series, can be represented as solutions of (mixed) ω-algebraic systems of equations and by weighted ω-pushdown automata.
In our first main result, we show that (mixed) ω-algebraic systems can be transformed into Greibach normal form. We use the Greibach normal form in our second main result to prove that simple ω-reset pushdown automata recognize all ω-algebraic series. Simple ω-reset automata do not use ε-transitions and can change the stack only by at most one symbol. These results generalize fundamental properties of context-free languages to weighted context-free languages.
|
Slides |
| 17:20 |
Uli Fahrenberg, Christian Johansen, Georg
Struth and Krzysztof Ziemiański |
Languages of Higher-Dimensional Automata (short talk)
We introduce languages of higher-dimensional automata (HDAs) and develop some of their properties. To this end, we define a new category of precubical sets, uniquely naturally isomorphic to the standard one, and introduce a notion of event consistency. HDAs are then finite, labeled, event-consistent precubical sets with distinguished subsets of initial and accepting cells. Their languages are sets of interval orders closed under subsumption; as a major technical step we expose a bijection between interval orders and a subclass of HDAs. We show that any finite subsumption-closed set of interval orders is the language of an HDA, that languages of HDAs are closed under binary unions and parallel composition, and that bisimilarity implies language equivalence.
This work is part of an ongoing program to develop a theory of regular concurrent languages. In RAMiCS-18 the first three authors together with Ratan Bahadur Thapa introduced gluing-parallel posets with interfaces as a model for concurrent Kleene algebra. Here we develop the basics of HDA languages as sets of gluing-parallel pomsets, and in currently ongoing work we prove a Kleene theorem for such languages.
This talk is based on arxiv:2103.07557 which has recently been accepted for publication in MSCS. In the talk I will put this work in the context above.
|
Slides |
| 19:30 | Dinner |
| Saturday November 6, 2021 |
|---|
| 7:00 | Breakfast |
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.
Additionally to the standard CfP, RAMiCS is also calling for
short contributions and posters. We are hence calling for
presentations of original, unfinished, already published, or otherwise
interesting work within the topics of the RAMiCS conferences. The
submission can be in the form of a poster, an abstract, a paper
submitted to or published at another conference, etc. Short
contributions will not be published in the conference
proceedings.
