著者

小林 直樹 篠原 歩 佐藤 亮介 五十嵐 淳 海野 広志

出版者

東京大学

雑誌

基盤研究(S)

巻号頁・発行日

2015-05-29

---

本課題では、高階モデル検査の(1)理論的基盤の強化とそれに基づく高階モデル検査アルゴリズムの改良、(2)プログラム検証への応用、(3)高階モデル検査の拡張とそのプログラム検証への応用、(4)データ圧縮への応用、の4つを柱に研究を進めている。以下、それぞれの項目について、平成28年度(およびその繰越として遂行した平成29年度の一部の結果)について述べる。(1)理論的基盤の強化:HORSモデル検査とHFLモデル検査という2種類の高階モデル検査の間に相互変換が存在することを示すとともに、HFLモデル検査問題を型推論問題に帰着できることを示した。後者の結果に基づき、HFLモデル検査器のプロトタイプを作成した。また、高階文法の性質について調べ、語を生成するオーダーnの文法と木文法を生成するオーダーn-1の文法と間の対応関係を示した。さらに、高階モデル検査アルゴリズムの改良を行い、値呼びプログラムに対して直接的に高階モデル検査を適用する手法を考案、実装した。(2)プログラム検証への応用:プログラム検証で扱える対象プログラムや性質の拡充を行い、関数型プログラムの公平非停止性の検証、コード生成プログラムの検証、動的なスレッド生成を伴う高階並列プログラムの検証、などを可能にした。(3)拡張高階モデル検査:HORSに再帰型を加えて拡張したμHORSに対するモデル検査アルゴリズムの改良を行い、その有効性をJavaプログラムの検証を通して示した。(4)データ圧縮への応用:データをそれを生成する関数型プログラムの形に圧縮する方式(高階圧縮)について、圧縮後のプログラムをビット列に変換する部分の改良を行った。また、高階圧縮のための様々な要素技術について研究を進めた。

著者

塚田 武志 小林 直樹

出版者

情報処理学会

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.4, no.2, pp.31-47, 2011-03-25

---

言語の包含判定問題とは,与えられた言語 L1 と L2 について L1 ⊆ L2 が成立するか否かを判定する問題であり,理論的な興味の対象であるだけでなく,プログラム検証などへの広い応用を持つ重要な問題である.この問題に関する既知の最も強い結果の 1 つが文脈自由言語と超決定性言語の包含判定の決定可能性である.このオリジナルの証明は,Greibach と Friedman によって与えられている.我々はこの問題に対して,小林らによって提案されている型に基づく言語の包含判定の手法を適用し,決定可能性に対する別証明を与えた.この手法は以下のような利点を持つ.(1) 部分型関係やポンプの補題などのよく知られた概念で理論が展開できる.(2) 型推論を効率的に行う方法は多数提案されており,それらを利用することができる.また,提案する証明は小林らのアイデアを正規言語よりも広いクラスに適用したはじめての例であり,その他の非正規言語クラスへの応用も期待される.The language containment problem, which asks whether L1 ⊆ L2 for given languages L1 and L2, is an important problem in the field of formal language theory and has a variety of applications including program verification. One of the strongest result about this problem is the decidability for the case where L1 and L2 are context free and superdeterministic languages respectively, originally proved by Greibach and Friedman. In this paper, we give a new proof of the decidability, inspired by Kobayashi's type-based approach to language containment problems. The new proof has the following advantages. (1) The key notions and lemmas in the proof are well-known ones, such as subtyping and Pumping Lemma. (2) We can apply well-studied techniques for efficient typability checking. Furthermore, our proof is the first application of the type-based approach to the inclusion between non-regular languages and it seems applicable to other cases.

著者

岡田 光弘 小林 直樹 照井 一成 田村 直之

出版者

慶應義塾大学

雑誌

基盤研究(B)

巻号頁・発行日

2003

---

