Open Access. Powered by Scholars. Published by Universities.®

Physical Sciences and Mathematics Commons

Open Access. Powered by Scholars. Published by Universities.®

Articles 1 - 5 of 5

Full-Text Articles in Physical Sciences and Mathematics

Machine-Assisted Proof Support For Validation Beyond Simulink, Chunqing Chen, Jin Song Dong, Jun Sun Nov 2007

Machine-Assisted Proof Support For Validation Beyond Simulink, Chunqing Chen, Jin Song Dong, Jun Sun

Research Collection School Of Computing and Information Systems

Simulink is popular in industry for modeling and simulating embedded systems. It is deficient to handle requirements of high-level assurance and timing analysis. Previously, we showed the idea of applying Timed Interval Calculus (TIC) to complement Simulink. In this paper, we develop machine-assisted proof support for Simulink models represented in TIC. The work is based on a generic theorem prover, Prototype Verification System (PVS). The TIC specifications of both Simulink models and requirements are transformed to PVS specifications automatically. Verification can be carried out at interval level with a high level of automation. Analysis of continuous and discrete behaviors is …


Novelty Detection For Cross-Lingual News Stories With Visual Duplicates And Speech Transcripts, Xiao Wu, Alexander G. Hauptmann, Chong-Wah Ngo Sep 2007

Novelty Detection For Cross-Lingual News Stories With Visual Duplicates And Speech Transcripts, Xiao Wu, Alexander G. Hauptmann, Chong-Wah Ngo

Research Collection School Of Computing and Information Systems

An overwhelming volume of news videos from different channels and languages is available today, which demands automatic management of this abundant information. To effectively search, retrieve, browse and track cross-lingual news stories, a news story similarity measure plays a critical role in assessing the novelty and redundancy among them. In this paper, we explore the novelty and redundancy detection with visual duplicates and speech transcripts for cross-lingual news stories. News stories are represented by a sequence of keyframes in the visual track and a set of words extracted from speech transcript in the audio track. A major difference to pure …


Enhancing The Performance Of Semi-Supervised Classification Algorithms With Bridging, Jason Yuk Hin Chan, Josiah Poon, Irena Koprinska May 2007

Enhancing The Performance Of Semi-Supervised Classification Algorithms With Bridging, Jason Yuk Hin Chan, Josiah Poon, Irena Koprinska

Research Collection School Of Computing and Information Systems

Traditional supervised classification algorithms require a large number of labelled examples to perform accurately. Semi-supervised classification algorithms attempt to overcome this major limitation by also using unlabelled examples. Unlabelled examples have also been used to improve nearest neighbour text classification in a method called bridging. In this paper, we propose the use of bridging in a semi-supervised setting. We introduce a new bridging algorithm that can be used as a base classifier in any supervised approach such as co-training or selflearning. We empirically show that classification performance increases by improving the semi-supervised algorithm’s ability to correctly assign labels to previouslyunlabelled …


Solving The Teacher Assignment-Course Scheduling Problem By A Hybrid Algorithm, Aldy Gunawan, Kien Ming Ng, Kim Leng Poh Jan 2007

Solving The Teacher Assignment-Course Scheduling Problem By A Hybrid Algorithm, Aldy Gunawan, Kien Ming Ng, Kim Leng Poh

Research Collection School Of Computing and Information Systems

This paper presents a hybrid algorithm for solving atimetabling problem, which is commonly encountered in manyuniversities. The problem combines both teacher assignment andcourse scheduling problems simultaneously, and is presented as amathematical programming model. However, this problem becomesintractable and it is unlikely that a proven optimal solution can beobtained by an integer programming approach, especially for largeproblem instances. A hybrid algorithm that combines an integerprogramming approach, a greedy heuristic and a modified simulatedannealing algorithm collaboratively is proposed to solve the problem.Several randomly generated data sets of sizes comparable to that ofan institution in Indonesia are solved using the proposed algorithm.Computational results …


An Improvement Heuristic For The Timetabling Problem, Aldy Gunawan, Kien Ming Ng, Kim Leng Poh Jan 2007

An Improvement Heuristic For The Timetabling Problem, Aldy Gunawan, Kien Ming Ng, Kim Leng Poh

Research Collection School Of Computing and Information Systems

This paper formulates a timetabling problem, which is often encountered in a university, as a mathematical programming model. The proposed model combines both teacher assignment and course scheduling problems simultaneously, which causes the entire model to become more complex. We propose an improvement heuristic algorithm to solve such a model. The proposed algorithm has been tested with several randomly generated datasets of sizes that are comparable to those occurring in a university in Indonesia. The computational results show that the improvement heuristic is not only able to obtain good solutions, but is also able to do so within reasonable computational …