Overview

In our laboratory, we study how to build formal models, i.e. mathematically and computationally tractable models, for complex objects in the real world. In particular, we focus on discrete-state systems and hybrid systems, where discrete-state systems are dynamical systems that can be represented by state transition diagrams, and hybrid systems are dynamical systems that exhibit both continuous and discrete dynamics. Moreover, we apply developed theory and methods to various kinds of targets in information systems, service systems, control systems, and systems biology.
（see also overview_e.pdf）．


Aim of Formal Modeling Approach

1. High Reliability
We can verify whether designed systems run correctly or not before actual operations. Moreover, if a system is proved to be incorrect, then we can know in which part of the system errors exist. Unlike simulation and test, possible behavior of systems can be comprehensively checked.

2. High Performance
We can optimize systems by assigning appropriate values for system parameters. Moreover, we can qualitatively evaluate performance of systems for given probabilistic inputs.

3. Design Automation
We can automatically synthesize systems that fulfill given specifications. Moreover, if some specification is proved to be infeasible, then feasible alternatives for the specification are presented.

4. System Identification
We can build dynamical mathematical models from observed data.


Related Areas
Researches in this laboratory are related to various research areas including theoretical computer science, software science, logics, systems science, control engineering, artificial intelligence, operations research, decision support systems, service science etc.

From Recent Results

1. Formal Approaches to Verification and Control of Dynamical Systems

By combining formal verification technology with existing control theory, it is possible to compute control inputs that achieve satisfaction of logical constraints together with optimization of a given objective function. For example, the figure below depicts the situation in which two cars are running on a road. Given some logical constraint such as “the two cars should come close to less than 0.5m at least every 3s”, the objective is to compute control inputs that minimize energy consumption and also achieve the logical constraint. This problem is solvable by combination of discrete abstraction technique based on bisimulation and model predictive control scheme.

1) Formal Approaches to Model-Based Development of Real-Time/Hybrid Systems
　　　　(sice208ws.pdf)

2) Control Theory for Hybrid Systems with Discrete Dynamics
　　　　(ACA2008.pdf)

3) Safety Verification by Fluidification of Discrete Dynamics
　　　　(ATPN08.pdf)

4) Box Abstraction of Transition Systems on Real Vector Fields
　　　　(sig_des2010.pdf)

2.Modeling Human Behavior in Service Fields

Our laboratory participates in a R&D project that aims to improve working environment in hospitals/nursing homes by using special IT devices called “Voice Tweet Device”. In the project, we try to build behavior models for human activities based on collected location data from the devices. Using the behavior models, we evaluate differences on the behavior between working staffs, and also detect suspicious activities that should be checked later. To verify the effectiveness of the devices, we also perform experiments on virtual fields, experiment spaces designed for reproducing typical situations in the real field. (URL: http://www.jaist.ac.jp/ks/mot/JSTservice/)

1) Behavior Modeling in Physical and Adaptive Intelligent Services
　　　　(cogsima2014.pdf)

2) Detection of Unusual Human Activities
　　　　(wodes2014.pdf)

3) Discrete Event Simulation
　　　　（simulation.avi）

4) Spatio-Temporal Situation Recognition
　　　　(SMC2019.pdf)

3. Data Science Approach to Diagnosis of Discrete Event Systems

We propose a new method for diagnosis of stochastic discrete event system. The only information necessary for the method is event logs from the target system. Using event logs from the system in the normal situation, N-gram models are learned, where the N-gram model is used as approximation of the system behavior in steady state. Based on the N-gram model, the diagnoser estimates what kind of faults has occurred in the system, or may conclude that no faults occurs.

　　　　(danms2013.pdf)

4. Modeling of Airspace Traffic Using CARATS Open Data

Ministry of Land, Infrastructure, Transport and Tourism of Japan provides a large amount of airspace traffic data to researchers. It is called the CARATS open data. One of the applications of this data is to build traffic flow models in order to predict future airspace traffic. We apply various modeling methods for building such models.

　　　　(CARATS.pdf)

5. Other Applications

1) Management of Cloud Computing Systems
Shinji Kikuchi, Kunihiko Hiraishi: Improving Reliability in Management of Cloud Computing Infrastructure by Formal Methods, IEEE/IFIP Network Operations and Management Symposium(NOMS) 2014, (2014/5/5-9, Krakow, Poland)

2) Verification of Business Process
Kenji Watahiki, Fuyuki Ishikawa, Kunihiko Hiraishi: Formal Verification of Business Processes with Temporal and Resource Constraints, 2011 IEEE International Conference on Systems, Man, and Cybernetics, pp.1173-1180 (2011/10/9-12, Anchorage, Alaska)

3) Computational Biology
Koichi Kobayashi and Kunihiko Hiraishi: ILP/SMT-Based Method for Design of Boolean Networks Based on Singleton Attractors, IEEE/ACM Transactions on Computational Biology and Bioinformatics, Issue No.6, pp.1253-1259 (2014)

4) Airport Surface Modeling and Simulation
Kenji Uehara, Kunihiko Hiraishi and Koichi Kobayashi: Modeling of Traffic Congestion on Airport Surface using Petri Net, IEICE Technical Report, MSS2014-54, pp.17-22 (2014)