次の3点を中心に研究を進めた。1.証明論と意味論の統合的見方について研究を進めた。カット消去定理等の証明論の基本定理の成立条件がPhase semanticsによる意味論的分析により明らかになることを示した。又、Simple logic等の線形論理の基礎理論に対して、証明論と意味論の統合を進めた。さらに、直観主義論理Phase semanticsと古典論理Phase semanticsとの密接な関係を明らかにした。Phase semanticsの成果に基づいてカット消去定理の意味論的条件の研究を進めた。2.Reduction Paradigmによる計算モデルとProof-Search Paradigmによる計算モデルを統一的に分析できる論理的枠組の確立に向けた研究を進めた。ゲーム論的意味論等の観点からの分析も加えた。(岡田・Girard等フランスグループとの共同研究)これまでのReduction Paradigm(関数型言語の論理計算モデル)とProof-Search Paradigm(論理型言語や証明構成の計算モデル)の内的な統合を可能にするLudics等の新たな論理体系理論の分析をGirardグループらと共同で行なった。3.線形論理的概念がプログラミング言語理論やソフトウェア形式仕様・検証理論、計算量理論等にどのように応用され得るかのケーススタディーを行なった。例えば昨年に引き続き、ダイナミック実時間システムのシステマティックな設計・検証や認証プロトコル安全性証明等を例にとり、線形論理的観点や手法の応用可能性を示した。この目的でフランス及び米国共同研究グループとの共同研究を行なうとともに、計3回の成果報告会を日仏共同で行った。

著者

荒木 領 小林 直樹 大野 光平 伊丹 誠

出版者

一般社団法人映像情報メディア学会

雑誌

映像情報メディア学会技術報告 (ISSN:13426893)

巻号頁・発行日

vol.36, no.10, pp.41-44, 2012-02-17

被引用文献数

1

---

ワンセグメントサービスは,日本における地上波デジタル放送の移動体向けのサービスである.しかし,使用帯域の狭さからマルチパスによるディップの影響を受けやすくなり,受信特性の劣化する可能性がある.この対策として,アンテナダイバーシティ技術がある.しかし,携帯電話などの小型のワンセグ受信機では,端末内に複数のアンテナを十分なダイバーシティ利得が得られるほど離して配置するのは不可能である.そこで,本稿では3台の受信端末を用いて受信情報を共有する協調受信を提案する.提案方式では,協調受信に用いる受信端末の台数を増やすことでワンセグメントサービスの誤り率特性が改善できることを示す.

著者

松村 千鶴 雨宮 加奈 雨宮 さよ子 雨宮 昌子 雨宮 良樹 板垣 智之 市野沢 功 伊藤 拓馬 植原 彰 内野 陽一 大川 清人 大谷 雅人 角谷 拓 掃部 康宏 神戸 裕哉 北本 尚子 國武 陽子 久保川 恵里 小林 直樹 小林 美珠 斎藤 博 佐藤 友香 佐野 耕太 佐野 正昭 柴山 裕子 鈴木 としえ 辻沢 央 中 裕介 西口 有紀 服巻 洋介 吉屋 利雄 古屋 ナミ子 本城 正憲 牧野 崇司 松田 喬 松本 雅道 三村 直子 山田 修 山田 知佳 山田 三貴 山田 祥弘 山田 玲子 柚木 秀雄 若月 和道 鷲谷 いづみ

出版者

日本生態学会

雑誌

保全生態学研究 (ISSN:13424327)

巻号頁・発行日

vol.8, no.2, pp.175-180, 2003-12-30

被引用文献数

2

---

Flower visitations by both native and exotic bumblebee species were investigated at 21 monitoring sites in various regions of Japan in the spring and summer of 2002. The investigation was part of a long-term program that has been in progress since 1997 to monitor the invasion of an alien bumblebee, Bombus terrestris L. (Hymenoptera: Apidae). Flower visitation by B. terrestris was ascertained at two monitoring sites, one in Shizuoka and one in Hokkaido, where a large number of colonies of this species have been commercially introduced for agricultural pollination.

