論文

• Takashi Tomita, Atsushi Ueno, Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki.. Safraless LTL synthesis considering maximal realizability, Acta Informatica, pp. 1-38, Oct. 2016.
• Sohei Ito, Takuma Ichinose, Masaya Shimakawa, Naoko Izumi, Shigeki Hagihara, Naoki Yonezaki. Qualitative analysis of gene regulatory networks by temporal logic, Theoretical Computer Science, Vol. 594, pp. 151-179, Aug. 2015.
• Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki. Bounded Strong Satisfiability Checking of Reactive System Specifications, IEICE Transactions on Information and Systems, A Publication of the Information and Systems Society, Vol. E97-D, No. 7, pp. 1746-1755, July 2014.
• Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki. Complexity of Strong Satisfiability Problems for Reactive System Specifications, IEICE Transactions on Information and Systems, A Publication of the Information and Systems Society, Vol. E96-D, No. 10, pp. 2187-2193, Oct. 2013.
• Sohei Ito, Takuma Ichinose, Masaya Shimakawa, Naoko Izumi, Shigeki Hagihara, Naoki Yonezaki. Modular analysis of gene networks by linear temporal logic, Journal of Integrative Bioinformatics, Vol. 10, No. 2, 216, 2013.  公式リンク  
  
• 萩原茂樹, 北村佑介, 島川昌也, 関戸聡, 米崎直樹. リアクティブシステム仕様を実現可能にするための環境制約の抽出, コンピューターソフトウェア, 岩波書店, Vol. 28, No. 3, pp. 132-146, Aug. 2011.
• I. Yamada, S. Ishiwata, I. Terasaki, M. Azuma, Y. Shimakawa, M. Takano. Synthesis, Structure, and Physical Properties of A-site Ordered Perovskites ACu3Co4O12 (A = Ca and Y), CHEMISTRY OF MATERIALS, Vol. 22, No. 18, pp. 5328-5332, Sept. 2010.

国際会議発表 (査読有り)

• Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki. Efficiency of the Strong Satisfiability Checking Procedure for Reactive System Specifications, International Conference on Computer, Electronic Engineering and Information Science (CEEIS 2017), Dec. 2017.
• Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki. Towards Improvements of Bounded Realizability Checking, Workshop on Computation: Theory and Practice (WCTP2017), Sept. 2017.
• Shigeki Hagihara, Masaya Shimakawa, Naoki Yonezaki. Discussion on Verification of Voting Protocols, 17th Philippine Computing Science Congress (PCSC 2017), Proceedings of the 17th Philippine Computing Science Congress, Mar. 2017.
• Shigeki Hagihara, Masahiko Tomoishi, Masaya Shimakawa, Naoki Yonezaki. Combining Unification and Rewriting in Proofs for Modal Logics with First-order Undefinable Frames, 5th International Conference on Computer Science, Electronics Technology and Automation (ICCSETA 2017), Preproceedings of 5th International Conference on Computer Science, Electronics Technology and Automation (ICCSETA 2017), Mar. 2017.
• Masaya Shimakawa, Kenji Osari, Shigeki Hagihara, Naoki Yonezaki. Modularization of formal specifications for efficient synthesis of reactive systems, 6th International Conference on Software and Computer Applications (ICSCA 2017), Preproceedings of 6th International Conference on Software and Computer Applications (ICSCA 2017), Feb. 2017.
• Shigeki Hagihara, Yoshiharu Fushihara, Masaya Shimakawa, Masahiko Tomoishi, Naoki Yonezaki. Web server access trend analysis based on the Poisson distribution, 6th International Conference on Software and Computer Applications (ICSCA 2017), Preproceedings of 6th International Conference on Software and Computer Applications (ICSCA 2017), Feb. 2017.
• Masaya Shimakawa, Yuuji Iwasaki, Shigeki Hagihara, Naoki Yonezaki. Discussion of LTL Subsets for Efficient Verification, Workshop on Computation: Theory and Practice (WCTP2016), Preproceedings of Workshop on Computation: Theory and Practice (WCTP2016), pp. 1-14, Sept. 2016.
• Shigeki Hagihara, Atsushi Ueno, Takashi Tomita, Masaya Shimakawa, Naoki Yonezaki. Simple synthesis of reactive systems with tolerance for unexpected environmental behavior, the 4th FME Workshop on Formal Methods in Software Engineering (FormaliSE '16), Proceedings of the 4th FME Workshop on Formal Methods in Software Engineering (FormaliSE '16), ACM New York, pp. 15-21, May 2016.
• Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki.. Towards Unbounded Realizability Checking, Workshop on Computation: Theory and Practice (WCTP2015), Preproceedings of Workshop on Computation: Theory and Practice (WCTP2015), pp. 80-90, Sept. 2015.
• Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki.. Reducing Bounded Realizability Analysis to Reachability Checking, 9th International Workshop on Reachability Problems(RP 2015), Reachability Problems, Lecture Notes in Computer Science, Springer, Vol. 9328, pp. 140-152, Sept. 2015.
• Shohei Mochizuki, Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki. Fast Translation from LTL to Büchi Automata via Non-transition-based Automata, 16th International Conference on Formal Engineering Methods (ICFEM 2014), Formal Methods and Software Engineering, 16th International Conference on Formal Engineering Methods, ICFEM 2014, Lecture Notes in Computer Science, Springer, Vol. 8829, pp. 364-379, Nov. 2014.
• Shigeki Hagihara, Naoki Egawa, Masaya Shimakawa, Naoki Yonezaki. Minimal strongly unsatisfiable subsets of reactive system specifications, the 29th ACM/IEEE international conference on Automated software engineering (ASE2014), Proceedings of the 29th ACM/IEEE international conference on Automated software engineering (ASE2014), ACM New York, pp. 629-634, Sept. 2014.
• Kenji Osari, Takuya Murooka, Kiyotaka Hagiwara, Takahiro Ando, Masaya Shimakawa, Sohei Ito, Shigeki Hagihara, Naoki Yonezaki. An object-oriented language for parameterised reactive system specification based on linear temporal logic, Workshop on Computation: Theory and Practice (WCTP2013), Preproceedings of Workshop on Computation: Theory and Practice (WCTP2013), pp. 94-113, Sept. 2013.
• Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki. SAT–Based Bounded Strong Satisfiability Checking of Reactive System Specifications, Information & Communication Technology - EurAsia Conference 2013 (ICT-EurAsia 2013), Information and Communicatiaon Technology, Lecture Notes in Computer Science, Vol. 7804, pp. 60-70, Mar. 2013.
• Sohei Ito, Takuma Ichinose, Masaya Shimakawa, Naoko Izumi, Shigeki Hagihara, Naoki Yonezaki. Modular analysis of gene networks by linear temporal logic, proceedings of 9th International Symposium on Integrative Bioinformatics, pp. 43-54, Mar. 2013.
• Sohei Ito, Takuma Ichinose, Masaya Shimakawa, Naoko Izumi, Shigeki Hagihara, Naoki Yonezaki. Qualitative analysis of gene regulatory networks using network motifs, proceedings of 4th International Conference on Bioinformatics Models, Methods and Algorithms (BIOINFORMATICS2013), pp. 15-24, Feb. 2013.
• Sohei Ito, Takuma Ichinose, Masaya Shimakawa, Naoko Izumi, Shigeki Hagihara, Naoki Yonezaki. Modular analysis of gene networks using temporal logic (abstract), 5th Annual RECOMB Conference on Regulatory and Systems Genomics, with DREAM Challenges, program booklet, pp. 118-119, Nov. 2012.
• Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki. Complexity of Checking Strong Satisfiability of Reactive System Specifications, International Conference on Advances in Information Technology and Communication, AIT 2012, International Conference on Advances in Information Technology and Communication, AIT 2012, pp. 42-51, Sept. 2012.
• Shigeki Hagihara, Takahiro Arai, Masaya Shimakawa, Naoki Yonezaki. Developing Embedded Systems from Formal Specifications Written in Temporal Logic, the Third International Conference on Trends in Information, Telecommunication and Computing (ITC2012), Proceedings of the Third International Conference on Trends in Information, Telecommunication and Computing, Lecture Notes in Electrical Engineering, Springer, Vol. 150, pp. 107-113, Aug. 2012.
• Shigeki Hagihara, Yusuke Kitamura, Masaya Shimakawa, Naoki Yonezaki. Extracting Environmental Constraints to Make Reactive System Specifications Realizable, Proceedings of 16th Asia-Pacific Software Engineering Conference APSEC 2009, pp. 61-68, Dec. 2009.

国内会議発表 (査読有り)

• 冨田尭, 上野篤史, 萩原茂樹, 島川昌也, 米崎直樹. 可能な限り仕様を満たすリアクティブシステムの合成, 第22回 ソフトウェア工学の基礎ワークショップ FOSE 2015, ソフトウェア工学の基礎XXII, 日本ソフトウェア科学会 FOSE 2015, 近代科学社, pp. 77-86, Nov. 2015.
• 萩原茂樹, 江川直毅, 島川昌也, 米崎直樹. 強充足不能なリアクティブシステム仕様における欠陥範囲の特定, 第20回 ソフトウェア工学の基礎ワークショップ FOSE 2013, ソフトウェア工学の基礎XX, 日本ソフトウェア科学会 FOSE 2013, 近代科学社, pp. 143-152, Nov. 2013.
• 望月翔平, 島川昌也, 萩原茂樹, 米崎直樹. LTL式からBuchiオートマトンへの高速な変換法, 第19回 ソフトウェア工学の基礎ワークショップ FOSE 2012, ソフトウェア工学の基礎XIX, 日本ソフトウェア科学会 FOSE 2012, 近代科学社, pp. 91-100, Dec. 2012.
• 新井貴大, 島川昌也, 萩原茂樹, 米崎直樹. 時間論理で記述された仕様からのプログラム自動抽出による組み込みシステム構成手法, ソフトウェア工学の基礎XVIII, 日本ソフトウェア科学会 FOSE2011, pp. 151-156, Nov. 2011.
• 萩原茂樹, 北村佑介, 島川昌也, 米崎直樹. リアクティブシステム仕様を実現可能にするための環境制約の抽出, ソフトウェア工学の基礎XVI, 日本ソフトウェア科学会 FOSE2009, pp. 37-48, Nov. 2009.
• 北村佑介, 島川昌也, 萩原茂樹, 米崎直樹. リアクティブシステム仕様の外部環境制約について, 第五回システム検証の科学技術シンポジウム, 第五回システム検証の科学技術シンポジウム予稿集, pp. 7-18, Nov. 2008.
• 島川昌也, 萩原茂樹, 米崎直樹. リアクティブシステム仕様の強充足可能性判定問題の計算量について, 第4回システム検証の科学技術シンポジウム予稿集, pp. 21-29, Nov. 2007.
• 島川昌也, 萩原茂樹, 米崎直樹. リアクティブシステムを対象とした様々な実行時検証概念の形式化とその判定アルゴリズムの完全性, 第二回システム検証の科学技術シンポジウム予稿集, pp. 246-259, Oct. 2005.  公式リンク  
  

