Theory and Practice of Computation

The following sections are included:

• CONTENTS
• PREFACE
• Organizing Committee

Object-oriented programming is one of the fundamental notions in every phase of software development. Several kinds of theoretical frameworks for formalizing object-oriented programming languages have been proposed. The object calculus, proposed by Abadi and Cardelli, formulates various styles of object-oriented programming languages such as prototype-based and class-based programming languages. The sigma calculus is the simplest among the various systems of object calculus.

Distributed computation is a fundamental technology in information technology. The remote procedure call (RPC) is a widely used technology for programming in distributed computation. The remote procedure call is known as the remote method invocation in object-oriented programming. Cooper and Wadler proposed the RPC calculus, which is a formal system for modeling remote procedure calls.

Matumoto and Nishizaki proposed the RMI calculus, which is based on the sigma calculus and incorporated with remote method invocations. In their work, they studied the relationship between the RPC and RMI calculi. They found a correspondence between all-by-value evaluations of the two calculi. In this paper, we investigate call-by-name evaluation for the calculi.

Spiking Neural P Systems (SNP systems in short) are Turing complete computing models inspired by biological spiking neurons. In this work we relate SNP Systems with delay and those without delay using SNP algebra, a type of process algebra specifically for SNP systems. Given an initial configuration where only the initial neuron(s) fires a spike, i.e. the first set of neuron(s) to fire, we focus on four SNP system modules performing four spike routings: sequential, join, split, and iteration. We show that there exist bisimulations between the respective four modules of SNP systems with delays and the four modules without delays. We then use these modules (both with and without delays) to create larger SNP systems such that bisimulations also exist between them.

We present a polynomial-time transformation of the input for a variant of Median String Problem (MSP) that employs Hamming distance into the input for Approximate Gene Cluster Discovery Problem (AGCDP). Since MSP is NP-complete, the transformation forms the integral part of the reduction of MSP into AGCDP, for all input instances, such that AGCDP is confirmed to be NP-hard.

In this paper, we show that the two biogeochemical processes, carbon and nitrogen cycles are weakly bisimilar or weakly equivalent. We model each process as labeled transition system (LTS), where transitions between Carbon and Nitrogen states are movements from different compartment of Earth. We showed that there exist a binary relation over the states of the two systems, such that one weakly simulates the other with respect to their changes in location.

Two of the general families of membrane systems in Membrane computing are cell-like and neural-like systems. Transition P systems or TP systems and Spiking Neural P systems or SNP systems are part of the cell-like and neural-like families, respectively. In this work we provide a relation between TP systems with noncooperative rules or nTP systems and SNP systems with weighted synapses or wSNP systems (both are synchronous and nondeterministic). In particular we define a reasonable operating mode of nTP systems we refer to as k-restricted object-minimal region-maximal parallelism or k-O_min, R_max mode. We show that there exists a simulation of nTP systems operating in 1-O_min, R_max mode with wSNP systems. Remarks for further study of cell-like and neural-like relations are also provided.

In this study, we propose a formal approach for the analysis of robustness with regard to human-made faults in procedural manuals. In many cases, fault detection and recovery tasks are embedded in procedural manuals that allow us to detect human-made faults. This investigation is important in preserving the trust of workflows in safety critical domains. We define the formal semantics of human-made faults according to Discrete Action Classification, which classifies fault actions of experts in a domain — the formal definition of the faults is based on a transition system. Using these semantics, we inject faults into a fault-free model of a procedural manual. After that, we verify that the model embedded with faulty tasks satisfies a property as the goal of a procedural manual by model checking. A model checking tool is given the opposite of the formula as a goal, and if this tool reports counter examples, we say that the procedural manual is not robust. We apply our framework to a procedural manual that a nurse executes for taking blood samples. In the case, we conclude that the procedural manual is not robust because that tool reports counter examples.