著者

羽生 宏人 和田 英一 丹羽 崇博 近藤 靖雄 川村 尚史 丸山 信也 岡村 彩乃 山科 早英良 永井 康仁 中道 達也 上道 茜 田中 成明 小林 直樹 笠原 次郎 森田 泰弘

出版者

THE JAPAN SOCIETY FOR AERONAUTICAL AND SPACE SCIENCES

雑誌

航空宇宙技術 (ISSN:18840477)

巻号頁・発行日

vol.9, pp.15-21, 2010

被引用文献数

1

---

The educational hybrid-rocket was successfully launched and it also landed within the predicted area. Aerodynamic characteristics of the rocket designed by students of Tsukuba University were evaluated by the wind tunnel testing with the support of Tokai University. The flight path affected by the environmental condition, especially wind direction and velocity, was simulated with the original calculation program. The altitude of the rocket was measured with the optical equipment and the apex was 123 m although the calculation indicated 198 m. We expected that the insufficient filling or the volatilization of Nitrous oxide as an oxidizer led to this result. And then, the apex was verified with a function of the oxidizer filling ratio. The results showed that 81.2 % of the oxidizer volume in comparison with the firing test condition was accumulated in the tank at the launch.

著者

小林 直樹

雑誌

文学史研究 (ISSN:03899772)

巻号頁・発行日

vol.47, pp.114-128, 2007

著者

秦東寺 久美 石橋 聡 小林 直樹

出版者

一般社団法人電子情報通信学会

雑誌

電子情報通信学会論文誌. D-II, 情報・システム, II-パターン処理 (ISSN:09151923)

巻号頁・発行日

vol.82, no.6, pp.1018-1030, 1999-06-25

被引用文献数

20

---

次世代動画像圧縮の標準であるMPEG-4では, 新たにVOP (Video Object Plane)という概念を取り入れ, 背景や物体等のビデオオブジェクトごとに符号化することが可能である. 特に動画像中の各々のフレームに共通な領域の動きが一組の平面の動きモデルで表されるとき, スプライトと呼ばれる平面オブジェクトを生成することが可能である. すなわち, 背景画像に代表されるような動画像中の複数フレームにわたる領域を1枚の静止画であるスプライトから再構成できる. スプライトを使用すると符号化効率の大幅な改善が期待できるため, スプライト生成技術に関する期待は大きい. 本論文では, ビデオクリップを撮影したときのカメラモーションに着目し, (1)7種類のカメラモーションと平行移動動きベクトルの関係を定式化し, (2)カメラモーションを反映した大局的な動きを算出するアルゴリズムを提案, (3)大局的な動きを用いてスプライトを自動生成するアルゴリズムを提案した. また, 複数の実画像を用いて実験を行った結果, 撮影時のカメラモーションを良好に抽出でき, これを用いてスプライトを自動生成することができた.

著者

鈴木 康夫 酒井 克彦 忠政 明彦 小林 直樹

出版者

一般社団法人日本機械学会

雑誌

生産加工・工作機械部門講演会 : 生産と加工に関する学術講演会

巻号頁・発行日

vol.2001, no.3, pp.59-60, 2001-11-20

被引用文献数

1

---

The purpose of this paper is to investigate the potential application of the cutting in the nitrogen atmosphere. In order to clarify the effects of the nitrogen atmosphere, cutting tests were carried out on plain carbon steel S45C with carbide tool. Cutting tests were conducted in the sealed chamber of which the atmosphere was changeable. Nitrogen, argon, carbon dioxide gases and air were used as the atmosphere.

著者

小林 直樹 田村 俊世 湊 小太郎

出版者

公益社団法人 日本生体医工学会

雑誌

生体医工学 (ISSN:1347443X)

巻号頁・発行日

vol.51, no.1, pp.31-37, 2013-02-10 (Released:2013-09-10)

参考文献数

8

---

