Research Overview

In our laboratory, we study how to build formal models for complex objects in the real world. Particularly, we focus on concurrent systems and hybrid systems, where a concurrent system is a dynamic system in which many interacting processes run concurrently, and a hybrid system is a dynamic system that exhibits both continuous and discrete dynamics. Moreover, we apply developed methods and tools to various kinds of targets in information systems, control systems, and systems biology.
（see also overview_e.pdf）．


Aim of Formal Modeling Approach

1. High Reliability
Before the operation, we can verify whether designed systems run correctly or not. 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. We can qualitatively evaluate performance of systems for given probabilistic inputs.

3. Design Automation
We can automatically synthesize a system that satisfies a given specification on its behavior. Moreover, if the 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, system science, control engineering, artificial intelligence, operations research, decision support systems, etc.

From Recent Results

1. Formal Approaches to Verification and Control of Dynamical Systems

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

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

　　 3) Development of the Computation Tool ``KCLP-HS''
　　　　(wodes06.pdf)

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

2. Systems Biology

　　 1) Estimation of Gene Regulatory Networks
　　　　(gene_regulation.pdf)

　　 2) Analysis and Control of Gene Regulatory Networks Based on Discrete Models
　　　　(2010ACC.pdf)

See also publications page.