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

Computer Sciences Commons™

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

Singapore Management University

Discipline
Keyword
Publication Year
Publication
Publication Type
File Type

Articles 7201 - 7230 of 9003

Full-Text Articles in Computer Sciences

Defending Against Cross Site Scripting Attacks, Lwin Khin Shar, Hee Beng Kuan Tan Aug 2011

Defending Against Cross Site Scripting Attacks, Lwin Khin Shar, Hee Beng Kuan Tan

Research Collection School Of Computing and Information Systems

Researchers have proposed multiple solutions to cross-site scripting, but vulnerabilities continue to exist in many Web applications due to developers' lack of understanding of the problem and their unfamiliarity with current defenses' strengths and limitations.

Go to article

Finding Robust-Under-Risk Solutions For Flowshop Scheduling, Steven O. Kimbrough, Ann Kuo, Hoong Chuin Lau Jul 2011

Finding Robust-Under-Risk Solutions For Flowshop Scheduling, Steven O. Kimbrough, Ann Kuo, Hoong Chuin Lau

Research Collection School Of Computing and Information Systems

We propose and explore, in the context of benchmark problems for flowshop scheduling, a risk-based concept of robustness for optimization problems. This risk-based concept is in distinction to, and complements, the uncertainty-based concept employed in the field known as robust optimization. Implementation of our concept requires problem solution methods that sample the solution space intelligently and that produce large numbers of distinct sample points. With these solutions to hand, their robustness scores are easily obtained and heuristically robust solutions found. We find evolutionary computation to be effective for this purpose on these problems.

Go to article

Relevant Knowledge Helps In Choosing Right Teacher: Active Query Selection For Ranking Adaptation, Peng Cai, Wei Gao, Kam-Fai Wong, Aoying Zhou Jul 2011

Relevant Knowledge Helps In Choosing Right Teacher: Active Query Selection For Ranking Adaptation, Peng Cai, Wei Gao, Kam-Fai Wong, Aoying Zhou

Research Collection School Of Computing and Information Systems

Learning to adapt in a new setting is a common challenge to our knowledge and capability. New life would be easier if we actively pursued supervision from the right mentor chosen with our relevant but limited prior knowledge. This variant principle of active learning seems intuitively useful to many domain adaptation problems. In this paper, we substantiate its power for advancing automatic ranking adaptation, which is important in web search since it's prohibitive to gather enough labeled data for every search domain for fully training domain-specific rankers. For the cost-effectiveness, it is expected that only those most informative instances in …

Go to article

Effects Of Mentoring On Player Performance In Massively Multiplayer Online Role-Playing Games (Mmorpgs), Kyong Jin Shim, Kuo-Wei Hsu, Jaideep Srivastava Jul 2011

Effects Of Mentoring On Player Performance In Massively Multiplayer Online Role-Playing Games (Mmorpgs), Kyong Jin Shim, Kuo-Wei Hsu, Jaideep Srivastava

Research Collection School Of Computing and Information Systems

Massively Multiplayer Online Role-Playing Games (MMORPGs) have become increasingly popular and have communities comprising millions of subscribers. With their increasing popularity, researchers are realizing that video games can be a means to fully observe an entire isolated universe. In this study, we examine and report our findings on the effects of mentoring activities on player performance in Ever Quest II, a popular MMORPG developed by Sony Online Entertainment.

Go to article

Cryptanalysis Of Hsiang-Shih's Authentication Scheme For Multi-Server Architecture, Kuo-Hui Yeh, Nai-Wei Lo, Yingjiu Li Jul 2011

Cryptanalysis Of Hsiang-Shih's Authentication Scheme For Multi-Server Architecture, Kuo-Hui Yeh, Nai-Wei Lo, Yingjiu Li

Research Collection School Of Computing and Information Systems

From user point of view, password-based remote user authentication technique is one of the most convenient and easy-to-use mechanisms to provide necessary security on system access. As the number of computer crimes in modern cyberspace has increased dramatically, the robustness of password-based authentication schemes has been investigated by industries and organizations in recent years. In this paper, a well-designed password-based authentication protocol for multi-server communication environment, introduced by Hsiang and Shih, is evaluated. Our security analysis indicates that their scheme is insecure against session key disclosure, server spoofing attack, and replay attack and behavior denial.

Go to article

Heuristic Algorithms For Balanced Multi-Way Number Partitioning, Jilian Zhang, Kyriakos Mouratidis, Hwee Hwa Pang Jul 2011

