UWSpace

UWSpace is the University of Waterloo’s institutional repository for the free, secure, and long-term home of research produced by faculty, students, and staff.

Depositing Theses/Dissertations or Research to UWSpace

Are you a Graduate Student depositing your thesis to UWSpace? See our Thesis Deposit Help and UWSpace Thesis FAQ pages to learn more.

Are you a Faculty or Staff member depositing research to UWSpace? See our Waterloo Research Deposit Help and Self-Archiving pages to learn more.

Photo by Waterloo staff

Communities in UWSpace

Select a community to browse its collections.

Recent Submissions

  • Thumbnail Image
    Item type: Item ,
    Reducing CTL-live model checking to semantic entailment in first-order logic (version 1)
    (University of Waterloo, 2014-03-20) Vakili, Amirhossein; Day, Nancy A.
    The core of temporal logic model checking is the reachability problem, which is not expressible in first-order logic (FOL). Most model checking algorithms, both for finite and infinite Kripke structures, contain a loop that iterates to reach a fixed-point. As a result, reasoners with input languages no more expressive than FOL have been used iteratively for model checking rather than having the reasoner solve the problem completely by itself. In this article, we present a method for reducing model checking of finite and infinite Kripke structures that are expressed in FOL to entailment checking in FOL for a fragment of computational tree logic (CTL), which we call CTL-live. CTL-live includes all the CTL connectives that are expressible in the mu-calculus using the least fixed-point operator. These connectives are traditionally used to express liveness properties. This reduction allows us to consider model checking of CTL-live as a FOL theorem proving problem, and to use directly FOL reasoning techniques for model checking without the need of fixed-point operators, transitive-closure, or induction. We prove that CTL-live is maximal in the sense that model checking of CTL connectives that are not included in CTL-live is not reducible to semantic entailment in FOL.
  • Thumbnail Image
    Item type: Item ,
    A multiagent-based simulation model to support management decision making in software development
    (University of Waterloo, 2014-03-06) Baina, Davy; Lucena, Carlos J. P.; Cowan, Donald; Bommel, Pierre; Valdares, Carolina; Oliveira, Toacy
    Context Techniques to support the development of software projects and describe the quality of the results have received substantial attention from the research community because software projects often do not achieve their intended results in terms of factors such as time to completion and quality of the final product. Objective In this paper, we propose a MultiAgent-Based Simulation Model to support project managers in the decision-making process that is required in the creation of software systems. This model is based on the Project Management Body of Knowledge (PMBOK) in areas such as cost, time, scope and human resources. Methods We present an illustrative example that was drawn from our experience with real-world software development projects conducted within our research group. Such an example demonstrates the benefits and drawbacks of using MultiAgent System simulation as a support tool for the project manager's decision-making process. Results We have created a simulation model and associated scenarios that allow a project manager to analyze strategic options throughout the project. Each option is based on the PMBOK practices allowing project managers to investigate the best scenario that meets the project needs such as cost, time and quality. Conclusions Some factors are crucial to the success or failure of a project. Decisions made by the project manager are one such set of factors that determine if the project goals are achievable. Through using MABS to simulate scenarios we have become convinced that this approach can contribute to the understanding of the phenomena that occur during a software development project and provide real assistance to the project manager.
  • Thumbnail Image
    Item type: Item ,
    A multiagent based context-aware and self-adaptive model for virtual network provisioning
    (University of Waterloo, 2014-02-28) Valadares, Carolina; Cowan, Donald; Lucena, Carlos; Baia, Davy
    Recent research in network virtualization has focused on the Internet ossification problem [1] whereby multiple independent virtual networks (VN) [1] that exhibit a high degree of autonomy share physical resources and can provide services with varying degrees of quality. Thus, the Network field has taken evolutionary steps on re-thinking the design and architectural principles of VN [2][3]. However, to the best of our knowledge, there has been little investigation into the autonomic behaviour of such architectures [4][5]. This paper describes an attempt to use Multiagent System (MAS) principles to design an autonomic and self-adaptive model for virtual network provisioning (VNP) that fills a gap in the current Internet architecture. In addition, we provide an analysis of the requirements of self-adaptive provisioning for designing reliable autonomic model that is able to self-organize its own resources, with no external control, in order to cope with environmental changes. Such behaviour will be required as the next generation Internet evolves. Through our evaluation, we demonstrate that the model achieves its main purpose of efficiently self-organizing the VN, since it is able to anticipate critical scenarios and trigger corresponding adaptive plans.
  • Thumbnail Image
    Item type: Item ,
    Secure and Efficient Computation Offloading in Mobile Edge Computing Networks
    (University of Waterloo, 2026-08-24) Qin, Xue
    The Internet of Things (IoT) enables large numbers of connected devices to support intelligent, delay-sensitive, and computation-intensive applications. However, IoT devices are typically constrained by limited computing capability, storage capacity, and energy supply. Mobile edge computing (MEC) addresses these limitations by deploying computing resources close to IoT devices, allowing computation-intensive tasks to be processed at nearby edge servers. During wireless offloading, IoT devices may transmit either raw task data or computational workloads for edge processing, or compact task-relevant semantic representations for edge inference. These two offloading paradigms aim to achieve reliable and efficient task processing and accurate and communication-efficient edge inference, respectively. Achieving these objectives in practical MEC networks involves three key challenges. First, due to the broadcast nature of wireless communications, the transmitted information may be intercepted by passive eavesdroppers, resulting in raw-data leakage or semantic privacy risks. Second, time-varying wireless channels, stochastic task arrivals, and fluctuating edge resources make offloading, transmission, and computing decisions highly coupled. Third, different IoT applications impose diverse quality-of-service (QoS) requirements, including latency, reliability, energy efficiency, deadline-aware task completion, and task accuracy. These requirements are often coupled and may conflict with each other. Considering these challenges, the objective of this thesis is to develop secure, efficient, and QoS-aware computation offloading solutions for dynamic MEC networks under eavesdropping threats. From a user-centric perspective, three research problems are investigated. The considered system progressively evolves from a single-user single-server scenario to a single-user multi-server collaborative scenario and further to a multi-user multi-server scenario. Meanwhile, the protection objective extends from transmission-level data security to representation-level semantic privacy. First, secure partial computation offloading is investigated in a single-user single-server MEC system. Each divisible task is partitioned between local processing and edge processing, while friendly jammer-assisted physical-layer security is employed to protect the offloaded task data. The offloading ratio, friendly jammer selection, and edge-server CPU-frequency allocation are jointly optimized under dynamic task and wireless conditions. The resulting long-term optimization problem is formulated as a Markov decision process with a hybrid discrete-continuous action space. To solve this problem, a hybrid-action deep deterministic policy gradient (HDDPG) algorithm is developed. The proposed approach supports secure, energy-efficient, and deadline-aware computation offloading by improving task completion performance while reducing energy consumption. Second, the system is extended to a single-user multi-server collaborative MEC scenario. A divisible task can be partitioned among local computing and multiple nearby edge servers, enabling parallel processing and collaborative use of distributed edge resources. This scenario introduces higher-dimensional and more strongly coupled decisions, including the task partition ratios, friendly jammer selections, and CPU-frequency allocations across multiple servers. An Omni-DDPG framework is developed to jointly optimize these constrained continuous, discrete, and continuous decisions. The proposed framework improves secure task completion, latency, and energy efficiency through coordinated task partitioning, security control, and edge-resource allocation. Extended multi-user simulations further demonstrate the scalability potential of the learned policy in larger collaborative MEC settings. Third, semantic privacy-preserving offloading is studied in a multi-user multi-server MEC system. Unlike the first two works, which focus on data-oriented secure offloading, this work considers semantic offloading, where IoT devices transmit compact task-relevant latent representations instead of complete raw task data. Although this approach reduces communication overhead, the transmitted representations may still expose sensitive task-related information to passive eavesdroppers. To address this issue, a diffusion-based semantic encoding framework is developed. A forward diffusion process generates approximately noise-like latent representations before wireless transmission, while an authorized edge server employs a learned reverse diffusion model to recover task-relevant representations for downstream inference. The framework is evaluated under wireless channel noise and quantization and compared with autoencoder- and variational autoencoder-based semantic encoders. The results demonstrate a favorable trade-off among task accuracy, semantic privacy, transmission latency, and energy efficiency. In summary, this thesis presents a progressive investigation of secure and efficient computation offloading across different MEC system scales and protection levels. The first two works develop learning-based control solutions for data-oriented secure offloading, while the third work extends the protection objective to semantic privacy-preserving offloading. The proposed solutions address task offloading, resource allocation, wireless transmission security, and semantic representation protection, providing algorithmic and practical foundations for scalable, secure, and intelligent edge computing systems.
  • Thumbnail Image
    Item type: Item ,
    Fatigue Behavior of a Unidirectional Non-crimp Fabric Glass Fiber Reinforced Reactive Thermoplastic Composite
    (Canadian Association for Composite Structures and Materials (CACSMA), 2022-08-12) Shi, Erli; Montesano, John
    Wind turbines are being used in regions where exposure to extremely low temperatures and high winds has become the standard operating condition, which increases the demand on the turbine blade structure. Wind turbine blades are typically manufactured from glass fiber/epoxy laminates, which tend to exhibit increased brittle failure modes with decreasing operating temperatures. In order to improve the performance of wind turbine blades under extreme operating conditions, replacing conventional glass fiber/epoxy composite materials with resin-infusible glass fiber/reactive thermoplastic composite materials may provide several benefits, including improved low-temperature toughness and end-of-life recyclability. The goal of this study was to assess the fatigue performance of a resin-infused unidirectional (UD) non-crimp fabric (NCF) glass fiber/acrylic composite material at room temperature (RT) and -50°C. Tension-tension fatigue tests were conducted on UD specimens to compare the relative performance, fatigue life, and fatigue resistance. The increase in temperature during the different stages of the RT fatigue tests was monitored using a high-definition infrared camera to provide a qualitative assessment of damage evolution.