国内会議発表 (査読なし・不明)

• 島川 昌也, 萩原 茂樹, 米崎 直樹. リアクティブシステム仕様の実現可能性に関する非有界検査の効率化に向けて, 第14回ディペンダブルシステムワークショップ DSW2016, Dec. 2016.
• 冨田尭, 萩原茂樹, 島川昌也, 米崎直樹. 実現可能性の必要条件に基づいた不完全リアクティブシステム合成, 日本ソフトウェア科学会第32回大会講演論文集, Sept. 2015.
• 上野篤史, 冨田尭, 島川昌也, 萩原茂樹, 米崎直樹. 環境許容性のあるリアクティブシステム合成法, 電子情報通信学会ソフトウェアサイエンス研究会, 信学技報, Vol. 114, No. 510, pp. 7-12, Mar. 2015.
• 萩原茂樹, 江川直毅, 島川昌也, 米崎直樹. リアクティブシステム仕様の極小強充足不能部分計算に関する考察, 情報処理学会第99回プログラミング研究発表会, June 2014.
• 上野篤史, 望月翔平, 島川昌也, 萩原茂樹, 米崎直樹. LTL式で記述されたリアクティブシステム仕様の高速な実現可能性判定器の実装, 第20回ソフトウェア工学の基礎ワークショップFOSE2013, Nov. 2013.
• 長利健治, 室岡拓弥, 萩原聖貴, 安藤崇央, 島川昌也, 伊藤宗平, 萩原茂樹, 米崎直樹. 記述性を重視したリアクティブシステム用仕様記述言語T, 第20回ソフトウェア工学の基礎ワークショップFOSE2013, Nov. 2013.
• 上野篤史, 望月翔平, 島川昌也, 萩原茂樹, 米崎直樹. LTL式で記述されたリアクティブシステム仕様の高速な実現可能性判定器の実装に関する研究, 日本ソフトウェア科学会第30回大会講演論文集, Sept. 2013.
• 島川昌也, 萩原茂樹, 米崎直樹. 実現可能性判定コスト削減のための無限ゲーム単純化手法, 日本ソフトウェア科学会第27回大会講演論文集, Sept. 2010.
• 萩原聖貴, 安藤崇央, 島川昌也, 伊藤宗平, 萩原茂樹, 米崎直樹. 記述性を重視したリアクティブシステム用仕様記述言語T, 日本ソフトウェア科学会第26回大会講演論文集, Sept. 2009.
• 島川昌也, 萩原茂樹, 米崎直樹. 実現可能性判定コスト削減のためのLTL構文の制限とそれによる仕様の判定法, 日本ソフトウェア科学会第26回大会講演論文集, Sept. 2009.
• 島川昌也, 萩原茂樹, 米崎直樹. SAT Solverを用いたリアクティブシステム仕様の有界強充足可能性判定, 日本ソフトウェア科学会第25回大会講演論文集, Sept. 2008.
• 島川昌也, 萩原茂樹, 米崎直樹. 仕様の自動検証に適したLTLフラグメント ― 実現集合を表す決定性オートマトン構成の立場から―, 日本ソフトウェア科学会第23回大会, 日本ソフトウェア科学会第23回大会講演論文集, Sept. 2006.
• 島川昌也, 萩原茂樹, 米崎直樹. 実時間論理により記述された動作仕様の実行時検証手続き, 日本ソフトウェア科学会第21回大会講演論文集, pp. 179-183, Sept. 2004.

学位論文

• リアクティブシステム仕様の実現可能性検証における計算量削減方式に関する研究,  論文要旨,  博士（工学）,  東京工業大学,  2014/09/25,   
• リアクティブシステム仕様の実現可能性検証における計算量削減方式に関する研究,  本文,  博士（工学）,  東京工業大学,  2014/09/25,   
• リアクティブシステム仕様の実現可能性検証における計算量削減方式に関する研究,  審査の要旨,  博士（工学）,  東京工業大学,  2014/09/25,   

[ BibTeX 形式で保存 ]    [ 論文・著書をCSV形式で保存 ]    [ 特許をCSV形式で保存 ]