Theory and Algorithms Commons^™

An Idealist’S Approach For Smart Contract Correctness, Duy Tai Nguyen, Hong Long Pham, Jun Sun, Quang Loc Le

Research Collection School Of Computing and Information Systems

In this work, we experiment an idealistic approach for smart contract correctness verification and enforcement, based on the assumption that developers are either desired or required to provide a correctness specification due to the importance of smart contracts and the fact that they are immutable after deployment. We design a static verification system with a specification language which supports fully compositional verification (with the help of function specifications, contract invariants, loop invariants and call invariants). Our approach has been implemented in a tool named iContract which automatically proves the correctness of a smart contract statically or checks the unverified part …

Robust Maximum Capture Facility Location Under Random Utility Maximization Models, Tien Thanh Dam, Thuy Anh Ta, Tien Mai

Research Collection School Of Computing and Information Systems

We study a robust version of the maximum capture facility location problem in a competitive market, assuming that each customer chooses among all available facilities according to a random utility maximization (RUM) model. We employ the generalized extreme value (GEV) family of models and assume that the parameters of the RUM model are not given exactly but lie in convex uncertainty sets. The problem is to locate new facilities to maximize the worst-case captured user demand. We show that, interestingly, our robust model preserves the monotonicity and submodularity from its deterministic counterpart, implying that a simple greedy heuristic can guarantee …

Joint Location And Cost Planning In Maximum Capture Facility Location Under Random Utilities, Ngan H. Duong, Tien Thanh Dam, Thuy Anh Ta, Tien Mai

Research Collection School Of Computing and Information Systems

We study a joint facility location and cost planning problem in a competitive market under random utility maximization (RUM) models. The objective is to locate new facilities and make decisions on the costs (or budgets) to spend on the new facilities, aiming to maximize an expected captured customer demand, assuming that customers choose a facility among all available facilities according to a RUM model. We examine two RUM frameworks in the discrete choice literature, namely, the additive and multiplicative RUM. While the former has been widely used in facility location problems, we are the first to explore the latter in …

Motif-Cluster: A Spatial Clustering Package For Repetitive Motif Binding Patterns, Mengyuan Zhou

Department of Computer Science and Engineering: Dissertations, Theses, and Student Research

Previous efforts in using genome-wide analysis of transcription factor binding sites (TFBSs) have overlooked the importance of ranking potential significant regulatory regions, especially those with repetitive binding within a local region. Identifying these homogenous binding sites is critical because they have the potential to amplify the binding affinity and regulation activity of transcription factors, impacting gene expression and cellular functions. To address this issue, we developed an open-source tool Motif-Cluster that prioritizes and visualizes transcription factor regulatory regions by incorporating the idea of local motif clusters. Motif-Cluster can rank the significant transcription factor regulatory regions without the need for experimental …

Artificial Intelligence History, And Libraries: History And Legacy Of Library Contributions To Machine Learning, Wilhelmina Randtke

Library Faculty Presentations

Machine learning seems to be newly everywhere. It's not new, so much as faster processing makes it newly useful. Imagine an automated cataloging program that takes 300 years to run, versus one that takes a week to run. Increased processing speed is a substantive change. This presentation overviews the history of libraries and artificial intelligence. First, teasing out past applications of machine learning in libraries. High quality results and concrete applications of artificial intelligence in libraries have been explored and published for decades. Over time, faster processing allows use at scale. Second, how library and metadata work contributes to machine …

Multi-Representation Variational Autoencoder Via Iterative Latent Attention And Implicit Differentiation, Nhu Thuat Tran, Hady Wirawan Lauw

Research Collection School Of Computing and Information Systems

Variational Autoencoder (VAE) offers a non-linear probabilistic modeling of user's preferences. While it has achieved remarkable performance at collaborative filtering, it typically samples a single vector for representing user's preferences, which may be insufficient to capture the user's diverse interests. Existing solutions extend VAE to model multiple interests of users by resorting a variant of self-attentive method, i.e., employing prototypes to group items into clusters, each capturing one topic of user's interests. Despite showing improvements, the current design could be more effective since prototypes are randomly initialized and shared across users, resulting in uninformative and non-personalized clusters.To fill the gap, …

Instance-Specific Algorithm Configuration Via Unsupervised Deep Graph Clustering, Wen Song, Yi Liu, Zhiguang Cao, Yaoxin Wu, Qiqiang Li

Research Collection School Of Computing and Information Systems

Instance-specific Algorithm Configuration (AC) methods are effective in automatically generating high-quality algorithm parameters for heterogeneous NP-hard problems from multiple sources. However, existing works rely on manually designed features to describe training instances, which are simple numerical attributes and cannot fully capture structural differences. Targeting at Mixed-Integer Programming (MIP) solvers, this paper proposes a novel instances-specific AC method based on end-to-end deep graph clustering. By representing an MIP instance as a bipartite graph, a random walk algorithm is designed to extract raw features with both numerical and structural information from the instance graph. Then an auto-encoder is designed to learn dense …