Heuristic Algorithms For Balanced Multi-Way Number Partitioning, Jilian Zhang, Kyriakos Mouratidis, Hwee Hwa Pang

Research Collection School Of Computing and Information Systems

Balanced multi-way number partitioning (BMNP) seeks to split a collection of numbers into subsets with (roughly) the same cardinality and subset sum. The problem is NP-hard, and there are several exact and approximate algorithms for it. However, existing exact algorithms solve only the simpler, balanced two-way number partitioning variant, whereas the most effective approximate algorithm, BLDM, may produce widely varying subset sums. In this paper, we introduce the LRM algorithm that lowers the expected spread in subset sums to one third that of BLDM for uniformly distributed numbers and odd subset cardinalities. We also propose Meld, a novel strategy for …

Go to article

Trust Network Inference For Online Rating Data Using Generative Models, Freddy Tat Chua Chua, Ee Peng Lim Jul 2011

Trust Network Inference For Online Rating Data Using Generative Models, Freddy Tat Chua Chua, Ee Peng Lim

Research Collection School Of Computing and Information Systems

In an online rating system, raters assign ratings to objects contributed by other users. In addition, raters can develop trust and distrust on object contributors depending on a few rating and trust related factors. Previous study has shown that ratings and trust links can influence each other but there has been a lack of a formal model to relate these factors together. In this paper, we therefore propose Trust Antecedent Factor (TAF)Model, a novel probabilistic model that generate ratings based on a number of rater’s and contributor’s factors. We demonstrate that parameters of the model can be learnt by Collapsed …

Go to article

A Hybrid Agent Architecture Integrating Desire, Intention And Reinforcement Learning, Ah-Hwee Tan, Yew-Soon Ong, Akejariyawong Tapanuj Jul 2011

A Hybrid Agent Architecture Integrating Desire, Intention And Reinforcement Learning, Ah-Hwee Tan, Yew-Soon Ong, Akejariyawong Tapanuj

Research Collection School Of Computing and Information Systems

This paper presents a hybrid agent architecture that integrates the behaviours of BDI agents, specifically desire and intention, with a neural network based reinforcement learner known as Temporal DifferenceFusion Architecture for Learning and COgNition (TD-FALCON). With the explicit maintenance of goals, the agent performs reinforcement learning with the awareness of its objectives instead of relying on external reinforcement signals. More importantly, the intention module equips the hybrid architecture with deliberative planning capabilities, enabling the agent to purposefully maintain an agenda of actions to perform and reducing the need of constantly sensing the environment. Through reinforcement learning, plans can also be …

Go to article

Real-World Parameter Tuning Using Factorial Design With Parameter Decomposition, Aldy Gunawan, Hoong Chuin Lau, Elaine Wong Jul 2011

Real-World Parameter Tuning Using Factorial Design With Parameter Decomposition, Aldy Gunawan, Hoong Chuin Lau, Elaine Wong

Research Collection School Of Computing and Information Systems

In this paper, we explore the idea of improving the efficiency of factorial design for parameter tuning of metaheuristics. In a standard full factorial design, the number of runs increases exponentially as the number of parameters. To reduce the parameter search space, one option is to first partition parameters into disjoint categories. While this may be done manually based on user guidance, an automated approach proposed in this paper is to apply a fractional factorial design to partition parameters based on their main effects where each partition is then tuned independently. With a careful choice of fractional design, our approach …

Go to article

Generating Aspect-Oriented Multi-Document Summarization With Event-Aspect Model, Peng Li, Yinglin Wang, Wei Gao, Jing Jiang Jul 2011

Generating Aspect-Oriented Multi-Document Summarization With Event-Aspect Model, Peng Li, Yinglin Wang, Wei Gao, Jing Jiang

Research Collection School Of Computing and Information Systems

In this paper, we propose a novel approach to automatic generation of aspect-oriented summaries from multiple documents. We first develop an event-aspect LDA model to cluster sentences into aspects. We then use extended LexRank algorithm to rank the sentences in each cluster. We use Integer Linear Programming for sentence selection. Key features of our method include automatic grouping of semantically related sentences and sentence ranking based on extension of random walk model. Also, we implement a new sentence compression algorithm which use dependency tree instead of parser tree. We compare our method with four baseline methods. Quantitative evaluation based on …

Go to article

