数理解析研究所講究録902 巻 1995 年 133-144

133

Towards a Formal Framework for Multimedia DataandTheir Players With

京都大学数理解析研究所 田辺誠$\mathrm{Q}\mathrm{o}\mathrm{S}$(Makoto TANABE)

京都大学数理解析研究所 中島玲二 (Reiji NAKAJIMA) *要旨

マルチメディア・システムに要求される重要な機能の一つは, 連
続データ演奏を与えられた$\mathrm{Q}\mathrm{o}\mathrm{S}$で実現することの可否を, 分析する能力である. 本稿では, マルチメディア・システムを論ずるための形式的な枠組を導入する. まず, 連続データ演奏に必要となる資源を扱うため, 時間区間と実行能力 (計算能力や通信能力など) の二つの次元を持つ構造を概念化する. これを用いて,$\mathrm{Q}\mathrm{o}\mathrm{S}$を満足する連続データ演奏の実現可能性を形式化する. 実現可能性の推論規則を導入することにより, メディア間の同期制御, 演奏の部分共有などの, マルチメディアシステムの種々の性質を論ずることが可能となる.
$*${$\mathrm{t}\mathrm{a}\mathrm{n}\mathrm{a}\mathrm{b}\mathrm{e},$reii }$\mathrm{i}$$@\mathrm{k}\mathrm{u}\mathrm{r}\mathrm{i}\mathrm{m}\mathrm{S}$.kyoto-u.

$\mathrm{a}\mathrm{c}$.jp

134

1

はじめに

マルチメディア. システムとは 7.

1.1

近年の, CPU の高速化やディスクの大容量化などのハードウェア技術の発達は, コンピュータの, マルチメデイアシステムとしての利用をうながした $[1, 6]$ . 動画データ, 音声データなどのメディアデータの演奏を, コンピュータによって制御・統合することが可能となったのである.
マルチメディア. システム (以後, システムと呼ぶ) とは何であるか ? 利用者は,システムに連続データの演奏要求を行なう. 演奏要求には, 演奏時間 (duration) の指定やメディア間の同期指定等, 様々な時間的制約が含まれる. 利用者は通常, 演奏データを指定すると同時に, 行なわれる演奏の質についての要求も行なう ($\mathrm{Q}\mathrm{o}\mathrm{S}$の指定).

$\mathrm{Q}\mathrm{o}\mathrm{S}$の指定は, システムにさらなる制約を課す. システムは, 課された要求と利用可能な資源 (CPU 能力, ネットワークの帯域幅など) を解析し,演奏が実現可能であれば適切な資源を確保し, 演奏を実行する. 演奏が実現不可能であれば利用者にその旨を伝え, 要求 p 変更をうながす.
マルチメディア・システムをリアルタイムシステムの $-$ つに位置付けることは可能であるが, マルチメディアシステムに課せられる時間的制約は, これまでの, 管制塔の飛行機管理, エレベーター制御[2] などにおける時間的制約とは, 基本的に異なる性質を持つ. それは,制約の内容が時間的な連続性を持つことである. 例えば, 「動画デー
タの,15 フレーム毎秒以上の滑らかさを保持したままの 10 秒間の演奏」 は, 10 秒間に渡る連続した制約としてのとらえ方が自然である.
では, マルチメディア. システムにおいて, 何が本質的な問題となるか 7.

135$\mathrm{Q}\mathrm{o}\mathrm{S}$の保証$\mathrm{Q}\mathrm{o}\mathrm{S}$を満足する演奏を得ることが, システムの利用者にとっての第–義である. 従って, 連続データの演奏を扱う際には,$\mathrm{Q}\mathrm{o}\mathrm{S}$を利用者に保証することが重要となる.

資源の確保質の高い演奏を実現するためには, CPU, ネットワークな.

どの資源を適切に利用することが必要である.
$\mathrm{Q}\mathrm{o}\mathrm{S}$

従って, 利用者にを保証するためには資源をあらかじめ確保することが必要となる.

時間区間の構造上述のように, 連続データの演奏要求は, 時間区間に渡る連続的な制約を生み出す. 従って, データ演奏, 資源等を形式化する際には, それらに時間区間としての構造を与えることが望ましい.

演奏の共有複数の利用者が, 同 $-$ の演奏の共有を要求することがある.
このような共有演奏を取り扱うことも, システムには要求される.

