RAMiCS 2021 Accepted Papers with Abstracts

Abstract: 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.

Abstract: 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.

Abstract: 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.

Abstract: 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.

Abstract: 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.

Abstract: 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.

Abstract: 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.

Abstract: 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.

Abstract: 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.

Abstract: 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.

Abstract: 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.

Abstract: 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.

Abstract: 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).

Abstract: 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.

Abstract: 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.

Abstract: 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.

Abstract: 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.

Abstract: 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.

Abstract: 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.

Abstract: 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.

Abstract: 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.

Abstract: 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.

Abstract: 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.

Abstract: 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.

Abstract: 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.

Abstract: 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.

Abstract: 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.

Abstract: 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 \emph{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.

Abstract: In economics and multi-agent systems, \emph{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 \emph{Aumman structures}), it can be computed in time $O(n\alpha(n))$ where $\alpha(n)$ is the inverse of the Ackermann function.