Online Auc Maximization, Peilin Zhao, Steven C. H. Hoi, Rong Jin, Tianbo Yang Jul 2011

Online Auc Maximization, Peilin Zhao, Steven C. H. Hoi, Rong Jin, Tianbo Yang

Research Collection School Of Computing and Information Systems

Most studies of online learning measure the performance of a learner by classification accuracy, which is inappropriate for applications where the data are unevenly distributed among different classes. We address this limitation by developing online learning algorithm for maximizing Area Under the ROC curve (AUC), a metric that is widely used for measuring the classification performance for imbalanced data distributions. The key challenge of online AUC maximization is that it needs to optimize the pairwise loss between two instances from different classes. This is in contrast to the classical setup of online learning where the overall loss is a sum …

Go to article

Mining Weakly Labeled Web Facial Images For Search-Based Face Annotation, Dayang Wang, Steven C. H. Hoi, Ying He Jul 2011

Mining Weakly Labeled Web Facial Images For Search-Based Face Annotation, Dayang Wang, Steven C. H. Hoi, Ying He

Research Collection School Of Computing and Information Systems

In this paper, we investigate a search-based face annotation framework by mining weakly labeled facial images that are freely available on the internet. A key component of such a search-based annotation paradigm is to build a database of facial images with accurate labels. This is however challenging since facial images on the WWW are often noisy and incomplete. To improve the label quality of raw web facial images, we propose an effective Unsupervised Label Refinement (ULR) approach for refining the labels of web facial images by exploring machine learning techniques. We develop effective optimization algorithms to solve the large-scale learning …

Go to article

Solution Pluralism And Metaheuristics, Steven O. Kimbrough, Ann Kuo, Hoong Chuin Lau, Frederic H. Murphy, David Harlan Wood Jul 2011

Solution Pluralism And Metaheuristics, Steven O. Kimbrough, Ann Kuo, Hoong Chuin Lau, Frederic H. Murphy, David Harlan Wood

Research Collection School Of Computing and Information Systems

Solution pluralism is an approach to problem solving and deliberation. It employs a plurality of distinct solutions for a decision problem for aiding decision making. The concept is well established in existing practice, although perhaps not recognized as such. This paper: (1) presents the concept as a generalization of established practice, (2) briefly describes successful uses of the concept in practice, and (3) presents several areas that appear would benefit from application of the concept. Throughout, the role of metaheuristics in finding the pluralities of solutions is emphasized.

Go to article

Parallel Learning To Rank For Information Retrieval, Shuaiqiang Wang, Byron J. Gao, Ke Wang, Hady W. Lauw Jul 2011

Parallel Learning To Rank For Information Retrieval, Shuaiqiang Wang, Byron J. Gao, Ke Wang, Hady W. Lauw

Research Collection School Of Computing and Information Systems

Learning to rank represents a category of effective ranking methods for information retrieval. While the primary concern of existing research has been accuracy, learning efficiency is becoming an important issue due to the unprecedented availability of large-scale training data and the need for continuous update of ranking functions. In this paper, we investigate parallel learning to rank, targeting simultaneous improvement in accuracy and efficiency.

Go to article

Scalable Multiagent Planning Using Probabilistic Inference, Akshat Kumar, Shlomo Zilberstein, Marc Toussaint Jul 2011

Scalable Multiagent Planning Using Probabilistic Inference, Akshat Kumar, Shlomo Zilberstein, Marc Toussaint

Research Collection School Of Computing and Information Systems

Multiagent planning has seen much progress with the development of formal models such as Dec-POMDPs. However, the complexity of these models -- NEXP-Complete even for two agents -- has limited scalability. We identify certain mild conditions that are sufficient to make multiagent planning amenable to a scalable approximation w.r.t. the number of agents. This is achieved by constructing a graphical model in which likelihood maximization is equivalent to plan optimization. Using the Expectation-Maximization framework for likelihood maximization, we show that the necessary inference can be decomposed into processes that often involve a small subset of agents, thereby facilitating scalability. We …

Go to article

Message-Passing Algorithms For Quadratic Programming Formulations Of Map Estimation, Akshat Kumar, Shlomo Zilberstein Jul 2011

Message-Passing Algorithms For Quadratic Programming Formulations Of Map Estimation, Akshat Kumar, Shlomo Zilberstein

Research Collection School Of Computing and Information Systems