1.2$\mu$-logic の概観

マルチメディアシステムの問題を形式的に論ずるための枠組として, 以下の特徴を持つ$\bullet$$\mu$-logic を導入する.

連続データの演奏要求を, 形式的に扱う. これまでにも, 連続データを扱うフォ一マルシステムとして, ペトリネットによるシステムがあった [3].

これは, 演奏時間の固定された連続データをペトリネットのノードに, 複合データの並列合成, 逐次合成をノードの合成に, それぞれ対応させるものである.
り入れた

. と,

$\mathrm{c}$$\mathrm{Q}\mathrm{o}\mathrm{S}$指定の概念を取

演奏時間の固定されない連続データを扱うことも可能としたことが,$\mu$-logic の特徴である.

136$\bullet$

演奏に必要となる資源を, 時間区間と実行能力 (計算能力や通信能力) の二つの次元を持つ構造 (“連続資源”) として概念化し, その性質の記述に区間論理 [5] を応用した.

$\bullet$

利用可能な資源と$\mathrm{Q}\mathrm{o}\mathrm{S}$を満足する連続データ演奏との関係を, “実現可能性” として形式化し, その推論規則も与えた. 特に, 共有演奏の実現可能性について議論ができることが -logic の特徴であ
$\mu$

る.

マルチメディア演奏の例を挙げる.

Restricted

例 1:$\mathrm{B}\mathrm{l}\mathrm{o}\mathrm{c}\mathrm{k}\mathrm{i}\mathrm{n}\mathrm{g}\mathrm{s}[4]$

圧縮動画データ

データ解凍などの演奏準備の間, 静止画
例2:$\mathrm{T}\mathrm{V}$

ニュース放映の共有にひきつづき, 地方ニュース$\mathrm{Q}\mathrm{o}\mathrm{S}$以下のを演奏する.の表示を行なう.

中央の放送局が, 全国ニュース $N$$N_{A}$

を中継放送した後, 地方ニュース2$M_{1}$$M_{2}$

を放映する. 地方の放送局は, $N$$N_{B}$を放送する.

を満足する連続データ演奏$A_{1},$ $A_{2}$のように, 演奏データとその$\mathrm{Q}\mathrm{o}\mathrm{S}$を指定する記述を,“演奏記述” (performance description) と呼ぶ.

$A_{1}$:. 静止画像データ$M_{1}$の表示を 32.000 色で行なう.

演奏の持続時間は特に指定しない.
$A_{2}$:

圧縮動画データ$M_{2}$の演奏を 256 色以上で行なう.

演奏時間は短くて 10 秒, 長くて 15 秒とする.

また, 毎秒 10 フレーム以上の表示を要求する.

137

演奏記述を合成するためのオペレータを定義する.
$D::=A|(D_{1}||D_{2})|(D_{1}; D_{2})|D^{\mu}|(D_{1}\wedge D2)$

ここで, “ $A$ ” は上例の“ $(D_{1}||D_{\wedge}\zeta).)$ ”$A_{1},$ $A_{2}$のようなプリミティブな演奏記述,

は, 同 $-$ の時間区間上でのを指定する演奏記述, “ $(D_{1}; D_{2})$ ” は,$D_{1},$$D_{2}$$D_{1},$ $D_{2}$双方の実現 (区間同期)

双方の隣あった区間上での実現 (逐次実行) を指定する演奏記述, “ $(D_{1}\wedge D_{2})$ ” は,の実現を指定する演奏記述である. また, 同 $-$ の識別子

$D_{1},$ $D_{2}$$\mu$

双方の付いた複数の演奏記述の出現は, それらが同 $-$ の演奏によって実現されることを指定する.
記述例例 1 の静止画データ,$N_{A},$$N_{B}$$M_{-1}$と動画データの演奏記述がそれぞれ$A_{1},$$A_{2}$$M_{2}$, 例 2 のニュース $N$ ,, Global,$LoCa\iota_{A},$$Loca\iota_{B}$で与えられているとする. 例 1, 例 2 において要求される演奏は,それぞれ演奏記述“$(A_{1} ; A_{2})$”

及び“$((Global^{\mu}; L_{\mathit{0}}Ca\iota A)\wedge(Globa\iota^{\mu}; L_{\mathit{0}}Ca\iota_{B}))$で表される. ここで識別子$\mu$”

