2000 Fiscal Year Annual Research Report
解析的意味論に基づく実時間プログラムシステムの検証の研究
| Project/Area Number |
10680332
|
|---|
| Research Institution | UNIVERSITY OF TSUKUBA |
|---|
Principal Investigator |
水谷 哲也 筑波大学, 電子・情報工学系, 講師 (70209758)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
池田 靖雄 埼玉短期大学, 情報処理学科, 講師 (10279599)
細野 千春 筑波大学, 電子・情報工学系, 助教授 (20108294)
五十嵐 滋 筑波大学, 電子・情報工学系, 教授 (80027367)
塩 雅之 常磐大学, コミュニティ振興学部, 講師 (60302395)
富田 康治 経済産業省, 産業技術総合研究所, 研究員 (80357574)
|
|---|
| Keywords | 実時間システムの検証 / エンヴェローブ理論 / SOFA / 音楽情報処理 / Tense Arithmetic |
|---|
| Research Abstract |
論理的プログラムに関する研究は,現代のプログラム理論において重要な問題の1つである.本研究では,解析的意味論を基にした解析的同値理論及び実時間プログラム検証体系SOFA,エンヴェロープ理論tense arithmetic等により,論理的プログラム・システム及びその検証系を構築した.解析的意味論で用いられるν-定義可能行為はプログラムを高階の数学理論の言語で表現するものであり,数学的,論理的に厳密な理論を展開することができる.またSOFA,tense arithmetic等の実時間プログラム検証体系はビークルの制御系や生ピアノの自動重奏システムなどの連続的に変化する外部の物理系を離散的に制御するプログラム系を検証するシステムである.
連続変化外部系を離散的に制御するプログラム系のtense arithmeticによる検証・解析システムの研究を行い、
・ビークル自動制御系の論理的仕様表現及び解析の研究を行なうとともに,実時間システムの例題のひとつである音楽情報処理分野においては,楽曲構造に着目することにより,
・実時間協調演奏システムの形式的理論的表現
・演奏ルールの形式的理論的表現
・それらの成果に基づいた楽曲分析システム,実時間協調演奏システムの実装を研究し,成果を得た.
|
-
[Publications] Liu.J.,Hiraga.R.and Igarashi.S: "Musical Analysis of a Computer Music Project. by Computer-Assistance, for Computer Music Application "Porc.of ICMC. 477-480 (2000)
-
[Publications] 永田恵典,船田宏聡,水谷哲也,五十嵐滋: "芸術的演奏生成を目的とする協調演奏システム"人工知能学会全国大会(第14回)論文集. 472-475 (2000)
-
[Publications] 五十嵐滋,小池宏幸,水谷哲也: "音楽の構造機能とそれに基く演奏創造"人工知能学会全国大会(第14回)論文集. 487-490 (2000)
-
[Publications] 水谷哲也,酒井祐樹,塩雅之,五十嵐滋: "Tense Arithmeticによる協調演奏システムの使用表現とその実装"応用数学合同研究集会報告集. 13-18 (2000)
-
[Publications] 船田宏聡,永田恵典,酒井祐樹,五十嵐滋,水谷哲也: "PSYCHE:協調システムを中心として"第42回プログラミングシンポジウム. 165-168 (2001)
-
[Publications] Mizutani,T., Igarashi,S.and Shio,M.: "Representation of a Discretely Controlled Continuous Systems in Tense Arithmetic"Electronic Notes In Theoretical Computer Science. 42. 1-12 (2001)
-
[Publications] 五十嵐滋: "ヤマハミュージックメディア"演奏を科学する. 220 (2000)
