Mathematical methods to know the past, the present, and the future

HIRAISHI Laboratory
Professor：HIRAISHI Kunihiko

E-mail：
［Research areas］
Mathematical Systems Science and Its Applications, Service science, Data science
［Keywords］
Discrete-Event/Hybrid Systems, Formal Verification, Agent Simulation, Situation Awareness, Business Process

Skills and background we are looking for in prospective students

Mathematical thinking, basic knowledge on algorithms, graph theory, linear algebra, and differential/integral calculus

What you can expect to learn in this laboratory

Ability to discover the problem to be studied, to build mathematical/formal models, to survey what technologies can be applied, and to combine various solution methods. To learn these skills, reading papers is insufficient and it is necessary to have a bird’s-eye view on the related research areas. Moreover, ability to implement new ideas as computer programs is required.

【Job category of graduates】 ICT, Manufacturing, Automobile

Research outline

Virtual Field Experiments for Smart Voice Messaging System

In this laboratory, we study how complex objects in the real world are formally modeled, and how the problems can be solved by the models, where we focus on the class of models that can be handled by mathematical methods and computers. We call this calss of models formal models. Using the models, we are able (1) to verify the correctness of the design in the early stage of the system development, (2) to optimize the system performance by parameter tuning, (3) to synthesize the system that satisfies given specifications, and (4) to identify system models based on observed data.　In addition, models can be used for mining knowledge from a large amount of data.

Recent research topics using formal modeling techniques are listed as follows:

• Behavior modeling and situation recognition in caregiving services (probabilistic models, agent simulation).
• Configuration change in cloud computing systems (formal method, online algorithms)
• Verification of business processes with time constraints (timed automata)
• Congestion control of airport surface (object Petri nets, queueing systems)
• Modeling and control of gene regulatory networks (Boolean nets, Markov processes)

We welcome student who are interested in solving real problems based on formal modeling technique.

Key publications

1. V. G. Trinh, T. Akutsu, K. Hiraishi: An FVS-based Approach to Attractor Detection in Asynchronous Random Boolean Networks, IEEE/ACM Transactions on Computational Biology and Bioinformatics (2020)
2. K. Uehara, K. Hiraishi: Process Mining Approach for the Conformance Checking of Discrete-Event Simulation Model, SICE Annual Conference 2019, pp. 615-620 (2019/9/10-13, Hiroshima, Japan)
3. K. Hiraishi, K. Kobayashi: A Pathfinding Problem for Search Trees with Unknown Edge Length, Journal of Discrete Algorithms, Vol. 49, pp.1-7 (2018)

Equipment

Software for design and verification of discrete-event/hybrid systems.