Computing maximum a posteriori (MAP) estimation in graphical models is an important inference problem with many applications. We present message-passing algorithms for quadratic programming (QP) formulations of MAP estimation for pairwise Markov random fields. In particular, we use the concave-convex procedure (CCCP) to obtain a locally optimal algorithm for the non-convex QP formulation. A similar technique is used to derive a globally convergent algorithm for the convex QP relaxation of MAP. We also show that a recently developed expectation-maximization (EM) algorithm for the QP formulation of MAP can be derived from the CCCP perspective. Experiments on synthetic and real-world problems …

Go to article

Unsupervised Discovery Of Discourse Relations For Eliminating Intra-Sentence Polarity Ambiguities, Lanjun Zhou, Binyang Li, Wei Gao, Zhongyu Wei, Kam-Fai Wong Jul 2011

Unsupervised Discovery Of Discourse Relations For Eliminating Intra-Sentence Polarity Ambiguities, Lanjun Zhou, Binyang Li, Wei Gao, Zhongyu Wei, Kam-Fai Wong

Research Collection School Of Computing and Information Systems

Polarity classification of opinionated sentences with both positive and negative sentiments1 is a key challenge in sentiment analysis. This paper presents a novel unsupervised method for discovering intra-sentence level discourse relations for eliminating polarity ambiguities. Firstly, a discourse scheme with discourse constraints on polarity was defined empirically based on Rhetorical Structure Theory (RST). Then, a small set of cuephrase-based patterns were utilized to collect a large number of discourse instances which were later converted to semantic sequential representations (SSRs). Finally, an unsupervised method was adopted to generate, weigh and filter new SSRs without cue phrases for recognizing discourse relations. Experimental …

Go to article

Unsupervised Information Extraction With Distributional Prior Knowledge, Cane Wing-Ki Leung, Jing Jiang, Kian Ming A. Chai, Hai Leong Chieu, Loo-Nin Teow Jul 2011

Unsupervised Information Extraction With Distributional Prior Knowledge, Cane Wing-Ki Leung, Jing Jiang, Kian Ming A. Chai, Hai Leong Chieu, Loo-Nin Teow

Research Collection School Of Computing and Information Systems

We address the task of automatic discovery of information extraction template from a given text collection. Our approach clusters candidate slot fillers to identify meaningful template slots. We propose a generative model that incorporates distributional prior knowledge to help distribute candidates in a document into appropriate slots. Empirical results suggest that the proposed prior can bring substantial improvements to our task as compared to a K-means baseline and a Gaussian mixture model baseline. Specifically, the proposed prior has shown to be effective when coupled with discriminative features of the candidates.

Go to article

Linking Entities To A Knowledge Base With Query Expansion, Swapna Gottipati, Jing Jiang Jul 2011

Linking Entities To A Knowledge Base With Query Expansion, Swapna Gottipati, Jing Jiang

Research Collection School Of Computing and Information Systems

In this paper we present a novel approach to entity linking based on a statistical language model-based information retrieval with query expansion. We use both local contexts and global world knowledge to expand query language models. We place a strong emphasis on named entities in the local contexts and explore a positional language model to weigh them differently based on their distances to the query. Our experiments on the TAC-KBP 2010 data show that incorporating such contextual information indeed aids in disambiguating the named entities and consistently improves the entity linking performance. Compared with the official results from KBP 2010 …

Go to article

Generating Aspect-Oriented Multi-Document Summarization With Event-Aspect Model, Peng Li, Yinglin Wang, Wei Gao, Jing Jiang Jul 2011

Generating Aspect-Oriented Multi-Document Summarization With Event-Aspect Model, Peng Li, Yinglin Wang, Wei Gao, Jing Jiang

Research Collection School Of Computing and Information Systems

In this paper, we propose a novel approach to automatic generation of aspect-oriented summaries from multiple documents. We first develop an event-aspect LDA model to cluster sentences into aspects. We then use extended LexRank algorithm to rank the sentences in each cluster. We use Integer Linear Programming for sentence selection. Key features of our method include automatic grouping of semantically related sentences and sentence ranking based on extension of random walk model. Also, we implement a new sentence compression algorithm which use dependency tree instead of parser tree. We compare our method with four baseline methods. Quantitative evaluation based on …

Go to article

Automated Detection Of Likely Design Flaws In Layered Architectures, Aditya Budi, - Lucia, David Lo, Lingxiao Jiang, Shaowei Wang Jul 2011

