Theory and Practice of Computation

The following sections are included:

• PREFACE
• PROGRAM COMMITTEES
• CONTENTS

Sandal is a modeling language designed for specifying and model-checking fault-prone message-passing systems. The language supports the modular description of typical faults including unexpected termination of processes, random loss of messages and timeout. Thus on defining a model in Sandal, one does not need to write such faulty actions explicitly intermingled with the primary behaviors of the model. The compiler of the language automatically weaves them and produces a set of NuSMV modules. This paper describes how the weaving mechanism works and demonstrates the usefulness of the language using an example.

Functional aspects of the behavioral properties of systems are the main concern in formal verification. However, performance aspects of them are also important. LTL^mp is an LTL extension with expressions about mean-payoff. This logic expresses not only qualitative and functional properties of patterns of event occurrences but also quantitative properties of average performance, such as the long-run frequency of event occurrences. In this paper, we introduce an efficient procedure for LTL^mp satisfiability checking. The procedure consists of (1) parsing and normalizing a given LTL^mp formula, and transforming it into a combination of LTL parts and mean-payoff parts, (2) translating the LTL parts into transition-based generalized Büchi automata (TGBAs), (3) decomposing the automata into accepting strongly connected components (SCCs), (4) interpreting combinations of the mean-payoff parts and the SCCs into formulae of the quantifier-free linear real arithmetic (LRA) theory, and then (5) deciding the satisfiability of the LRA formulae and that of the given LTL^mp formula. We implemented the procedure and confirmed the effectiveness of our implementation through some experiments.

The remote procedure call (RPC) is a widely used technology for programming in distributed computation. Cooper and Wadler proposed the RPC calculus in order to model remote procedure calls. In object-oriented programming languages, the remote method invocation (RMI) is introduced as its variation. RMI calculus, proposed by Matsumoto and Nishizaki, is a formal system based on the sigma calculus which formulates prototype-based object-oriented programming language, incorporated with remote method invocations. Araki and Nishizaki proposed call-by-name evaluation strategies of RMI calculus and of RPC calculus and studied correspondence between the call-by-name evaluation strategies of the RMI and RPC calculi. In this paper, we give call-by-need evaluation strategies to RMI and RPC calculi, which are called lazy RMI and RPC calculi. We show the soundness property of lazy RMI calculus with respect to the lazy RPC calculus.

People engage in a variety of interaction in the society. To study the interaction, we see it as a game and people as agents equipped with reinforcement learning algorithms. However, existing algorithms have strong and weak points when dealing with games. In this work, we combined two complementary reinforcement learning algorithms to overcome the weakness. We constructed an algorithm that maximizes payoffs in various games. Our proposed algorithm combined two famous reinforcement algorithms, i.e., M-Qubed and Satisficing algorithm (S-alg), using the Boltzmann multiplication ensemble method. Experimental studies, in which the M-Qubed agent, the S-alg agent, and the proposed agent played ten kinds of games in self-play and in a round-robin fashion, show that the proposed algorithm can gain good payoffs in nine of them and the two internal algorithms compensate each other. Finally, we also confirmed that the learning speed of the proposed algorithm is faster than M-Qubed.

Adaptive computer gaming aims at increasing the player's entertainment by adjusting the game's content to the player's preferences. This work explores the possibility of using gameplay statistics (called game metrics) to classify players of a short self-made Japanese-style role-playing game (JRPG) into one of two classes, namely, Fighter and Explorer. This classification is used to select the final scene of the game in order to meet the player's preferences. During this work a data collection and a subsequent experiment to evaluate the classification performance were conducted. The trained SVM classifier was able to assign the correct class to 9 out of 14 participants but showed significant weaknesses in classifying the Fighter class. A detailed look at these results and a discussion about the possible reasons for the discovered difficulties will be presented at the end of this work.