は, 二箇所に出現する演奏記述 Globalが, 同 $-$ のニュース放映によって満たされることを指定する.

3演奏に必要となる資源-連続資源

演奏記述は, 演奏データに加え, 演奏の$\mathrm{Q}\mathrm{o}\mathrm{S}$をも指定する. 従って, 演奏記述を満たすためには, 一定の時間区間に渡って, 適切なコンピューティング資源, ネットワーク資源などを確保することが必要となる.

ある時間区間に渡って, 計算能力や通信能力などを連続的に提138

供する資源を, 連続データに対応して “連続資源” あるいは

“プロセッサ” (processor) と呼ぶ.

演奏記述の実現に必要となるプロセッサは, ‘ヴロッセッサ記述”(processor description) を用いて記述する. プロセッサ記述は多くのオペレ一タを持つため, 各々の定義を記すことはしない. 図 1 を参照されたい.

.

$\mathrm{T}\mathrm{i}\mathrm{m}$

図 1: プロセッサ記述

プロセッサ記述の例として,$A_{1},$ $A_{2}$の実現に必要であり, かつ,と同 $-$ 区間に存在するプロセッサの記述を考える.

“$A_{1},$ $A_{2}$同 $-$ 区間である”

ことは, 4 節の “演奏の実現可能性” を取り扱う上で重要である.
$\bullet$$A_{1}$の実現に必要なプロセッサの記述

静止画の書き込みに必要なプロセ 7ッサの記述を$R_{1}$とする.

$A_{1}$の実現にはこのプロセッサのみが必要であるため, 求めるプロセッサ記述は,($R_{1}\mathrm{N}$True)となる. ここで “ True” とは, 任意のプロセッサによって満たされ139るプロセッサ記述である.
$\bullet$$A_{2}$の実現に必要なプロセッサの記述

動画の解凍と演奏に必要なプロセッサの記述をとし, 解凍に 10$R_{2}$秒間かかるとする. この時求めるプロセッサ記述は,$(Measure_{1\text{。}}\triangleright R_{2})$となる.

ここで $Measure_{10}$とは, 10 秒間の区間幅を持つ任意のプロセッサによって満たされるプロセッサ記述である.

4演奏の実現可能性と推論規則
演奏記述とプロセッサ記述との関係を,$\mu$-logic では演奏の実現可能性 (playability) として以下のように導入する.

:.

$[R]D$

$R$

$r$

:

$\langle R\rangle D$

$R$

$r$
-を満たす任意のプロセッサ$r$を用いて,と同 $-$ の区間上での $D$ の実現が可能.

を満たすあるプロセッサ$r$を用いて,と同 $-$ の区間上での $D$ の実現が可能.

$P::=[R]D|\langle R\rangle D|P_{1}\wedge P_{2}$であり、〈乃とは, 実現可能性$P_{1}$$P_{1},$$P_{2}$が共に保証されていることを示す.
$\mu$1の-logic には実現可能性の推論規則がいくつか用意されている. 例$A_{1}’,$$A_{2}$とすると,の実現可能性をそれぞれ “ $[R_{1}\mathrm{N}True]A_{1}$$(A_{1} ; A_{2})$”.’“$[Measure\iota 0\triangleright R_{2}]A2$の実現可能性は図 4 のように推論される. ここで、プロセッサ記述 $(R_{1}\ R_{2})$ は,$R_{1}$と$R_{2}$の双方を満たすプロセッサを記述する.

この推論は, 直観的には図 3 のようにとらえられる.

”

140

$Measure_{10arrow}:^{\pi}:True$$[R_{1}\dot{\mathrm{N}}.\cdot\dot{T}rue:]A_{1}$:.

$\cdot$$\overline{.\frac{[R_{1}\mathrm{N}Measure_{10}]A1[Measure_{10}\triangleright R2]A2}{[(R_{1}\mathrm{N}Measure_{1}0)\mathrm{N}(Measure_{10}\triangleright R2)](A_{12}A)}}.,[;]$. $\overline{.[R_{1}\mathrm{N}R’]2(A_{1}\cdot,A_{2})}$
ここで, $R_{2}’\equiv_{d}efs(Measure_{1}0\mathrm{N}True)\ R_{2}$($R_{2}$を満たし, 10 秒間以上の区間幅を持つプロセッサーの記述)