Automated Detection Of Likely Design Flaws In Layered Architectures, Aditya Budi, - Lucia, David Lo, Lingxiao Jiang, Shaowei Wang

Research Collection School Of Computing and Information Systems

Layered architecture prescribes a good principle for separating concerns to make systems more maintainable. One example of such layered architectures is the separation of classes into three groups: Boundary, Control, and Entity, which are referred to as the three analysis class stereotypes in UML. Classes of different stereotypes are interacting with one another, when properly designed, the overall interaction would be maintainable, flexible, and robust. On the other hand, poor design would result in less maintainable system that is prone to errors. In many software projects, the stereotypes of classes are often missing, thus detection of design flaws becomes non-trivial. …

Go to article

Kb-Anonymity: A Model For Anonymized Behavior-Preserving Test And Debugging Data, Aditya Budi, David Lo, Lingxiao Jiang, Lucia Lucia Jun 2011

Kb-Anonymity: A Model For Anonymized Behavior-Preserving Test And Debugging Data, Aditya Budi, David Lo, Lingxiao Jiang, Lucia Lucia

Research Collection School Of Computing and Information Systems

It is often very expensive and practically infeasible to generate test cases that can exercise all possible program states in a program. This is especially true for a medium or large industrial system. In practice, industrial clients of the system often have a set of input data collected either before the system is built or after the deployment of a previous version of the system. Such data are highly valuable as they represent the operations that matter in a client's daily business and may be used to extensively test the system. However, such data often carries sensitive information and cannot …

Go to article

Continuous Visible Nearest Neighbor Query Processing In Spatial Databases, Yunjun Gao, Baihua Zheng, Gencai Chen, Qing Li, Xiaofa Guo Jun 2011

Continuous Visible Nearest Neighbor Query Processing In Spatial Databases, Yunjun Gao, Baihua Zheng, Gencai Chen, Qing Li, Xiaofa Guo

Research Collection School Of Computing and Information Systems

In this paper, we identify and solve a new type of spatial queries, called continuous visible nearest neighbor (CVNN) search. Given a data set P, an obstacle set O, and a query line segment q in a two-dimensional space, a CVNN query returns a set of $${\langle p, R\rangle}$$ tuples such that $${p \in P}$$ is the nearest neighbor to every point r along the interval $${R \subseteq q}$$ as well as pis visible to r. Note that p may be NULL, meaning that all points in P are invisible to all points in R due to the obstruction of …

Go to article

Real-Time Trip Information Service For A Large Taxi Fleet, Rajesh Krishna Balan, Nguyen Xuan Khoa, Lingxiao Jiang Jun 2011

Real-Time Trip Information Service For A Large Taxi Fleet, Rajesh Krishna Balan, Nguyen Xuan Khoa, Lingxiao Jiang

Research Collection School Of Computing and Information Systems