This work is an attempt to construct a new group-wide meta-level architecture based on the Actor model. The overall goal is to establish a solid semantic basis for reflection in concurrent systems. The main idea presented in this paper is a constraint-based abstract specification of meta-level actors. The proposed method provides a general model of group-wide reflection and results in a clearer semantics.

The TALA Empathic Space is a physical, computing space that contains modules and sensors which recognizes the feelings of its occupant and responds to it by deploying changes in the environment. The space is composed of different modules and devices that collect and process data for it to be able to adapt by providing changes on the ambient settings. The COSMOS protocol provides a way on how devices and applications communicate and transfer data between devices in the empathic space. The protocol also provides an organized method for storing and accessing distributed data. Moreover, the empathic space also contains nodes which are devices or applications connected to a network and capable of sending and receiving data. COSMOS defines generic object called cosmos object, which is used to send commands and data for node to node communication and accessing data readily available on the network. COSMOS also provides an Application Programming Interface (API) that enables the user to device functions and commands for nodes usage and data acquisition and reception. With the growing devices and numerous data within the TALA Empathic Space, a user needs a convenient way to observe processes and outputs and manage the tools within the space. With the use of the COSMOS API, developers can create applications or systems that can control and manage the on-going transactions between devices and data in the empathic space. A dashboard system is capable of managing the device and gathering multiple, simultaneous data within the space. The TALA Dashbaord (TADa) is developed using the COSMOS API to provide users a manageable interface in accessing the devices and data available in the empathic space. The TADa system aims to provide different type of users - the Administrator who is able to control all devices, the Concierge to stream data, and the User who can simply view information — the system is able to adjust its accessibility per user.

We describe an object-oriented language, called T, for reactive system specifications based on linear temporal logic (LTL). Because the language is object-oriented, the specifications can be modular, and the modules are related by “is-a” and “has-a” relations. Furthermore, we can use parameterised specifications. We introduced the syntax and semantics of the language T, and report a compiler that interprets a specification written in T into an equivalent LTL formulation. Finally, we discuss the advantages of T and the compiler compared to other languages.

Students often face difficulty in self-directed learning scenarios (e.g., studying, research) because they need to control many aspects of the learning session. They need to decide what to learn, how long to perform a learning task, when to shift to a different learning task and manage distractions apart from others. We observed from our previous research that self-reflection and self-evaluation helped students manage their own learning. However, majority of the students only evaluated one or two major aspects of the learning session that they think needed to be changed or improved (e.g., need to spend less time in non-learning related activities, need to focus on only one learning task at a time). If students would look further into their learning session, they would discover more behaviors that also need to be re-evaluated. In this paper we discussed reinforcement learning-based methods for discovering good learning behavior which can be used by future systems to suggest to students possible ways to improve their behavior.

Wireless sensor networks (WSN) are a popular platform to support applications that require data collection from multiple sources. Using wireless networks to provide the communication infrastructure for these sensors makes the data from sensors prone to delays and loss due to the shared nature of a wireless medium. In applications where heterogeneous sensors are crucial for data collection, sensors generate data with different levels of importance and delivery requirements. This study presents a data collection method for WSNs that provides a classification scheme for sensors, and a prioritization method used to complement a TDMA-based medium access control algorithm to arbitrate data transmission among these sensors.

The emergence of e-patient has encouraged people to be more literate about healthcare subject. However, health information seeking remains problematic for most non-medical professionals (consumers). Most consumers are not knowledgeable with medical terminology. The diversity of consumer’s familiarity with health domain also leads to frustration since the information presented may fall outside the consumer’s comprehension level. This research aims to assist consumers obtain understandable health information by designing adaptive personalization approach in health information retrieval system. The proposed approach constructs user model dynamically based on the interaction with search engine. The user model captures contextual attributes and the familiarity level with health topic in a weighted semantic network. A node represents a topic of interest and its familiarity level and a weighted-link shows semantic similarity between nodes, which refers to Unified Medical Language System Semantic Network.