Wireless sensor network (WSN) is a network of small embedded systems called nodes. These nodes gather data using various sensors to monitor an event; and wirelessly pass the data to a base station for analysis. Low Energy Adaptive Clustering Hierarchy (LEACH) is a hierarchical cluster-based routing algorithm for WSNs. LEACH groups the nodes into clusters, each having a randomly selected cluster-head that acts as the gateway for its cluster-members. Since the cluster-head selection is random, the selected clusterhead may not have enough energy compared to the other nodes or might be located poorly on the network. These instances can reduce the system lifetime of the WSN. This paper introduces ClusterNet, a modification of the LEACH routing algorithm that considers the residual energy and location of the node as a metric for choosing the cluster-heads to increase the system lifetime of the WSN.

A dataset is built into a model for the classification of OPM songs into ten specific genres. Low-level musical features in the form of digital signals, like Spectral Centroid, Mel-Frequency Cepstral Coefficients among others, were collected to build the data set. A collection of 1000 songs, having 100 in-stances as representatives for each of the 10 genres from songs sang and com-posed by Filipino artists were used as data for the features in building the model. Different classifiers where employed to test and see which musical features specific for Filipino music are highlighted and can be attributed for further study. A multi-layer perceptron was selected most optimal for the model building. Additional features, genres have yet to be incorporated into the study in order to produce a set of more well-refined results.

We propose a methodology to recognize human emotion by utilizing data from brainwave captured by electroencephalogram (EEG). In this research, music clips were used and 12 electrodes were placed near the frontal lobe of brain according to 10-20 International System. Fractal dimension values were calculated by Higuchi algorithm for constructing feature vectors. Then, features were labeled by time-vary self-annotated emotions by participants in 2-dimensional emotion model. Support vector machine (SVM) and multilayer perceptron (MLP) were applied to recognize arousal and valence separately. From 10-fold cross-validation testing, high/low arousal levels could be recognized with 85.92-89.14% average accuracy. Also we could classify positive/negative valence levels with 90.28-90.83% average accuracy. Additionally, using data from either familiar songs or unfamiliar songs could make classifiers perform 3-7% better than using the data from the combination of both. Therefore, using homogeneous sets of either familiar or unfamiliar songs is recommended for conducting EEG-based emotion recognition model.

Aerial Dynamic Assessment Robot for National Advancement (ADARNA) is a research program of the Computer Technology (CT) department of De La Salle University College of Computer Studies that aims to improve the country's disaster response capabilities. ADARNA utilizes radio-controlled helicopters instrumented with high-resolution cameras to see where stranded people and damaged structures are located. The helicopters are equipped with enhanced GPS for image tagging and navigation, and will be fully or partially computer controlled for stability and flight path. Important data is sent to other drones by finding the best path to reach the sink for processing to extract terrain/area features of interest. Since drones have limited data transmission range, the drones have to find a communication path to send the important data to the sink. The objective of this study was to provide a protocol for collecting these important data from the drones into a single sink. The Zewbat data collection protocol lessens the number of total packets sent and the power consumption of the drones. Zewbat piggybacks the data packets by combining multiple packets into a single data packet, which in turn helps with the reduction of the total packets sent. The downside in using Zewbat is there's a possibility of dropping a data packet that contains all the other piggybacked data from different drones.

With the recent availability of Doppler radars in the Philippines in recent years, some local groups have taken advantage of the data it provides to generate several new types of weather information, one of which is a new form of rainfall forecast in the country, called rapid rainfall forecasts or nowcasts. Based on ClimateX, one of the first few applications to utilize Doppler radar data, this study used both Doppler radar data and automatic weather station (AWS) data to generate probabilistic nowcasting models by using support vector machines (SVM). Data from 2012, March to 2013, December was used for the training and test dataset, with 80% of the data being used for training. As the only input, Doppler radar data were used to produce rainfall forecasts for each hour for the next four hours from the nowcasting models. The results from several forecast verification methods show that using machine learning to provide rainfall nowcasts is a viable option.

Ambient Intelligent Spaces are essentially environments which are aware of various phenomena and react automatically based on certain events; as such, construction, deployment, and management of these smart spaces is not an easy task due to its complexity, physical and technological limitations, cost effectiveness, and dynamic environment. The research aims to create a strategy to ease management by using an architecture that includes REST and a node configuration protocol.

The following sections is included:

• AUTHOR INDEX