https://www.um.edu.mt/library/oar/handle/123456789/8421 Sun, 15 Nov 2026 01:25:39 GMT 2026-11-15T01:25:39Z 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/150522 Title: Novel data analytics techniques for analysing satellite imagery data, traffic and environment pollution data to predict the hospital admission rates Abstract: Accurately forecasting hospital admissions is critical for optimizing healthcare resource allocation and emergency preparedness. This study presents a comprehensive, data-driven framework for predicting emergency department (ED) admissions related to respiratory, circulatory, and all-cause health conditions using local ground stations and satellite-based meteorological and air pollution data. Despite growing evidence linking environmental factors to hospital admissions, traditional hospital management systems lack integration with environmental intelligence and encounters problem in utilizing resources. To bridge this gap, our research employs advanced machine learning and deep learning models including tree-based, neural network, and regularized regression techniques to capture complex, nonlinear relationships between environmental exposure and health outcomes. A key contribution of this work is the introduction of three novel prediction schemes: Deep Explainable AI For Respiratory-Based Prediction (DXAIRP) for respiratory admissions, Deep Explainable AI For Circulatory-Based Prediction (DXAICP) for circulatory admissions, and Explainable Extreme Gradient Boosting Scheme for Environmental Impact on All-Cause Emergency Admissions (BGXAI) for all-cause admissions. These schemes were rigorously evaluated across multiple datasets, demonstrating high predictive performance and reliability. The analysis revealed that air pollution parameters (PM2.5, PM10, CO, NO2, and O3) are the most significant predictors of hospital admissions, while meteorological factors such as wind speed, temperature, and relative humidity also contribute, albeit to a lesser extent. The study further identified optimal lag times for different admission types, with a two-day lag providing the highest accuracy for respiratory and circulatory admissions, and a three-day lag optimizing all-cause admission predictions. Additionally, results indicate that ground-based environmental data yield superior predictive accuracy compared to satellite-derived measurements. To ensure interpretability and trust in AI-driven predictions, the framework integrates SHapley Additive exPlanations (SHAP), an Explainable AI (XAI) technique that elucidates the influence of each environmental factor on model outputs. The Extreme Gradient Boosting Regressor (XGBR) and Multi-Layer Perceptron Regressor (MLPR), and their ensembling with XAI establishes a robust, transparent, and adaptable predictive approach. Beyond its academic contributions, this research has significant practical implications. The predictive framework can be integrated into hospital management systems to support data-driven decision-making, enabling healthcare administrators to anticipate ED surges and optimize resource distribution. This framework includes ground station-based data to capture localized environmental conditions and also integrates satellite-based environmental data, making it particularly valuable for regions with limited ground monitoring infrastructure, thereby addressing spatial and temporal gaps in environmental health monitoring. Overall, this research advances climate-health analytics by offering a scalable, interpretable, and data-driven methodology for predicting hospital admissions based on environmental factors. The findings contribute to the growing field of AI-driven healthcare forecasting, with potential applications in national health systems, expansion to other disease categories, and deployment in resource-limited settings through cloud-based infrastructures. Description: Ph.D.(Melit.) Wed, 01 Jan 2025 00:00:00 GMT https://www.um.edu.mt/library/oar/handle/123456789/150522 2025-01-01T00:00:00Z https://www.um.edu.mt/library/oar/handle/123456789/150298 Title: Image denoising in low-light conditions Abstract: This project presents a concise comparison of classical and modern image denoising techniques, addressing the problem of restoring images degradated by noise while preserving perceptual and structural detail. The primary goal is to evaluate and contrast representative classical algorithms with contemporary deep-learning models across controlled synthetic noise levels and a curated real-world photograph dataset. Experiments measure restoration fidelity, inference time and storage footprint using standard image quality metrics (peak signal-to-noise ratio and structural similarity index), runtime benchmarks and recorded model weight sizes, and the evaluation scripts and per-image results are provided in the repository to ensure reproducibility. Results demonstrate that deep networks typically achieve higher fidelity on synthetically degradated images and superior qualitative restoration on many real-world examples, whereas classical methods remain competitive at lower noise intensities and require substantially less computational and storage resources. The report discusses practical trade-offs including latency, model size and quantisation considerations, and concludes with recommendations for selecting denoising approaches in research and deployment contexts. All generated tables and code used to produce the results are available in the project repository. Description: B.Sc. (Hons)(Melit.) Thu, 01 Jan 2026 00:00:00 GMT https://www.um.edu.mt/library/oar/handle/123456789/150298 2026-01-01T00:00:00Z