図 2: $(A_{1} ; A_{2})$ の実現可能性

特に, 規則 [;] について説明する.

$\frac{[R_{1}]D_{1}[R_{2}]D2}{[R_{1}\mathrm{N}R_{2}](D_{1}\cdot D_{2})},[;]$

実現可能性 $[R_{1}]D_{1},$ $[.R_{2}]D_{2}$ が与えられた時, これらを用いて実現可能性$[R_{1}\mathrm{N}R_{2}](D_{1}; D_{2})$.

を保証することが可能である.

なぜなら,$R_{1},$ $R_{2}$をそれぞれ満たす二つのプロセッサが隣あった区間上に与えられたな

らば, その各々を用いて$D_{1},$ $D_{2}$の実現が可能, すなわち, $(D_{1;}D_{2})$ の実現が可能となるからである.

5. 共有演奏
共有演奏の実現可能性を推論するための規則を導入する.

:.

:.

$\pi$

$\frac{[R]D\mathcal{E}(R)}{[R^{+a}]D^{\mu}\wedge\langle R^{-}a\rangle D^{\mu}}$[sharing]

141

図 3: $(A_{1)}A_{2})$ の実現可能性(ここで, 識別子 $a,$$\mu$

は, この規則の適用毎に新しいものを用意する.

また, $\mathcal{E}(R)\equiv((R\otimes True)\Uparrow True)$ は, $R$ を満たすプロセッサが少な
ぐとも -つは存在することを表す. )この規則を, 例 2 の実現可能性の推論への適用に即して説明する.
全国ニュースの演奏記述 “Global” の実現可能性が “与えられているとする.

$[Net]G\iota_{\mathit{0}}ba\iota$”

で

ここで, “Net” は, ニュースの放映に必要となる (ネットワーク) 資源のプロセッサ記述である. この実現可能性に“[sharing] 規則” を適用することによって, 実現可能性“”$[Net^{+a}]Globa\iota\mu\wedge\langle Net^{-}a\rangle G\iota obal\mu$を得る.

これは, 次のように説明される.
$\bullet$

全国局, 地方局がそれぞれ実現可能性$P_{1}\equiv[Net^{+a}]G\iota_{\mathit{0}}ba\iota^{\mu},$$\bullet$$P2\equiv\langle Net^{-a}\rangle G\iota oba\iota\mu$を得る.

Global の二箇所の出現に付加された識別子 “ ” は, 二つの記述 “Global”$\mu$142が同 $-$ のニュース放映によって満たされることを指定する.
$\bullet$

全国局は, Net を満たす任意のプロセッサによるニュース放映を行なうことが可能であるため,$P_{1}$の様相は “ $[]$ ” となっている. $-$方, 地方局は放映の中継を行なうのみであるため, Net を満たすどのプロセッサをニュース放映に用いるかを決定できない. 従って,$\bullet$となる.

$P_{2}$の様相は “$P_{1}$

中の Ne 垣こ付加された識別子 $”+a$ ” は, Net を満たすプロセッ”$\langle\rangle$

サを全国局が確保せねばならないことを示す.

$-$ 方, 乃中の Netに付加された識別子 $”-a$ ” は, Net を満たすプロセッサが全国局によって確保されるため, 地方局にはこれを確保する必要がないことを示す.

6

おわりに

本稿では, マルチメデイ組として,$\mu$$\text{ア}$・システムを形式的に論じるための枠-logic を導入した. 今後の課題を挙げる. まず, 演奏の実行中にマウス操作によって演奏速度を変更するなどの, 動的な演奏を扱うための拡張が考えられる. また,$\mu$-logic は抽象度の高い枠組であるため, 実際のプログラミングのためにはより具体的なモデルが必要となろう. このようなモデルを考察し,ていきたい.
題である.

$\mu$$\mu$-logic への対応づけを行なっ-logic の表現力, 整合性などの理論的な考察も今後の課

143

参考文献
[1] : マルチメディアネットワーク QOS の発想が基盤技術を再構
築, Nikkei Electronics, No. $583(1993)$ , pp. 39-92.

[2] Hale, R.: Using Temporal Logic for Prototyping: The Designof a Lift Controller, Temporal Logic in Specification (LNCS398), Altincham,$\mathrm{U}\mathrm{K}$, Apri11987, pp. 375-408.

