https://www.um.edu.mt/library/oar/handle/123456789/10956 Sun, 15 Nov 2026 22:53:24 GMT 2026-11-15T22:53:24Z https://www.um.edu.mt/library/oar/handle/123456789/150964 Title: Behavioural theories for concurrent actors Abstract: In this work, we start by examining concurrent programming paradigms, specifically the actor model, and the challenges of formally ensuring that system refactorings preserve original behaviour. We explore the use of contextual behavioural theories to reason about these safety issues rigorously. While trace-based techniques are suggested as an improvement over the intractable nature of contextual testing, their inability to tractably reason about programs with an infinite number of traces prompts the need for another method of analysing actor systems. Furthermore, existing trace-based techniques use the notion of binding over traces to keep track of names, which becomes cumbersome as actor systems dynamically extrude names and grow in size. To address these gaps, this work presents a unified formal behavioural theory for concurrent actors. The primary contributions to knowledge include, first, the K | O ⊢ environment. This knowledge framework replaces trace binding by strictly enforcing the single-receiver property and elegantly handling dynamic name extrusion through defining known names and valid observer interfaces upfront. Second, we introduce an optimised trace preorder that restricts unobservable inputs, alongside a method for constructing a general observer. These results are required to demonstrate that trace techniques are both sound and complete with respect to safety testing. Finally, we present an asynchronous, set-based simulation. This framework based on coinductive reasoning is built to handle asynchronous actor systems that exhibit persistent behaviour and non-deterministic branching, allowing us to overcome the infinite-state analysis problem found in trace techniques, and simplifying the comparison of complex systems. Ultimately, these results establish a complete, provably equivalent behavioural theory that bridges contextual, trace-based, and coinductive preorders. This provides a scalable, mathematically rigorous model to safely verify system refactorings and component equivalence in modern, highly dynamic concurrent systems without the need for exhaustive testing. Description: Ph.D.(Melit.) Wed, 01 Jan 2025 00:00:00 GMT https://www.um.edu.mt/library/oar/handle/123456789/150964 2025-01-01T00:00:00Z https://www.um.edu.mt/library/oar/handle/123456789/150963 Title: Extending the limits of monitorability Abstract: One of the most fundamental and long-standing issues in computer science is making sure that a system behaves as intended. To address this challenge, systems may be veri ed dynamically using a lightweight monitoring technique called runtime verification. Even though runtime verification circumvents issues associated with traditional techniques, it is limited by the fact that observations are typically constrained to the current computation path of the system. This limitation is even more acute for correctness properties describing the system’s computational graph, known as branching-time properties. This thesis investigates whether runtime verification can be extended to meaningfully verify a wider range of branching-time properties. We depart from the classical setup where monitoring is limited to a single execution and investigate the enhanced observational capabilities when monitoring a system over multiple runs. To ensure generality in our results, we focus on branching-time properties expressed in the modal-calculus, a well-studied foundational logic used by state-of-the-art model checkers. As part of a comprehensive theory, the rst part of this thesis focuses on deterministic systems and demonstrates that the proposed multi-run monitoring setup can systematically extend previously established monitorability limits for branching-time properties. The second part extends the multi-run framework and corresponding results to systems that may exhibit non-deterministic behaviour. To show that the proposed setup is implementable, the third part outlines the steps for a full automation, as well as proves bounds that capture the correspondence between the syntactic structure of a property and the number of system runs required to adequately verify it. We also validate our results by instantiating the proposed multi-run monitoring setup to verify actor-based concurrent systems, a widely used concurrency paradigm. Given that these systems are inherently non-deterministic, the fourth part presents a general study of a highly non-deterministic calculus, where we systematically explore how the defining characteristics of the actor model enable the recovery of a certain degree of determinism. Description: Ph.D.(Melit.) Wed, 01 Jan 2025 00:00:00 GMT https://www.um.edu.mt/library/oar/handle/123456789/150963 2025-01-01T00:00:00Z https://www.um.edu.mt/library/oar/handle/123456789/144338 Title: Towards the efficient adaptation of offline physically based methods for real-time rendering Abstract: Rendering physically accurate caustics in real-time remains a persistent challenge due to their complex light interactions and high-frequency features. This thesis presents a comprehensive exploration into adapting oìine physically based rendering techniques for real-time caustic synthesis on modern GPU architectures. Central to this work is CandelaDXR, a GPU-accelerated light tracer that employs novel importance sampling strategies to improve convergence speed and visual adelity for caustics. By generating dynamic probability distribution functions conditioned on scene geometry, camera parameters, and material properties, CandelaDXR prioritises specular interactions and focuses sampling eêorts on perceptually relevant regions. To support this system, two auxiliary tools were developed: Anvil, a modular visual debugging platform for rendering pipelines, and Forge, an evaluation framework designed to facilitate reproducible, cross-system comparisons. These tools provide both insight and rigour in diagnosing rendering artefacts and validating algorithmic improvements. Additionally, the thesis introduces a spectral denoising pipeline tailored to the distinct characteristics of caustic signals, demonstrating the eêectiveness of Fourier, wavelet and curvelet-based transforms in preserving detail while reducing noise. Quantitative results across multiple scenes and viewpoints reveal signiacant performance gains, noise reduction, and perceptual improvements in CandelaDXR over baseline methods. Collectively, this work contributes a uniaed architecture for real-time caustic rendering, debugging, and evaluation, offering practical advances in both rendering theory and implementation for real-time physically based graphics. Description: Ph.D.(Melit.) Wed, 01 Jan 2025 00:00:00 GMT https://www.um.edu.mt/library/oar/handle/123456789/144338 2025-01-01T00:00:00Z https://www.um.edu.mt/library/oar/handle/123456789/140084 Title: Beyond single traces : implementing multiple execution monitoring in DetectEr Abstract: Runtime verification (RV) has emerged as a crucial technique for ensuring software correctness by monitoring system execution against formally specified properties. However, traditional RV approaches are limited to analyzing single execution traces, restricting their ability to verify properties that require evidence from multiple system runs, particularly in branching-time systems. This project extends DetectEr, an open-source runtime verification tool for actor-based systems, to support multiple execution monitoring. The extension enables verification of safety properties expressed in sHML∨ Det, an enhanced specification language that incorporates disjunctive operators beyond the original Safety Hennessy-Milner Logic (sHML). The implementation addresses three key challenges: adapting the theoretical framework to handle first-order events with data values, developing a robust history aggregation mechanism using Erlang Term Storage tables with trace normalisation, and implementing a breadth-first search algorithm for the history analysis proof system. The approach successfully demonstrates the practical feasibility of multiple execution monitoring through evaluation using a calculator server case study. The results show that the extended framework maintains backward compatibility with existing DetectEr functionality while enabling verification of previously unmonitorable properties, such as implication-based conditions requiring evidence across multiple execution traces. This work contributes to the runtime verification field by demonstrating that multiple execution monitoring can be effectively integrated into existing RV frameworks, expanding their verification capabilities. Description: B.Sc. (Hons)(Melit.) Wed, 01 Jan 2025 00:00:00 GMT https://www.um.edu.mt/library/oar/handle/123456789/140084 2025-01-01T00:00:00Z