Theoretical investigations of algebras yielded expressivity and complexity results; expressive algebras are needed to formalize interesting properties of processes, but the complexity of the algebra must be reasonably low so that it can serve as a tool for automated reasoning.

The aim of this project is to investigate algebras of binary relations that are suitable for a high-level reasoning about parallel processes. In particular, we will concentrate on algebras of binary relations that contain a (lower) semilattice reduct, since set-theoretic intersection can model parallel composition of programs. The interaction between the various program constructs has not been fully understood in the algebraic setting. Our aim is to clarify precisely which classes of algebars of binary relations can be (finitely) axiomatized and to determine the complexity of their (quasi-)equational theories. This will lead to a better understanding of the behaviour of (parallel) processes and serve as a theoretical foundation for verification and specification of processes.

Publications of Szabolcs Mikulas on these topics can be found here.