[3] Little, T. D. and Ghafoor, A.: Spatio-Temporal Compositionof Distributed Multimedia Objects for Value-Added Networks,

COMPUTER, (1991), pp 42-50.
[4] Steinmetz, R.: Synchronization Properties in Multimedia Systems, IEEE Journal on Selected Areas in Communications,Vol. 8,$\mathrm{N}\mathrm{o}$. 3(1990), pp 401-412.

[5] VENEMA, Y.: A Modal Logic for Chopping Intervals, Journalof Logic of Computation, Vol. 1,No. 4(1991).
[6] 船渡大地, 徳田英幸: Real-Time Mach 3.0 における連続メディア
サーバの実験 –QOS 制御を取り入れた Quick Time Player の評

価, 情報処理学会研究報告 (IPSJ $SIG$ Note8), 71993.

144

Appendix :$\mu$-logic の推論規則.

Deduction rules of playabilities are given as follows.のaxiom$\frac{[R]D\mathcal{E}(R)}{\langle R\rangle D}\langle\rangle$$[R]A$

where,::$[R_{1}]D$$\pi$$\mathcal{E}(R)\equiv_{d\mathrm{e}fs}$((R\otimes True)&True).

$R_{1}arrow \mathrm{J}\pi$$R_{2}arrow R_{1}\pi \mathrm{r}$$\langle.R_{1}\rangle D$$\rceil$$\frac{R_{2}arrow R_{1}}{[R_{2}]D}[arrow]$$\frac{[R\mathrm{i}D\mathcal{E}:(R:\pi)}{[R^{+a}]D^{\mu}\wedge\langle R^{-}a\rangle D^{\mu}}$

where, identifiers$\frac{\langle R_{1}\rangle DR_{1}arrow R2}{\langle R_{2}\rangle D}(arrow\rangle$[sharing]$a\in\Sigma_{\pi},$$\mu\in\Sigma_{\delta}$$\frac{\{R\rangle D:}{\langle R^{+a}\rangle D^{\mu}\wedge\langle R^{-}a\rangle D^{\mu}}\langle_{Sha.r}ing\rangle$

are selected uniquely

at eachtime of applications of these rules.
$\frac{[R^{\dotplus a}]D\mathcal{E}(\dot{R})\pi}{[R^{+a}]D^{\mu}\wedge\langle R^{-}a\rangle D^{\mu}}[sharing+]$$\frac{\langle R^{\dotplus a}\rangle D:}{\langle R^{+a}\rangle D^{\mu}\wedge\langle R^{-}a\rangle D^{\mu}}\langle sharing+$$\frac{\langle R^{-a}\rangle D:}{\langle R^{-a}\rangle D^{\mu}\wedge\langle R^{-}a\rangle D^{\mu}}$$\frac{\langle R_{1}\rangle D_{1}\wedge\langle R_{2}\rangle D_{2}}{\langle R_{1}\otimes R_{2}\rangle(D1\wedge D2)}\wedge$$\langle$sharing-..
$.. \frac{[R_{1}]D_{1}[R_{2}]D2}{[R_{1}\Uparrow R2](D_{1}||D_{2})}.[||]$::$[R_{1}^{\cdot}.]D_{1}$$[.\cdot]D_{2}\text{タ_{}2}$$. \cdot.\frac{[R_{1}]D_{1}\langle R_{2})D:2\dot{R}_{2^{arrow}}(\tau_{r}ue\triangle R_{1}):\pi}{\langle R_{1}\phi R_{2})(D1||D_{2})}..\langle||\rangle$$\frac{\iota^{-\cdot\perp}\mathrm{J}-1\iota^{-4}\mathrm{J}^{-}\Delta}{[R_{1}\mathrm{N}R_{2}](D_{1}\cdot D_{2})}.,[;]$$. \cdot\frac{(R_{1}\rangle D_{1}:[R2]D_{2}R_{1}arrow(R\sim\pi\triangleleft R_{2})}{\langle R\rangle(D_{1};D_{2})}.\cdot..\cdot..(;]$$. \cdot\frac{[R_{1}]D_{1}\langle R_{2}\rangle::D_{2}R2arrow(\dot{R}1\triangleright R)\pi}{\langle R\rangle(D_{1}\cdot D_{2})}.\cdot,\cdot.\cdot[;\rangle$