In this paper, we describe the design, analysis, implementation, and operational deployment of a real-time trip information system that provides passengers with the expected fare and trip duration of the taxi ride they are planning to take. This system was built in cooperation with a taxi operator that operates more than 15,000 taxis in Singapore. We first describe the overall system design and then explain the efficient algorithms used to achieve our predictions based on up to 21 months of historical data consisting of approximately 250 million paid taxi trips. We then describe various optimisations (involving region sizes, amount of …

Go to article

Link Type Based Pre-Cluster Pair Model For Coreference Resolution, Yang Song, Houfeng Wang, Jing Jiang Jun 2011

Link Type Based Pre-Cluster Pair Model For Coreference Resolution, Yang Song, Houfeng Wang, Jing Jiang

Research Collection School Of Computing and Information Systems

This paper presents our participation in the CoNLL-2011 shared task, Modeling Unrestricted Coreference in OntoNotes. Coreference resolution, as a difficult and challenging problem in NLP, has attracted a lot of attention in the research community for a long time. Its objective is to determine whether two mentions in a piece of text refer to the same entity. In our system, we implement mention detection and coreference resolution seperately. For mention detection, a simple classification based method combined with several effective features is developed. For coreference resolution, we propose a link type based pre-cluster pair model. In this model, pre-clustering of …

Go to article

Optimizing Sensor Data Acquisition For Energy-Efficient Smartphone-Based Continuous Event Processing, Archan Misra, Lipyeow Lim Jun 2011

Optimizing Sensor Data Acquisition For Energy-Efficient Smartphone-Based Continuous Event Processing, Archan Misra, Lipyeow Lim

Research Collection School Of Computing and Information Systems

Many pervasive applications, such as activity recognition or remote wellness monitoring, utilize a personal mobile device (aka smartphone) to perform continuous processing of data streams acquired from locally-connected, wearable, sensors. To ensure the continuous operation of such applications on a battery-limited mobile device, it is essential to dramatically reduce the energy overhead associated with the process of sensor data acquisition and processing. To achieve this goal, this paper introduces a technique of "acquisition-cost" aware continuous query processing, as part of the Acquisition Cost-Aware Query Adaptation (ACQUA) framework. ACQUA replaces the current paradigm, where the data is typically streamed (pushed) from …

Go to article

Topical Keyphrase Extraction From Twitter, Xin Zhao, Jing Jiang, Jing He, Yang Song, Palakorn Achananuparp, Ee Peng Lim, Xiaoming Li Jun 2011

Topical Keyphrase Extraction From Twitter, Xin Zhao, Jing Jiang, Jing He, Yang Song, Palakorn Achananuparp, Ee Peng Lim, Xiaoming Li

Research Collection School Of Computing and Information Systems

Summarizing and analyzing Twitter content is an important and challenging task. In this paper, we propose to extract topical keyphrases as one way to summarize Twitter. We propose a context-sensitive topical PageRank method for keyword ranking and a probabilistic scoring function that considers both relevance and interestingness of keyphrases for keyphrase ranking. We evaluate our proposed methods on a large Twitter data set. Experiments show that these methods are very effective for topical keyphrase extraction.

Go to article

Preserving Transparency And Accountability In Optimistic Fair Exchange Of Digital Signatures, Xinyi Huang, Yi Mu, Willy Susilo, Jianying Zhou, Robert H. Deng Jun 2011

Preserving Transparency And Accountability In Optimistic Fair Exchange Of Digital Signatures, Xinyi Huang, Yi Mu, Willy Susilo, Jianying Zhou, Robert H. Deng

Research Collection School Of Computing and Information Systems

Optimistic fair exchange (OFE) protocols are useful tools for two participants to fairly exchange items with the aid of a third party who is only involved if needed. A widely accepted requirement is that the third party's involvement in the exchange must be transparent, to protect privacy and avoid bad publicity. At the same time, a dishonest third party would compromise the fairness of the exchange and the third party thus must be responsible for its behaviors. This is achieved in OFE protocols with another property called accountability. It is unfortunate that the accountability has never been formally studied in …

Go to article

A Solution With Security Concern For Rfid-Based Track And Trace Services In Epcglobal-Enabled Supply Chains, Wei He, Yingjiu Li, Kevin Chiew, Tieyan Li, Eng Wah Lee Jun 2011

A Solution With Security Concern For Rfid-Based Track And Trace Services In Epcglobal-Enabled Supply Chains, Wei He, Yingjiu Li, Kevin Chiew, Tieyan Li, Eng Wah Lee

Research Collection School Of Computing and Information Systems

A supply chain represents the flow of materials, information, and finance as they move through supply chain partners such as manufacturers, suppliers, distributors, retailers, and consumers. The track & trace services in supply chains can help improve supply chain visibility and efficiency, and prevent counterfeiting and stealing of products thus enhance security. Track & trace services in supply chains require identification of items, capture of events as items move through supply chains, and query of events of items. RFID (radio frequency identification) is a technology that allows to identify objects simultaneously in a fully automated manner via radio waves. This …

Go to article

On Combining State Space Reductions With Global Fairness Assumptions, Shao Jie Zhang, Jun Sun, Jun Pang, Yang Liu, Jin Song Dong Jun 2011

On Combining State Space Reductions With Global Fairness Assumptions, Shao Jie Zhang, Jun Sun, Jun Pang, Yang Liu, Jin Song Dong

Research Collection School Of Computing and Information Systems

Model checking has established itself as an effective system analysis method, as it is capable of proving/dis-proving properties automatically. Its application to practical systems is however limited by state space explosion. Among effective state reduction techniques are symmetry reduction and partial order reduction. Global fairness often plays a vital role in designing self-stabilizing population protocols. It is known that combining fairness and symmetry reduction is nontrivial. In this work, we first show that global fairness, unlike weak/strong fairness, can be combined with symmetry reduction. We extend the PAT model checker with the technique and demonstrate its usability by verifying recently …

Go to article

First Prev Next Last