Theory and Algorithms Commons^™

The Autoproof Verifier: Usability By Non-Experts And On Standard Code, Carlo A. Furia, Christopher M. Poskitt, Julian Tschannen

Research Collection School Of Computing and Information Systems

Formal verification tools are often developed by experts for experts; as a result, their usability by programmers with little formal methods experience may be severely limited. In this paper, we discuss this general phenomenon with reference to AutoProof: a tool that can verify the full functional correctness of object-oriented software. In particular, we present our experiences of using AutoProof in two contrasting contexts representative of non-expert usage. First, we discuss its usability by students in a graduate course on software verification, who were tasked with verifying implementations of various sorting algorithms. Second, we evaluate its usability in verifying code developed …

Sails: Hybrid Algorithm For The Team Orienteering Problem With Time Windows, Aldy Gunawan, Hoong Chuin Lau, Kun Lu

Research Collection School Of Computing and Information Systems

The Team Orienteering Problem with Time Windows (TOPTW) is the extended version of the Orienteering Problem where each node is limited by a given time window. The objective is to maximize the total collected score from a certain number of paths. In this paper, a hybridization of Simulated Annealing and Iterated Local Search, namely SAILS, is proposed to solve the TOPTW. The efficacy of the proposed algorithm is tested using benchmark instances. The results show that the proposed algorithm is competitive with the state-of-the-art algorithms in the literature. SAILS is able to improve the best known solutions for 19 benchmark …

Inferring Interaction Type In Gene Regulatory Networks Using Co-Expression Data, Pegah Khosravi, Vahid H. Gazestani, Leila Pirhaji, Brian Law, Mehdi Sadeghi, Bahram Goliaei, Gary D. Bader

Publications and Research

Background

Knowledge of interaction types in biological networks is important for understanding the functional organization of the cell. Currently information-based approaches are widely used for inferring gene regulatory interactions from genomics data, such as gene expression profiles; however, these approaches do not provide evidence about the regulation type (positive or negative sign) of the interaction.

Results

This paper describes a novel algorithm, “Signing of Regulatory Networks” (SIREN), which can infer the regulatory type of interactions in a known gene regulatory network (GRN) given corresponding genome-wide gene expression data. To assess our new approach, we applied it to three different benchmark …

Message Passing For Collective Graphical Models, Tao Sun, Daniel Sheldon, Akshat Kumar

Research Collection School Of Computing and Information Systems

Collective graphical models (CGMs) are a formalism for inference and learning about a population of independent and identically distributed individuals when only noisy aggregate data are available. We highlight a close connection between approximate MAP inference in CGMs and marginal inference in standard graphical models. The connection leads us to derive a novel Belief Propagation (BP) style algorithm for collective graphical models. Mathematically, the algorithm is a strict generalization of BP—it can be viewed as an extension to minimize the Bethe free energy plus additional energy terms that are non-linear functions of the marginals. For CGMs, the algorithm is much …

State Preserving Extreme Learning Machine For Face Recognition, Md. Zahangir Alom, Paheding Sidike, Vijayan K. Asari, Tarek M. Taha

Electrical and Computer Engineering Faculty Publications

Extreme Learning Machine (ELM) has been introduced as a new algorithm for training single hidden layer feed-forward neural networks (SLFNs) instead of the classical gradient-based algorithms. Based on the consistency property of data, which enforce similar samples to share similar properties, ELM is a biologically inspired learning algorithm with SLFNs that learns much faster with good generalization and performs well in classification applications. However, the random generation of the weight matrix in current ELM based techniques leads to the possibility of unstable outputs in the learning and testing phases. Therefore, we present a novel approach for computing the weight matrix …

Automatic Video Self Modeling For Voice Disorder, Ju Shen, Changpeng Ti, Anusha Raghunathan, Sen-Ching S. Cheung, Rita Patel

Computer Science Faculty Publications

Video self modeling (VSM) is a behavioral intervention technique in which a learner models a target behavior by watching a video of him- or herself. In the field of speech language pathology, the approach of VSM has been successfully used for treatment of language in children with Autism and in individuals with fluency disorder of stuttering. Technical challenges remain in creating VSM contents that depict previously unseen behaviors. In this paper, we propose a novel system that synthesizes new video sequences for VSM treatment of patients with voice disorders. Starting with a video recording of a voice-disorder patient, the proposed …

Accuracy Comparison Of Numerical Integration Algorithms For Real-Time Hybrid Simulations, Ganesh Anant Reddy