In the principle model of pulse oximetry, the measured absorbance change occurs by a thickness change of the arterial blood. However, we cannot explain the absorbance change of the tissue only by thickness change of the arterial blood when we consider these three phenomena of circulatory dynamics:1) arterial blood flows into the tissue as pulsatile flow, 2) Oxygen saturation decreases by oxygen consumption in the tissue, and 3) venous blood flows out from the tissue. In this study, we made a new electrical model of pulse oximetry and examined the mechanism of the absorbance change when the height of the hand is changed. We measured absorbance ratio and SpO2 at three vertical hand positions, 1) on the table (middle), 2) rise over the head (up), 3) lowered (down), with six healthy volunteers. The absorbance ratios increased in the lowered hand position and there was an error to underestimate SpO2. The mean ± SD of SpO2 in the 6 subject at the middle, up, and down positions were 98.0 ± 1.28, 98.4 ± 0.84, 96.3 ± 1.69(%), respectively. We simulated pulse oximetry using our new electrical model, and we were able to express a mechanism to increase the absorbance ratio at the lowered hand position.

著者

小林 直樹 濱田 雅美

出版者

公益社団法人 日本生体医工学会

雑誌

生体医工学 (ISSN:1347443X)

巻号頁・発行日

vol.51, no.1, pp.17-23, 2013-02-10 (Released:2013-09-10)

参考文献数

13

---

Visual induced motion sickness (VIMS) due to real videos (passive videos) has been well evaluated by using a set of RR intervals (RRI) on electrocardiograms (ECG). However, in case of the estimation of VIMS for interactive videos suchas video games, it is difficult to obtain a stable VIMS index by using only RRI because of several modulation factors by respiration and personal errors among individual operations. For the evaluation of VIMS on interactive videos we propose VIMS quantification indices that use principal component analysis (PCA) of two time-variant biosignals, RRI and respiration signal (RESP), respectively. As VIMS indices we introduced frequency components of a score (rr) and a score (resp), which are time-variant scores resulting from PCA of the biosignals. The experimental results were estimated by regression analysis between the proposed indices and simulator sickness questionnaire (SSQ) or global motion vectors (GMVs) of videos. The experimental results show that a positive correlation is shown between the index of the score (rr) frequency analysis and SSQ for both passive and interactive videos. Because there are no significant difference between the indices for interactive video and for passive videos, the index does not influence operation factors, and reflects biomedical influence caused by video features such as GMVs. This means that the index calculated by score (rr) is effective for quantifying the VIMS caused by video factors, even though the dispersion of the index caused by the subject's individuality is not sufficiently small. This index also influenced the individuality of the subject's game habituation. On the other hand, there is little correlation between the index of the score (resp) frequency analysis and SSQ for each type of video. As a dependency of the operation and personal errors might be included in this index, we need to study more detail about this component.

著者

小林 直樹 藤原 ゆみ 金子 芳洋

出版者

環境衛生研究会

雑誌

ジ-ピ-ネット (ISSN:13414690)

巻号頁・発行日

vol.54, no.1, pp.48-56, 2007-04

著者

小林 直樹

雑誌

老年歯科医学 (ISSN:09143866)

巻号頁・発行日

vol.21, no.2, pp.81-85, 2006

著者

岩間 太 五十嵐 淳 小林 直樹

出版者

一般社団法人情報処理学会

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.48, no.4, pp.48-61, 2007-03-15

---