A tablet PC system using an etymological memorization method with animations can enable Japanese children to memorize English words. The system specifically helps with memorization of compound nouns, which are combination of two simple nouns, for animals. For each noun it shows an animation with a narration produced by a voice synthesizer, followed by an animation showing the compound noun, again with narration. The system was experimentally evaluated by comparing the effectiveness of using animation, pictures, and text. We examined whether sentence construction by combining a compound animal noun with a simple verb, accompanied by animation, was effective for memorization after learning such nouns. The experimental subjects were 111 Japanese children in the fifth and sixth grades of elementary school. The experimental results were analyzed in terms of various subjects and conditions.

This paper describes a serious game for studying chemical bonding – a subject that does not exist in the regular Japanese elementary school curriculum. The system aims to induce children’s interest in the unknown subject of chemistry. Using a system that shows atoms and molecules on a screen, children can perform chemical bonding virtually and produce virtual material objects by hand. The system uses the Kinect sensor for gesture recognition. It was evaluated in two experiments using test subjects. In the first experiment, the subjects were 37 children in the sixth grade. Most of these children became interested in chemistry, but there were some problems with the user interface. Accordingly, a second experiment was conducted to compare a modified interface and the initial unmodified interface. This experiment confirmed that the modified interface provided better operability and a more favorable user impression.

It is difficult for programming novices to correct a program when it does not behave as they intended. Although it is possible for novices to use a debugger, its installation can cause initial obstacles. Even after a successful installation, it can be difficult to choose appropriate actions. Therefore, a debugger is needed that needs no installation and provides features and information that match a beginners’ proficiency. This paper discusses the design of a visual debugger for C that runs in Web browsers. The system is constructed using HTML + CSS + JavaScript, and therefore can be customized easily by a teacher. It offers information such as animations adapted to the state of a program’s execution. It is difficult to execute C programs in Web browsers because the C language is usually compiled into a machine-language form. The proposed system therefore uses an interpreter for a subset of C implemented in JavaScript.

This paper proposes a novel coding scheme which can extend the lifespan of flash memory. Flash memory has a number of advantages against conventional storage devices, but it must be noted that the flash cells which constitute a flash memory accommodate, not a small, but limited number of operations only. A flash code provides a clever way to represent data values in flash memory so that the number of operations over flash cells becomes as small as possible, and this contributes to extend the lifespan of flash memory. Several flash codes have been studied so far, and this paper proposes a novel coding scheme which makes use of two different modes of encoding. Computer simulation shows that the proposed coding scheme shows much better average-case performance than existing codes. Besides the computer simulation, the paper also gives detailed analysis of the performance which justifies the advantage of the proposed code from a more theoretical viewpoint.

We propose an applied Java programming exercise with board-game strategy for problem-solving learning. In the study, we use the Gogo game, a variation of Gomoku. During implementation of move methods of the game, students learn the realization of an idea as algorithms and revisions through trial and error based on execution results. In addition, we have developed a support system called WinG, which consists of the local review package LA and the contest management server CS. The server maintains a preliminary and a final league, which decide the scores of students based on the results of round-robin matching. We performed several educational practice sessions in 2011. By introducing three levels of index strategies as the standard of strength, the number of student submissions increased. A weighted winning degree was introduced for more precise strategy ranking and rating. We analyze the relations and tendencies of the rankings in both leagues, and also discuss the efficiency of the process in round-robin matching and an approximate ranking method for immediately response.

We usually prove logical formulas by rewriting them step by step. Reduction machines have been proposed for functional programming languages to make an inference based on such a rewriting scheme. However, it has not been efficient in distributed environment, since they rewrite a logical formula on a memory by using processors. A computer network has many switches, and transfers packets to their destinations. We propose to rewrite a formula in logic or algebra on distributed switches and state memories with higher-order meta-rules. Although such inference seems similar to one by a production rule in expert systems, it utilizes distributed working memories and self-optimizing properties in their inference with meta-rules. We show this mechanism is appropriate for weight-based learning for controlling its inference, and inter-subjective formalization for a sensor network in Empathic Computing.

The following section is included:

• AUTHOR INDEX