Deep Reinforcement Learning With Explicit Context Representation, Francisco Munguia-Galeano, Ah-Hwee Tan, Ze Ji

Research Collection School Of Computing and Information Systems

Though reinforcement learning (RL) has shown an outstanding capability for solving complex computational problems, most RL algorithms lack an explicit method that would allow learning from contextual information. On the other hand, humans often use context to identify patterns and relations among elements in the environment, along with how to avoid making wrong actions. However, what may seem like an obviously wrong decision from a human perspective could take hundreds of steps for an RL agent to learn to avoid. This article proposes a framework for discrete environments called Iota explicit context representation (IECR). The framework involves representing each state …

Toward Intention Discovery For Early Malice Detection In Cryptocurrency, Ling Cheng, Feida Zhu, Yong Wang, Ruicheng Liang, Huiwen Liu

Research Collection School Of Computing and Information Systems

Cryptocurrency’s pseudo-anonymous nature makes it vulnerable to malicious activities. However, existing deep learning solutions lack interpretability and only support retrospective analysis of specific malice types. To address these challenges, we propose Intention-Monitor for early malice detection in Bitcoin. Our model, utilizing Decision-Tree based feature Selection and Complement (DT-SC), builds different feature sets for different malice types. The Status Proposal Module (SPM) and hierarchical self-attention predictor provide real-time global status and address label predictions. A survival module determines the stopping point and proposes the status sequence (intention). Our model detects various malicious activities with strong interpretability, outperforming state-of-the-art methods in extensive …

Configuring Timing Parameters To Ensure Execution-Time Opacity In Timed Automata, Étienne André, Engel Lefaucheux, Didier Lime, Dylan Marinho, Jun Sun

Research Collection School Of Computing and Information Systems

Timing information leakage occurs whenever an attacker successfully deduces confidential internal information by observing some timed information such as events with timestamps. Timed automata are an extension of finite-state automata with a set of clocks evolving linearly and that can be tested or reset, making this formalism able to reason on systems involving concurrency and timing constraints. In this paper, we summarize a recent line of works using timed automata as the input formalism, in which we assume that the attacker has access (only) to the system execution time. First, we address the following execution-time opacity problem: given a timed …

Machine Learning Approach To Activity Categorization In Young Adults Using Biomechanical Metrics, Nathan Q. C. Holland

Mechanical & Aerospace Engineering Theses & Dissertations

Inactive adults often have decreased musculoskeletal health and increased risk factors for chronic diseases. However, there is limited data linking biomechanical measurements of generally healthy young adults to their physical activity levels assessed through questionnaires. Commonly used data collection methods in biomechanics for assessing musculoskeletal health include but are not limited to muscle quality (measured as echo intensity when using ultrasound), isokinetic (i.e., dynamic) muscle strength, muscle activations, and functional movement assessments using motion capture systems. These assessments can be time consuming for both data collection and processing. Therefore, understanding if all biomechanical assessments are necessary to classify the activity …

Online Aircraft System Identification Using A Novel Parameter Informed Reinforcement Learning Method, Nathan Schaff

Doctoral Dissertations and Master's Theses

This thesis presents the development and analysis of a novel method for training reinforcement learning neural networks for online aircraft system identification of multiple similar linear systems, such as all fixed wing aircraft. This approach, termed Parameter Informed Reinforcement Learning (PIRL), dictates that reinforcement learning neural networks should be trained using input and output trajectory/history data as is convention; however, the PIRL method also includes any known and relevant aircraft parameters, such as airspeed, altitude, center of gravity location and/or others. Through this, the PIRL Agent is better suited to identify novel/test-set aircraft.

First, the PIRL method is applied to …

Sentiment Analysis Of Public Perception Towards Elon Musk On Reddit (2008-2022), Daniel Maya Bonilla, Samuel Iradukunda, Pamela Thomas

The Cardinal Edge

As Elon Musk’s influence in technology and business continues to expand, it becomes crucial to comprehend public sentiment surrounding him in order to gauge the impact of his actions and statements. In this study, we conducted a comprehensive analysis of comments from various subreddits discussing Elon Musk over a 14-year period, from 2008 to 2022. Utilizing advanced sentiment analysis models and natural language processing techniques, we examined patterns and shifts in public sentiment towards Musk, identifying correlations with key events in his life and career. Our findings reveal that public sentiment is shaped by a multitude of factors, including his …

Carbon-Aware Mine Planning With A Novel Multi-Objective Framework, Nurul Asyikeen Binte Azhar, Aldy Gunawan, Shih-Fen Cheng, Erwin Leonardi

Research Collection School Of Computing and Information Systems