Civil & Environmental Engineering Theses & Dissertations

The use of accurate numerical integration algorithms is one of the key factors for a successful real-time hybrid simulation (RTHS). In RTHSs, explicit integration algorithms are preferred more than implicit methods since all calculations need to be completed within a given time step during simulation. Explicit methods require the use of effective stiffness and damping for experimental substructures, which are incorporated into the calculation of the integration parameters. In general, those values that are greater than the expected stiffness and damping of the experimental substructure are used to ensure the stability of simulation. If a rate-dependent and nonlinear experimental substructure …

Object Tracking From Multiple Multi-Axis Platforms In Four Dimensions, Theodore A. Teates

Electrical & Computer Engineering Theses & Dissertations

Object handoff in free space requires a sound framework between at least two optical sensors and one object. Previous work developed an algorithm that can determine the ap­ propriate time to initiate handoff of object tracking responsibilities from one optical sensor with an object in view to another optical sensor with the same object in view. In order to maintain persistent tracking of objects in this work, gimbal movements of optical sensors are determined by calculations using the Lagrange method to determine the trackability measures between the moving object and the handoff cone for the appropriate optical sensor. The rotation …

Meta-Raps Hybridization With Machine Learning Algorithms, Fatemah Al-Duoli

Engineering Management & Systems Engineering Theses & Dissertations

This dissertation focuses on advancing the Metaheuristic for Randomized Priority Search algorithm, known as Meta-RaPS, by integrating it with machine learning algorithms. Introducing a new metaheuristic algorithm starts with demonstrating its performance. This is accomplished by using the new algorithm to solve various combinatorial optimization problems in their basic form. The next stage focuses on advancing the new algorithm by strengthening its relatively weaker characteristics. In the third traditional stage, the algorithms are exercised in solving more complex optimization problems. In the case of effective algorithms, the second and third stages can occur in parallel as researchers are eager to …

Solar: Scalable Online Learning Algorithms For Ranking, Jialei Wang, Ji Wan, Yongdong Zhang, Steven C. H. Hoi

Research Collection School Of Computing and Information Systems

Traditional learning to rank methods learn ranking models from training data in a batch and offline learning mode, which suffers from some critical limitations, e.g., poor scalability as the model has to be retrained from scratch whenever new training data arrives. This is clearly nonscalable for many real applications in practice where training data often arrives sequentially and frequently. To overcome the limitations, this paper presents SOLAR- a new framework of Scalable Online Learning Algorithms for Ranking, to tackle the challenge of scalable learning to rank. Specifically, we propose two novel SOLAR algorithms and analyze their IR measure bounds theoretically. …

Optimizing Selection Of Competing Features Via Feedback-Directed Evolutionary Algorithms, Tian Huat Tan, Yinxing Xue, Manman Chen, Jun Sun, Yang Liu, Jin Song Dong Dong

Research Collection School Of Computing and Information Systems

Software that support various groups of customers usually require complicated configurations to attain different functionalities. To model the configuration options, feature model is proposed to capture the commonalities and competing variabilities of the product variants in software family or Software Product Line (SPL). A key challenge for deriving a new product is to find a set of features that do not have inconsistencies or conflicts, yet optimize multiple objectives (e.g., minimizing cost and maximizing number of features), which are often competing with each other. Existing works have attempted to make use of evolutionary algorithms (EAs) to address this problem. In …

A Comparative Study Between Motivated Learning And Reinforcement Learning, James T. Graham, Janusz A. Starzyk, Zhen Ni, Haibo He, T.-H. Teng, Ah-Hwee Tan

Research Collection School Of Computing and Information Systems

This paper analyzes advanced reinforcement learning techniques and compares some of them to motivated learning. Motivated learning is briefly discussed indicating its relation to reinforcement learning. A black box scenario for comparative analysis of learning efficiency in autonomous agents is developed and described. This is used to analyze selected algorithms. Reported results demonstrate that in the selected category of problems, motivated learning outperformed all reinforcement learning algorithms we compared with.

Cooperative 3-D Map Generation Using Multiple Uavs, Andrew Erik Lawson

University Scholar Projects

This report aims to demonstrate the feasibility of building a global 3-D map from multiple UAV robots in a GPS-denied, indoor environment. Presented are the design of each robot and the reasoning behind choosing its hardware and software components, the process in which a single robot obtains a individual 3-D map entirely onboard, and lastly how the mapping concept is extended to multiple robotic agents to form a global 3-D map using a centralized server. In the latter section, this report focuses on two algorithms, Online Mapping and Map Fusion, developed to facilitate the cooperative approach. A limited selection …