ファイルやメモリなどの計算資源がプログラム中でどのように使用されるかを型を用いて推論するための手法が五十嵐,小林らにより提案されている.彼らの手法では,各計算資源に対して起こりうるアクセス列の集合を使用法表現と呼ばれる式として推論する.しかしながら,推論された使用法表現が表すアクセス列の集合が,仕様として許されるアクセス列からなる言語に包含されているかどうかを判定するアルゴリズムが考案されておらず, 計算資源使用法検証の完全な自動化は達成できていなかった.本論文では,ある特定の言語クラスに属する仕様に対し,そのような包含判定を行うための健全かつ完全なアルゴリズムを提案する.仕様として任意の正則言語を許す場合には,包含判定問題は決定不能なので,我々のアルゴリズムが扱う仕様のクラスは,1つの入力記号について,遷移元および遷移先の状態がたかだか1つしか存在しない有限オートマトンが受理する言語のクラスとして与えられ,正則言語のクラスより小さい.しかしながら,ファイルなど現実の計算資源の仕様の多くは,我々のアルゴリズムで扱える言語のクラスに属する.したがって,本論文のアルゴリズムを五十嵐と小林らによる従来の研究と組み合わせることにより,ファイルなど多くの計算資源の使用法検証を自動化できる.In our previous work, we have developed a type-based method for inferring how resources such as files and memory are accessed in a program. Due to the lack of an algorithm for deciding whether the inferred resource usage conforms to the specification, however, it was not possible to verify automatically that resources are accessed according to the specification. In this paper, we propose a sound and complete algorithm for deciding the conformance of the inferred resource usage to the specification. Since the language denoted by the inferred resource usage belongs to a class larger than the class of the context-free languages, the class of specifications that our algorithm can deal with is smaller than the class of regular languages. Fortunately, however, that language class contains many of the typical resource usage specifications used in practice. Thus, by combining our algorithm with our previous method for resource usage inference, we can automatically check whether each resource is accessed according to the specification in many cases.

著者

秦泉寺 久美 渡辺 裕 岡田 重樹 小林 直樹

出版者

一般社団法人電子情報通信学会

雑誌

電子情報通信学会論文誌. D-II, 情報・システム, II-パターン処理 (ISSN:09151923)

巻号頁・発行日

vol.84, no.5, pp.758-768, 2001-05-01

参考文献数

13

被引用文献数

15

---

新しい画像符号化標準のMPEG-4が標準化されつつある。これは、低いレートにおいてはH.26XやMPEG-1,2に代表される従来符号化法と比較してより高品質の画像を提供するものである。また、新しい機能であるオブジェクト単位の符号化を提供するものである。筆者らはインターネット等に適用できる超低ビットレート符号化方法の開発を行っている。従来法に比べて劇的な符号量削減が可能であるMPEG-4の符号化ツールである「スプライト符号化」に着目し、前景、背景の2層からなるビデオオブジェクトの自動抽出アルゴリズムを提案する。生成した前景、背景のビデオオブジェクトをそれぞれMPEG-4オブジェクト符号化並びにスプライト符号化に適用(スプライトモード)して、スプライトを用いないMPEG-4 Simple profileの符号化法(ノーマルモード)と比較検討を行った。特に、フレームレートや前景オブジェクトの割合を変化させ、符号量に与える影響を調査した。その結果、フレームレートに関係なく、前景比率が画面全体の10〜15%程度である場合にMPEG-4通常符号化方法の1/4〜1/2程度の符号量で同程度の画質を実現できることを確認した。また超低レート(128kbit/s、64kbit/s)においてフレームレート、客観画質の評価を行ったところ、同程度のSNRで倍以上のフレームレートを達成できることを確認した。

著者

小林 直樹 石橋 聡 一之瀬 進

出版者

一般社団法人映像情報メディア学会

雑誌

映像情報メディア学会技術報告 (ISSN:13426893)

巻号頁・発行日

vol.23, no.3, pp.33-38, 1999-01-21

---

MPEG-2 transcoding scheme is proposed as scalable transmission system for a video-on-demand system is described. In this system video contents encoded by MPEG-2 are transmitted to receiver terminals via communication lines that have different bit rate. A transcoding technique that directly converts a bit stream encoded by MPEG-2 into a lower coding rate stream without decoding is proposed. The transcoder called Trampeg includes size reduction and frame drop approach. The experimental results show that an MPEG-2 stream of 6 Mbps is able to be transcoded into a stream of 1.5 Mbps-300 Kbps.