The logistical complication of long-term mine planning involves deciding the sequential extraction of materials from the mine pit and their subsequent processing steps based on geological, geometrical, and resource constraints. The net present value (NPV) of profit over the mine's lifespan usually forms the sole objective for this problem, which is considered as the NP-hard precedence-constrained production scheduling problem (PCPSP) as well. However, increased pressure for more sustainable and carbon-aware industries also calls for environmental indicators to be considered. In this paper, we enhance the generic PCPSP formulation into a multi-objective optimization (MOO) problem whereby carbon cost forms an additional …

Uncertainty-Adjusted Inductive Matrix Completion With Graph Neural Networks, Petr Kasalicky, Antoine Ledent, Rodrigo Alves

Research Collection School Of Computing and Information Systems

We propose a robust recommender systems model which performs matrix completion and a ratings-wise uncertainty estimation jointly. Whilst the prediction module is purely based on an implicit low-rank assumption imposed via nuclear norm regularization, our loss function is augmented by an uncertainty estimation module which learns an anomaly score for each individual rating via a Graph Neural Network: data points deemed more anomalous by the GNN are downregulated in the loss function used to train the low-rank module. The whole model is trained in an end-to-end fashion, allowing the anomaly detection module to tap on the supervised information available in …

Grasp Solution Approach For The E-Waste Collection Problem, Aldy Gunawan, Dang Viet Anh Nguyen, Pham Kien Minh Nguyen, Pieter Vansteenwegen

Research Collection School Of Computing and Information Systems

The digital economy has brought significant advancements in electronic devices, increasing convenience and comfort in people’s lives. However, this progress has also led to a shorter life cycle for these devices due to rapid advancements in hardware and software technology. As a result, e-waste collection and recycling have become vital for protecting the environment and people’s health. From the operations research perspective, the e-waste collection problem can be modeled as the Heterogeneous Vehicle Routing Problem with Multiple Time Windows (HVRP-MTW). This study proposes a metaheuristic based on the Greedy Randomized Adaptive Search Procedure complemented by Path Relinking (GRASP-PR) to solve …

Quantifying Taxi Drivers' Behaviors With Behavioral Game Theory, Mengyu Ji, Yuhong Xu, Shih-Fen Cheng

Research Collection School Of Computing and Information Systems

With their flexibility and convenience, taxis play a vital role in urban transportation systems. Understanding how human drivers make decisions in a context of uncertainty and competition is crucial for taxi fleets that depend on drivers to provide their services. As part of this paper, we propose modeling taxi drivers’ behaviors based on behavioral game theory. Based on real-world data, we demonstrate that the behavioral game theory model we select is superior to state-of-the-art baselines. These results provide a solid foundation for improving taxi fleet efficiency in the future.

Threshold Attribute-Based Credentials With Redactable Signature, Rui Shi, Huamin Feng, Yang Yang, Feng Yuan, Yingjiu Li, Hwee Hwa Pang, Robert H. Deng

Research Collection School Of Computing and Information Systems

Threshold attribute-based credentials are suitable for decentralized systems such as blockchains as such systems generally assume that authenticity, confidentiality, and availability can still be guaranteed in the presence of a threshold number of dishonest or faulty nodes. Coconut (NDSS'19) was the first selective disclosure attribute-based credentials scheme supporting threshold issuance. However, it does not support threshold tracing of user identities and threshold revocation of user credentials, which is desired for internal governance such as identity management, data auditing, and accountability. The communication and computation complexities of Coconut for verifying credentials are linear in the number of each user's attributes and …

K-St: A Formal Executable Semantics Of The Structured Text Language For Plcs, Kun Wang, Jingyi Wang, Christopher M. Poskitt, Xiangxiang Chen, Jun Sun, Peng Cheng

Research Collection School Of Computing and Information Systems

Programmable Logic Controllers (PLCs) are responsible for automating process control in many industrial systems (e.g. in manufacturing and public infrastructure), and thus it is critical to ensure that they operate correctly and safely. The majority of PLCs are programmed in languages such as Structured Text (ST). However, a lack of formal semantics makes it difficult to ascertain the correctness of their translators and compilers, which vary from vendor-to-vendor. In this work, we develop K-ST, a formal executable semantics for ST in the K framework. Defined with respect to the IEC 61131-3 standard and PLC vendor manuals, K-ST is a high-level …

Models And Algorithms For Promoting Diverse And Fair Query Results, Md Mouinul Islam

Dissertations

Ensuring fairness and diversity in search results are two key concerns in compelling search and recommendation applications. This work explicitly studies these two aspects given multiple users' preferences as inputs, in an effort to create a single ranking or top-k result set that satisfies different fairness and diversity criteria. From group fairness standpoint, it adapts demographic parity like group fairness criteria and proposes new models that are suitable for ranking or producing top-k set of results. This dissertation also studies equitable exposure of individual search results in long tail data, a concept related to individual fairness. First, the dissertation focuses …