Logical and Algebraic Investigations into Properties of Concurrent Systems

This dissertation is intended to contribute to the logical and algebraic study of behavioural properties of concurrent systems from two complementary perspectives: a static one, focused on the compositional analysis of finite-trace properties in interleaving systems, and a dynamic one, exploring the modelling, specification, and verification of dynamic epistemic multi-agent systems. Accordingly, the work is organised into two parts. In Part I, within the interleaving approach to concurrency, the thesis develops a proof-theoretic framework for the structural analysis of finite-trace properties, with particular emphasis on those defined via prefix-closure. The interaction of the prefix-closure operator and its residual (with respect to set-theoretic inclusion) with intersection, union, and language concatenation is investigated. The variety of closure l-monoids is introduced as a minimal algebraic abstraction of finite-trace properties, amenable to description within an analytic proof system. As a proof-theoretic counterpart to these structures, the display-like sequent calculus LMC is introduced and shown to be sound and complete, to admit cut elimination, and to be decidable. Altogether, this approach supports an algebraic and proof-theoretic analysis of finite-trace property patterns of verification relevance, while providing a compositional treatment of safety, liveness, and related notions. In Part II, a unified approach to the modelling and verification of knowledge-based dynamic multi-agent systems is developed. A new model of computation, called a Kripke labelled transition system (KLTS), is introduced, combining labelled transition systems with multi-agent Kripke frames to support uniform reasoning about system dynamics and the evolution of agents’ knowledge. On this basis, the logic EHML is defined by combining Hennessy–Milner Logic with the normal multimodal logic S5n. A Hilbert-style proof system for EHML is provided; soundness and completeness with respect to the intended semantics, as well as decidability, are established. The logic is shown to be associated with a bisimulation that characterises behavioural equivalence in KLTS-based models of the systems of interest. Finally, building on the KLTS semantics, the process-algebraic language ECCS is introduced to support modular specification and analysis of concurrent multi-agent systems, with running examples drawn from real-world multi-agent standards. Overall, this thesis aims to advance the mathematical foundations of the formal analysis and verification of concurrent systems, fostering the interaction between logical/algebraic methods and computational modelling techniques.