Calculating Staircase Slope From A Single Image, Nicholas Joseph Clarke

Master's Theses

Realistic modeling of a 3D environment has grown in popularity due to the increasing realm of practical applications. Whether for practical navigation purposes, entertainment value, or architectural standardization, the ability to determine the dimensions of a room is becoming more and more important. One of the trickier, but critical, features within any multistory environment is the staircase. Staircases are difficult to model because of their uneven surface and various depth aspects. Coupling this need is a variety of ways to reach this goal. Unfortunately, many such methods rely upon specialized sensory equipment, multiple calibrated cameras, or other such impractical setups. …

Using Probabilistic Graphical Models To Solve Np-Complete Puzzle Problems, Fengjiao Wu

Master's Projects

Probabilistic Graphical Models (PGMs) are commonly used in machine learning to solve problems stemming from medicine, meteorology, speech recognition, image processing, intelligent tutoring, gambling, games, and biology. PGMs are applicable for both directed graph and undirected graph. In this work, I focus on the undirected graphical model. The objective of this work is to study how PGMs can be applied to find solutions to two puzzle problems, sudoku and jigsaw puzzles. First, both puzzle problems are represented as undirected graphs, and then I map the relations of nodes to PGMs and Belief Propagation (BP). This work represents the puzzle grid …

Trip: Tracking Rhythms In Plants, An Automated Leaf Movement Analysis Program For Circadian Period Estimation, Kathleen Greenham, Ping Lou, Sara E. Remsen, Hany Farid, C Robertson Mcclung

Dartmouth Scholarship

Background: A well characterized output of the circadian clock in plants is the daily rhythmic movement of leaves. This process has been used extensively in Arabidopsis to estimate circadian period in natural accessions as well as mutants with known defects in circadian clock function. Current methods for estimating circadian period by leaf movement involve manual steps throughout the analysis and are often limited to analyzing one leaf or cotyledon at a time.

Methods: In this study, we describe the development of TRiP (Tracking Rhythms in Plants), a new method for estimating circadian period using a motion estimation algorithm that can …

Compression Of Video Tracking And Bandwidth Balancing Routing In Wireless Multimedia Sensor Networks, Yin Wang, Jianjun Yang, Ju Shen, Bryson Payne, Juan Guo, Kun Hua

Computer Science Faculty Publications

There has been a tremendous growth in multimedia applications over wireless networks. Wireless Multimedia Sensor Networks(WMSNs) have become the premier choice in many research communities and industry. Many state-of-art applications, such as surveillance, traffic monitoring, and remote heath care are essentially video tracking and transmission in WMSNs. The transmission speed is constrained by the big file size of video data and fixed bandwidth allocation in constant routing paths. In this paper, we present a CamShift based algorithm to compress the tracking of videos. Then we propose a bandwidth balancing strategy in which each sensor node is able to dynamically select …

Optimal "Big Data" Aggregation Systems - From Theory To Practical Application, William J. Culhane Iv

Open Access Dissertations

The integration of computers into many facets of our lives has made the collection and storage of staggering amounts of data feasible. However, the data on its own is not so useful to us as the analysis and manipulation which allows manageable descriptive information to be extracted. New tools to extract this information from ever growing repositories of data are required.

Some of these analyses can take the form of a two phase problem which is easily distributed to take advantage of available computing power. The first phase involves computing some descriptive partial result from some subset of the original …

Efficient Estimation Of Cluster Population, Sanjeev K C

UNLV Theses, Dissertations, Professional Papers, and Capstones

Partitioning a given set of points into clusters is a well known problem in pattern recognition, data mining, and knowledge discovery. One of the well known methods for identifying clusters in Euclidean space is the K-mean algorithm. In using the K-mean clustering algorithm it is necessary to know the value of k (the number of clusters) in advance. We propose to develop algorithms for good estimation of k for points distributed in two dimensions. The techniques we pursue include a bucketing method, g-hop neighbors, and Voronoi diagrams. We also present experimental results for examining the performances of the bucketing method …

The Apprentices' Tower Of Hanoi, Cory Bh Ball

Electronic Theses and Dissertations

The Apprentices' Tower of Hanoi is introduced in this thesis. Several bounds are found in regards to optimal algorithms which solve the puzzle. Graph theoretic properties of the associated state graphs are explored. A brief summary of other Tower of Hanoi variants is also presented.