An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop. - Takeshi Nagaoka; Kozo Okano; Shinji Kusumoto (IEICE Trans. Inf. Syst., 2010)

Clock Number Reduction Abstraction on CEGAR Loop Approach to Timed Automaton. - Kozo Okano; Behzad Bordbar; Takeshi Nagaoka (ICNC, 2011)

QoS Analysis of Real-Time Distributed Systems Based on Hybrid Analysis of Probabilistic Model Checking Technique and Simulation. - Takeshi Nagaoka; Akihiko Ito; Kozo Okano; Shinji Kusumoto (IEICE Trans. Inf. Syst., 2011)