- Mathematical optimization and its application
- Software verification tools
- Service Computing
- Mathematical information science, complex systems
- Industrial Engineering, Management Systems
- Development support for high performance parallel programs
- Astrophysics and Mathematical Sciences
Mathematical optimization and its application
Our research deals with mathematical optimization and its application to various combinatorial optimization problems. Some examples of these problems are the Chinese postman problem (to find a shortest cycle that visits, at least once, every edge of a connected directed or undirected graph), the travelling salesman problem (to find a shortest cycle that visits every vertex of a connected directed or undirected graph exactly once), and the apportionment problem (to find a distribution of seats proportional to the population of states or electoral districts). We strive to develop efficient algorithms for these and other difficult problems, and to derive their properties. Below, we briefly show an application of optimization to social science. To meet the ideal of a representative democracy (one person, one vote), we have developed a new class of apportionment methods which include the five methods in the following figure (left). One of the most important properties is bias. We discovered that the Webster method is the best among various methods from this standpoint. See the bottom right figure for an interesting illustration of how different methods converge.
Software verification tools
This laboratory studies software verification that uses model checking. We have developed the following verification tools thus far:
- UML state machine diagram tool
This verification tool was developed for UML (Unified Modeling Language) state machine diagrams, is often used by software development engineers, and uses the UPPAAL model-checker tool. When a state machine diagram is drawn using this tool, UPPAAL input files are automatically generated, thus verifying whether a separately input expression holds.
- Automatic test code generation tool
Specifically developed for the Ruby programming language, this is an automatic test code generation tool for unit tests. When a NuSMV model checker is used to describe the behaviors of a target program and the properties it is expected to hold, this tool uses counterexamples, obtained as a result of NuSMV execution, to automatically generate test codes.
- C language program verification tool
This is a C language program verification tool that takes advantage of CBMC, a model checker for C language programs. Applied individually, CBMC cannot verify programs that may cause an infinite loop, but this tool has solved this bottleneck and can detect memory leaks, NULL pointers, unauthorized memory area access, divide by zero, and other deleterious anomalies.
Integrating state-of-the-art technologies, such as telecommunication, enterprise, and internet technologies, has become a crucial requirement to meet diverse demands in the current IT world. Coordination of these domains could spur development of versatile IT applications and produce personalized services tailored for each individual customer. This concept, referred to as Service Computing, reduces development costs and time, and will be a key factor in high-mix low-volume applications.
Our basic approach is to join together various Web-Service-based components accessible through networks. These components include Cloud APIs, databases, media servers, sensors, a Voice over IP (VoIP) server, and others we have developed. For example, a VoIP server coordinated with a text-to-speech component and a Twitter site can transfer a voice stream speaking Twitter text. We create applications on PCs, servers, AndroidTM terminals, Cloud platforms (Google App Engine TM), or embedded systems. Service Computing is expected to play an important role in the Web world and enterprise environments, as well as in our daily lives.
Mathematical information science, complex systems
Our research investigates the nature of systems consisting of many elements that have simple functions yet demonstrate complex behavior as a whole. A typical example is cellular automata (CA), in which finite automata are arranged in regular arrays. We are also working on evolutionary computation, which employs evolutionary systems, and the L-system, which is used to model the growth processes of plant development.
Industrial Engineering, Management Systems
Our research focuses on the optimal design and operation of various kinds of management systems, with particular attention given to production and education systems. The methodologies used in our research include Industrial Engineering (IE), Operations Research (OR), and computer simulations.
One of the research projects we are working on is the improvement of production schedules by using batch splitting. It is commonly accepted that batch splitting can improve various evaluation measures, but as the number of batches is increased through splitting, shop floor control and scheduling problems tend to become more difficult. Thus, there is a great need for efficient batching and scheduling methods. We have developed a genetic algorithm (GA) that prevents searching efficiency from being reduced when the number of batches is increased through batch splitting, and we are evaluating its properties using computer simulations.
Development support for high performance parallel programs
Our research focuses on the development of support for parallel programs. Recently, many types of parallel computing hardware are available in the field of scientific computing, including PC clusters, multicore processors, GPUs, and their combinations. The complexity of the various architectures makes it difficult to develop efficient parallel programs. Therefore, our research addresses the framework and compiler techniques that will enable anyone to easily develop programs by abstracting the requirements of parallel programming.
Astrophysics and Mathematical Sciences
Our group studies theoretical physics and mathematical modeling using simulations, mainly with solving differential equations or statistical approaches.
For graduate course students:
Main research topics are in astrophysical phenomena especially related to general theory of relativity, such as black holes, gravitational waves, and cosmology. Current targeting topics are (a) testing gravity theories from data analysis of gravitational wave, (b) non-linear dynamics in higher-dimensional space-time, and (c) formation process of black holes and singularities. Not only their simulations, but their formulations and methodologies are included.
For undergraduate students:
Using topics in astrophysical phenomenon, students will be trained how to formulate a model, how to simulate differential equations, how to analyze and interpret their results, including visualizations. Students will pick up their favorite topics for their Bachelor Thesis, e.g. developing database systems, games or educational materials.