Search

We consider process algebras with branching parametrized by an equational theory T, and show that it is possible to axiomatize bisimilarity under certain conditions on T. Our proof abstracts an earlier argument due to Grabmayer and Fokkink (LICS'20), and yields new completeness theorems for skip-free process algebras with probabilistic (guarded) branching, while also covering existing completeness results.

We forge connections between the theory of fractal sets obtained as attractors of iterated function systems and process calculi. To this end, we reinterpret Milner's expressions for processes as contraction operators on a complete metric space. When the space is, for example, the plane, the denotations of fixed point terms correspond to familiar fractal sets. We give a sound and complete axiomatization of fractal equivalence, the congruence on terms consisting of pairs that construct identical self-similar sets in all interpretations. We further make connections to labelled Markov chains and to invariant measures. In all of this work, we use important results from process calculi. For example, we use Rabinovich's completeness theorem for trace equivalence in our own completeness theorem. In addition to our results, we also raise many questions related to both fractals and process calculi., Comment: Expanded and edited into a journal version. Submitted to the CALCO 2023 special issue of LMCS

We introduce Probabilistic Guarded Kleene Algebra with Tests (ProbGKAT), an extension of GKAT that allows reasoning about uninterpreted imperative programs with probabilistic branching. We give its operational semantics in terms of special class of probabilistic automata. We give a sound and complete Salomaa-style axiomatisation of bisimilarity of ProbGKAT expressions. Finally, we show that bisimilarity of ProbGKAT expressions can be decided in $O(n^3 \log n)$ time via a generic partition refinement algorithm.

Guarded Kleene Algebra with Tests (GKAT) is a fragment of Kleene Algebra with Tests (KAT) that was recently introduced to reason efficiently about imperative programs. In contrast to KAT, GKAT does not have an algebraic axiomatization, but relies on an analogue of Salomaa's axiomatization of Kleene Algebra. In this paper, we present an algebraic axiomatization and prove two completeness results for a large fragment of GKAT consisting of skip-free programs.

A recently published paper (Schmid, Rozowski, Silva, and Rot, 2022) offers a (co)algebraic framework for studying processes with algebraic branching structures and recursion operators. The framework captures Milner's algebra of regular behaviours (Milner, 1984) but fails to give an honest account of a closely related calculus of probabilistic processes (Stark and Smolka, 1999). We capture Stark and Smolka's calculus by giving an alternative framework, aimed at studying a family of ordered process calculi with inequationally specified branching structures and recursion operators. We observe that a recent probabilistic extension of guarded Kleene algebra with tests (Rozowski, Kozen, Kappe, Schmid, Silva, 2022) is a fragment of one of our calculi, along with other examples. We also compare the intrinsic order in our process calculi with the notion of similarity in coalgebra.

It came to the attention of myself and the coauthors of (S., Rozowski, Silva, Rot, 2022) that a number of process calculi can be obtained by algebraically presenting the branching structure of the transition systems they specify. Labelled transition systems, for example, branch into sets of transitions, terms in the free semilattice generated by the transitions. Interpreting equational theories in the category of sets has undesirable limitations, and we would like to have more examples of presentations in other categories. In this brief article, I discuss monad presentations in the category of partially ordered sets and monotone maps. I focus on quantitative monads, namely free modules over ordered semirings, and give sufficient conditions for one of these to lift a monad on the category of sets. I also give a description of ordered semirings that are useful for specifying unguarded recursive calls. Examples include ordered probability theory and ordered semilattices.

We develop a (co)algebraic framework to study a family of process calculi with monadic branching structures and recursion operators. Our framework features a uniform semantics of process terms and a complete axiomatisation of semantic equivalence. We show that there are uniformly defined fragments of our calculi that capture well-known examples from the literature like regular expressions modulo bisimilarity and guarded Kleene algebra with tests. We also derive new calculi for probabilistic and convex processes with an analogue of Kleene star.

There is a large amount of literature on the topic of covarieties, coequations and coequational specifications, dating back to the early seventies. Nevertheless, coequations have not (yet) emerged as an everyday practical specification formalism for computer scientists. In this review paper, we argue that this is partly due to the multitude of syntaxes for writing down coequations, which seems to have led to some confusion about what coequations are and what they are for. By surveying the literature, we identify four types of syntaxes: coequations-as-corelations, coequations-as-predicates, coequations-as-equations, and coequations-as-modal-formulas. We present each of these in a tutorial fashion, relate them to each other, and discuss their respective uses., Comment: Appeared in CALCO 2021

An open problem posed by Milner asks for a proof that a certain axiomatisation, which Milner showed is sound with respect to bisimilarity for regular expressions, is also complete. One of the main difficulties of the problem is the lack of a full Kleene theorem, since there are automata that can not be specified, up to bisimilarity, by an expression. Grabmayer and Fokkink (2020) characterise those automata that can be expressed by regular expressions without the constant 1, and use this characterisation to give a positive answer to Milner's question for this subset of expressions. In this paper, we analyse Grabmayer and Fokkink's proof of completeness from the perspective of universal coalgebra, and thereby give an abstract account of their proof method. We then compare this proof method to another approach to completeness proofs from coalgebraic language theory. This culminates in two abstract proof methods for completeness, what we call the local and global approaches, and a description of when one method can be used in place of the other., Comment: In Proceedings MFPS 2021, arXiv:2112.13746

Guarded Kleene Algebra with Tests (GKAT) is an efficient fragment of KAT, as it allows for almost linear decidability of equivalence. In this paper, we study the (co)algebraic properties of GKAT. Our initial focus is on the fragment that can distinguish between unsuccessful programs performing different actions, by omitting the so-called early termination axiom. We develop an operational (coalgebraic) and denotational (algebraic) semantics and show that they coincide. We then characterize the behaviors of GKAT expressions in this semantics, leading to a coequation that captures the covariety of automata corresponding to behaviors of GKAT expressions. Finally, we prove that the axioms of the reduced fragment are sound and complete w.r.t. the semantics, and then build on this result to recover a semantics that is sound and complete w.r.t. the full set of axioms., Comment: 32 pages

Work of Eagle, Farah, Goldbring, Kirchberg, and Vignati shows that the only separable C*-algebras that admit quantifier elimination in continuous logic are $\mathbb{C},$ $\mathbb{C}^2,$ $M_2(\mathbb{C}),$ and the continuous functions on the Cantor set. We show that, among finite dimensional C*-algebras, quantifier elimination does hold if the language is expanded to include two new predicate symbols: One for minimal projections, and one for pairs of unitarily conjugate projections. Both of these predicates are definable, but not quantifier-free definable, in the usual language of C*-algebras. We also show that adding just the predicate for minimal projections is sufficient in the case of full matrix algebras, but that in general both new predicate symbols are required., Comment: 11 pages