数理解析研究所講究録
第 1744 巻 2011 年 1-10

1

実時間最終状態受理式決定性限定 1 カウンタ変換器の多項式時間等価性判定アルゴリズム
若月 光夫 *

1

富田悦次 i

清野 和司 \dag er

まえがき西野哲朗 \S

らは，多項式時間内で等価性判定を可解とする条件の追求を行っている．文献 [12] では，dpdt の部分クラス

決定性プッシュダウンオートマトン (dpda) の等価性判定問題は，Senizergues により，任意のクラスに対する可解性が示されている ([8]). しかし，そのアルゴ

文献 [11] のアルゴリズムを対象 dpdt 対に特化して単リズムは非常に複雑な方式である．dpda の等価性判定

純化することにより，その等価性判定が多項式時間では，オートマトンや形式文法を基礎とするシステムの学習過程などにおいて主要な役割を果たすことができる ([9] 等). 従って，その効率化に対して，多項式時間内で等価性判定が可能なアルゴリズムの実現は非常に重要である．

である，実時間空スタック受理式決定性限定 1 カウン
タ変換器 (実時間空スタック受理式 droct) について，解決できることを証明した．また，文献 [14] では，文献 [12] のアルゴリズムを拡張することによって，ある条件下での -推移を許した空スタック受理式 droct 対$\epsilon$に対しても，多項式時間で等価性を判定できることを示した．受理記号列集合部分が本質的に正則を超える
ような変換器に対する等価性判定が多項式的に行える

筆者らは，分岐アルゴリズムと名付けた単純で直接的な等価性判定手法を提唱してきた ([2], [5] 等). この手法を用いることにより，状態が単一という制限を持
つ単純決定性プッシュダウンオートマトン同士，あるいは，スタック記号が単一という制限を持っ決定性限
定 1 カウンタオートマトン同士について，その等価性判定を多項式時間で解決するアルゴリズムを得ている([4], [6], [7]).

の対象 dpdt のクラスとは比較不能な関係にある，単純
決定性プッシュダウン変換器同士の等価性判定が多項式的に行えることを示しているが，thickness(文献 [4]参照) をパラメータの一つとして用いており，これは対象とする変換器の記述長の指数オーダになり得る．

一方，dpda に出力機構を付与した決定性プッシュダ

本稿では，文献 [12] 等とは受理方式の異なる，実時

ウン変換器に対しても，その等価性判定に関する多くの成果が報告されている ([1], [8] 等). dpdt
は，受理非受理のみを判定する dpda に比較して，より実用的な意味を持ち重要であるが，その等価性判定
は一般に非常に複雑になる．ここでも，分岐アルゴリズ
ムを用いた簡単化の効果により，dpda の等価性判定と$(dpdt)$ほぼ同レベルの複雑さで dpdt の等価性判定を行うことができ，筆者らはこれまでに幾つかの単純なアルゴリ
ズムを示してきた ([3], [11], [12] 等).

特に，文献 [11]は，-推移を許した dpdt 対に対して，その等価性判定
可能な範囲を従来より大きく拡張した最新の成果であとの結果は，文献 [12], [14] の他には，文献 [lO] で示されているだけである．文献 [10] では，文献 [12], [14]間最終状態受理式 droct 対に対する等価性判定が多項
式時間で行えることを示す．

2

定義と表記法本稿で使用する定義と表記法は，文献 [2], [3], [11],[12] を基礎としているので，これらの文献を参照されたい．ただし，読み易さの観点から，必要に応じて同じ定義を本稿中にも再度記述するものとする．

$\epsilon$

り，現時点では，これを包含する結果は報告されていない．しかし，このアルゴリズムも最大手数としては指数関数的時間を要するものであった．そこで，筆者$*$

電気通信大学大学院情報理工学研究科\dagger 東芝ソリューション株式会社\ddagger 電気通信大学/ 中央大学研究開発機構\S 電気通信大学大学院情報理工学研究科

定義 2.1 (文献 [11], p.2676, 定義 2.1, 文献 [12],p.1189, 定義 2.1 参照)
dpdt $T$ を次のように表記$T=(Q, \Gamma, \Sigma, \Delta, \mu, q_{0}, Z_{0}, F)$する．
. ここで， は状$Q$態集合， はスタック記号集合， は入力記号集合，$q0$ は初期状態，
は出力記号集合， は推移規則の集合，$F(\subseteq Q)$ は最終状態の集合をは初期スタック記号，$\Gamma$$\Sigma$$\Delta$$\mu$$Z_{0}$$T$ が空スタック受理式の場合，表す．なお，$F=\emptyset$と2
明示して表すこととし，さもなければ， は最終状態
受理式とする．更に， の要素は， $q\in Q,$ $A\in\Gamma$ ,$T$$(p, A)arrow(q, \theta)a/z$
に対して，
の各々は
のような形式をとる．ここで，$a\in\Sigma\cup\{\epsilon\},$$z\in\Delta^{*},$$\theta\in\Gamma^{*}$$z,$ $q,$である$a=\epsilon$

場合，この規則を -規則と呼び，このとき，いかなる$\epsilon$$z’\in$ム$*,$$(q’, \theta’)\in Q\cross\Gamma^{*}$

に対しても， の.

を失うことなく，-規則において$\theta=\epsilon$$\epsilon$

この状況を次のように表記する．
$(p_{1}, \alpha_{1})^{x}=_{T}^{/z}(rn)(p_{m+1}, \alpha_{m+1})$$x=a_{1}a_{2}\ldots a_{m},$ $z=z_{1}z_{2}\ldots z_{m}$ .
ただし，

$\mu$

なる規則は含まない．一般性

要素に $(p, A)^{a’/z’}arrow(q’, \theta’)$$(p_{rr\iota}, \alpha_{m})^{a_{n1}/z_{m}}arrow(p_{m+1}, \alpha_{m+1})\tau$$p,$ $A,$ $a$$\theta$の組に対して一意に定められる．また，$a’\in\Sigma,$

...,

$p,$

$\mu$

なお，便宜上，$m=0$ の場合を次のように定める．

とおける．更$(p_{1}, \alpha_{1})^{\epsilon}=_{T}^{/\epsilon}(0)(p_{1},\alpha_{1})$に，dpda $M=(Q, \Gamma, \Sigma, \delta,q_{0}, Z_{0}, F)$ を，dpdt

$T$

の随

伴 dpda と呼ぶ．ここで， は次のような推移規則の集同様に，dpdt

合である．

表記する．

$\delta$$\delta=\{(p, A)arrow^{a}(q,\theta)|(p, A)arrow(q,\theta)a/z\in\mu\}$.

$\epsilon$

定義 22(文献 [12], p.1189, 定義 22 参照)

ある$\Gamma=\{Z_{0}\}$dpda $M=(Q, \Gamma, \Sigma, \delta, q_{0}, Z_{0}, F)$ について，である場合，dpda $M$ を決定性限定 1 カウンタオー

restricted one-counter automaton; droca) と呼ぶ．同様に，ある dpdt $T=$
でについて，を決定性限定 1 カウンタ変換ある場合，dpdt
器 (deterministic restricted one counter transducer;
droct) と呼ぶ．また，上記のように，droct の出力$M$ をの機構を取り除いた droca が $M$ となる場合，
随伴 droca と呼ぶ．
トマトン (deterministic$\Gamma$$=$の随伴 dpda $M$ に関して次のように$(p_{1},\alpha_{1})=_{M}^{x}(m)(p_{m+1},\alpha_{m+1})$

なお，推移規則に -規則を一切含まない場合，そのdpda, dpdt は実時間であるという．

$(Q, \Gamma, \Sigma, \Delta, \mu, q_{0}, Z_{0}, F)$$T$.

$\{Z_{0}\}$

更に，ある$\alpha’’\in\Gamma^{*}$$\alpha_{i}=\alpha_{i}’\alpha’’,$$\alpha_{i}’\in\Gamma^{+},$.

が存在して，各ステップにおいて，$1\leq i\leq m+1$である場合，$|\not\in\Gamma$

なる記号を用いて，次のように表記する．
$(p_{1},\alpha_{1}’|\alpha’’)^{x}=_{T}^{/z}(m)(p_{m+1}, \alpha_{m+1}’|\alpha’’)$.

同様に， の随伴 dpda $M$ に関して次のように表記$T$する．
$(p_{1},\alpha_{1}’|\alpha’’)=_{M}^{x}(m)(p_{m+1}, \alpha_{m+1}’|\alpha’’)$.

$T$$\cdot$$T$$T$

定義 23(文献 [Il], pp. $267t\succ\cdot 2677$ , 定義 22, 文献 [12],dpdt $T$ の計算状況
pp.1189-1190, 定義 23 参照)
を $(p, \alpha)\in Q\cross\Gamma^{*}$ と表記する．ここで，記号列$\alpha$の$\alpha=A\alpha’’,$ $A\in$
左端をスタックの先頭とする．また，$\Gamma$としたとき，計算状況$(p, A)arrow(q, \theta)a/z\in\mu$$(p, A\alpha’’)$に，ある推移規則が適用されて dpdt $T$ が 1 ステップ

なお，上記の各$(p, A\alpha’’)arrow(q, \theta\alpha’’)a/zT^{\cdot}$

同じく，その随伴 dpda に関して次のように表記する．

は省略することもある．

定義 24(文献 [11], p.2677, 定義 24, 文献 [12],に出力記号列 $w,$ $h,$p.1190, 定義 24 参照)$h^{-1}w=t$, あるいは，
ついて，$w=ht$ である場合，$t\in\Delta^{*}$$wt^{-1}=h$ とも表記する．また，出力記号集合

関して，$\Delta^{-*}$

および$\Delta^{\pm*}$$\Delta^{-*}=\{h^{-1}|h\in\Delta^{*}\},$

お，$\Delta^{-*}-\{\epsilon\}$$h\in\Delta^{\pm*}$

を，$\Delta^{-+}$$\Delta$$\Delta^{\pm*}=\Delta^{*}\cup\Delta^{-*}$. なと表記する．更に，改めて，$k^{-1}\in\Delta^{-*},$, および，

として，以下の$||h||=|h|$ ,のとき，$k\in\Delta^{*}$

ような記号列長を定義する．

$h\in\Delta^{*}$$||h||=|k|$ .
のとき，$|k^{-1}|=-|k|$.

定義 25(文献 [11], p.2677, 定義 25, 文献 [12],p. 1190, 定義 25 参照) 実時間最終状態受理式 dpdt
$T$ の計算状況
こ対して以下を定義する．なお， の随伴 dpda を $M$ とする．
$(p, \alpha)\in Q\cross\Gamma^{*}\ovalbox{\tt\small REJECT}$

$T$

$a$

$(p, A\alpha’’)arrow(q,\theta\alpha’’)M^{\cdot}$$N(p, \alpha)=\{x\in\Sigma^{*}|$

次に，ある $p_{i}\in Q,$$\alpha_{i}\in\Gamma^{+},$$a_{i}\in\Sigma\cup\{\epsilon\},$$z_{i}\in\Delta^{*}$,$(p, \alpha)=_{M}^{x}(q, \epsilon)$

I $\leq i\leq m,$ $p_{m+1}\in Q,$
に対して，次のような 1 ステップ推移が $m$ 回連続する系列を考える．

for some $q\in Q$ }.

$\alpha_{m+1}\in\Gamma^{*}$$L(p, \alpha)=\{x\in\Sigma^{*}|$$a_{2}/z_{2}$$a_{1}/z_{1}$$(P1)\alpha_{1})arrow(p_{2})\alpha_{2}),$$T$$(p_{2},$$\alpha_{2})arrow(p_{3},$ $\alpha_{3})$
$T$

,

に

を次のような集合と定義す

る．

$h=k^{-1}\in\Delta^{-*}$

推移する状況を次のように表記する．

$(m)$ ”$(p, \alpha)=_{M}^{x}(q, \beta)$

for some $q\in F,$$\beta\in\Gamma^{*}$}.

3
TRANS $(p, \alpha)=\{x/y\in\Sigma^{*}\cross\Delta^{*}|$$(p, \alpha)^{x}=_{T}^{/y}(q, \beta)$(i)for some $q\in F,$$\beta\in\Gamma^{*}$(ii) TRANS

}.

(3)

$N(M)=N(q_{0}, Z_{0}),$ $L(M)=L(q_{0}, Z_{0})$ ,ここで，特に，TRANS $(T)=$ TRANS$(q_{0}, Z_{0})$と定義する．

$q\in Q,$

$A\in\Gamma,$$\alpha’’\in\Gamma^{*}$$(p, \alpha)\subseteq$$N(p, \alpha)=\emptyset$$(i)\sim(iii)$(i)$(p, \alpha\beta)$

ならば，任意の.

$\beta\in\Gamma^{*}$

に対して，次が成立する．

,(ii) $L(p, \alpha)=L(p, \alpha\beta)$ ,FIRST $(p, \alpha)=\{a\in\Sigma|(p, A)arrow^{a}(q, \theta)\in\delta$,$\alpha=A\alpha’’,$

の

,
TRANS

$L(p, \alpha)\subseteq L(p, \alpha\beta)$$N(p, \alpha\beta)=\emptyset$.

(iii) TRANS $(p, \alpha)=$ TRANS(1) については，文献 , Lemrna 31 参照．
(2), (3) については，定義 25 から得られる．口$(p, \alpha\beta)$, for some

(証明)$\theta\in\Gamma^{*}\}$

$[6|$

$T$ の
$|\alpha’|\leq|Q|$
上記の補題 31(1), (3) (i) より，
なる，
各計算状況
についてだけ，$FIRST_{live}(p, \alpha)$$(p, \alpha’)\in Q\cross\Gamma^{*}$$N(p, \alpha’)\neq\emptyset$

か否かをあらかじめ調べておけば， の任意の計算状$T$況 $(p, \alpha)\in Q\cross\Gamma^{*}$ について，$N(p, \alpha)\neq\emptyset$

か否かは直ちに判定できる．このような手続きは， の記述長に$T$$=\{\begin{array}{l}(p\not\in F \text{のとき} ) :\{a\in FIRST (p, \alpha)|(p, \alpha)=_{M}^{a}(q, \beta),L(q, \beta)\neq\emptyset, for sonle q\in Q, \beta\in\Gamma^{*}\},(p\in F \text{のとき} ) :\{a\in FIRST (p, \alpha)|(p, \alpha)=_{M}^{a}(q, \beta),L(q, \beta)\neq\emptyset, for soriie q\in Q, \beta\in\Gamma^{*}\}\cup\{\epsilon\}.\end{array}$

関する多項式オーダの時間で行える．
補題 32

実時間最終状態受理式 droct $T$$(Q, \Gamma, \Sigma, \Delta, \mu, q_{0}, Z_{0}, F)$の計算状況 $(p, \alpha)\in Q\cross\Gamma^{*}$

定義 26 (文献 [11], p2678, 定義 26, 文献 [12],Pp. 1190-1191, 定義 26 参照)
実時間最終状態受理
式 dpdtとすの計算状況を，各々る．また，その随伴 dpda をとする．ここで，$T_{1},$$(p, \alpha),$$T_{2}$$M_{1},$なる$L(M_{1})=L(M_{2})$ であると等価式で表記する．また，き，両 dpda は等価であるといい，$M_{1}\equiv M_{2}$と表記する．さもなくば，非等価であるといい，$M_{1}\not\equiv M_{2}$$h\in\Delta^{\pm*}$であることを，$(p, \alpha)\equiv h(\overline{p}, \beta)$

る．ここで，ある合，この等価式は$k\in\Delta^{*}$に対$\beta\in\Gamma^{*}$

して，

(3.1)

$(p, \alpha)^{x}=_{T}^{/z}(q, \beta)$$(\overline{p},$なる推移が存在するならば，ある$\Delta^{*},$$\beta’\in\Gamma^{*}$$x’$$\Sigma^{*},$

$\in$

$z’$

$\in$

$n\leq|Q|(|Q|-I)$ を満たす，に対して，$(p, \alpha)=_{T}x’/z’(n)(q, \beta’)$(証明)

文献 [7], Lemma 3.1 の証明と同様にして得られる．口$\beta)\}$

上記の補題 32 より，(31) の推移が存在するならば，なる等価式で表記すについて $h=k^{-1}$ である場

$k(p, \alpha)\equiv(\overline{p}, \beta)$$q\in Q,$

なる推移が存在する．

$(\overline{p}, \beta)$$=\{x/hv|x/v\in$ TRANS$z\in\Delta^{*},$

と

に対して，

TRANS $(p, \alpha)=h$ TRANS$x\in\Sigma^{*},$$M_{2}$$(p, \alpha)\equiv(\overline{p}, \beta)$

表記する．更に，について，ある$(\overline{p}, \beta)$

であることを，$L(p, \alpha)=L(\overline{p}, \beta)$$=$

とも表記する．また，TRANS $(T_{1})=$ TRANS
であるとき，両 dpdt は等価であるといい，乃と表記する．さもなくば，非$(T_{2})$

任意の $q\in F$ に対し，$|x’|\leq|Q|(|Q|-1)$ を満たす，$(p, \alpha)=_{T}(q, \beta’)x’/z’(x’\in\Sigma^{*}, z’\in\Delta^{*}, \beta’\in\Gamma^{*})$

る推移が存在する．従って，計算状況$|Q|(|Q|-1)$$(p, \alpha)$

な

から長さ

以下の入力記号列により，最終状態をも$T_{1}\equiv$

等価であるといい，$T_{1}\not\equiv T_{2}$3と表記する．

$T$である．

さて，等価性判定の対象とする実時間最終状態受理

実時間最終状態受理式 droctの計算状況 $(p, \alpha)\in Q\cross\Gamma^{*}$
$T$

$=$

$(Q, \Gamma, \Sigma, \Delta, \mu, q_{0}, Z_{0}, F)$について，次の (1)(I)$|\alpha|\geq|Q|$$\sim(3)$に対して $N(p, \beta)\neq\emptyset$(2) 任意の$\beta\in\Gamma^{*}$$T_{1}=(Q_{1}, \Gamma_{1}, \Sigma, \Delta, \mu_{1}, q_{01}, Z_{01}, F_{1})$ ,式 droct 対を，$T_{2}=(Q_{2}, \Gamma_{2}, \Sigma, \Delta, \mu_{2}, q_{02}, Z_{02}, F_{2})$とし，各々から出力機構を取り除いた droca (随伴 droca) をが成立する．

かつ $N(p, \alpha)\neq\emptyset$ ならば，任意の$L(p, \alpha)\neq\emptyset$

か否かを判定できる．また，この手続きが の記述長に関する多項式オーダの時間で行えることは，明らか前提および基本命題

補題 3.1つ計算状況へ推移するか否かを調べれば，$\beta\in\Gamma^{*}$.

に対して，次の (i), (ii) が成立する．

$M_{1},$$M_{2}$とする．

なお，文献 [7] において，任意の実時間最終状態受
理式 droca 同士の包含性判定を多項式時間で解決する4
アルゴリズムを得ており，これらの droca 対の等価性
判定自体は多項式時間内で判定できる．本稿では，上に対して事記 droct 対, 乃の随伴 droca 対に対前に等価性判定を行うことなく，droct 対
して直接，等価性判定を多項式時間内に行うことを考える．なお，以下では，スタック記号 $A\in\Gamma_{i}(i=1,2)$のスタック記号はを頻繁に使用するが， および$M_{1},$$T_{1}$$M_{2}$$T_{1},$$k_{i}(p, A)={\rm Max}\{{\rm Min}\{|w||(p, A)=^{w}(q, \epsilon)M_{1}$ ’$T_{2}$$T_{2}$$T_{1}$$N(p, A)\neq\emptyset$
また，
なる，ある $(p, A)\in Q_{i}\cross\Gamma_{i}(i=$に対して，以下の定数 $k_{i}(p, A)$ を定義する．

$1,2)$$Z_{0i}=A(i=1,2)$ であることそれぞれ 1 種類であり，$w\in\Sigma^{*}\}|q\in Q_{i}\}$更に，droca $M_{i}(i=1,2)$ に依存する，定数$p\in Q_{i},$であるとき，次の (i), (ii) が成立

する．

なお，

$w_{1},$$w_{2}\in\Delta^{*},$$P\in Q_{1},\overline{P}\in Q_{2}$,$\beta\in\Gamma_{2}^{*}$(3.2)

定の可解性は自明である．従って，以降では，$\rho\geq 2$

補題 3.3(3.3)$(q_{02}, Z_{02})=_{T_{2}}^{2}(\overline{p}, \beta)w/u)$$(p, \alpha)\equiv h(\overline{p},\beta)$

かっ$L(\overline{p}, \beta)\neq\emptyset$$h\in\Delta^{\pm*}$$\alpha’\in\Gamma_{1}^{*},$

であると$T_{1}\equiv T_{2}$であるとき，ある$u_{0},$ $u,$ $v_{0},$ $v\in\Delta^{*},$$\Sigma^{+},$$L(p, \alpha)\neq\emptyset$

を$\beta\in\Gamma_{2}^{+},$$x\in$$\alpha\in\Gamma_{1}^{+}$

,

に対して，

$\beta’\in\Gamma_{2}^{*}$$(q_{01}, Z_{01})^{xo/x/u}=_{T_{1}}^{u_{O}}(p,\alpha)=_{T_{1}}(p, \alpha’)$(3.4)

が成立する．

$(q_{02}, Z_{02})^{xo/vox/v}=_{T_{2}}(\overline{p},\beta)=_{T_{2}}(\overline{p}, \beta’)$であるとする．ここで，$N(p, \alpha)\neq\emptyset$$w_{1}’,$$x0\in\Sigma^{*},$$p\in Q_{1},\overline{p}\in Q_{2},$

が存在し，

.

(ii) 更に，ある $w’\in\Sigma^{*},$.

前提とする．

$(q_{01}, Z_{01})^{w/}=_{T_{1}}^{w_{1}}(p,\alpha)$

であり，更に，$w_{1}h=w_{2}$ なる，あるき，$A\in\Gamma_{i}\}$である場合は，その多項式時間等価性判$\rho\leq 1$(i) ある $w\in\Sigma^{*},$
に対して，$\alpha\in\Gamma_{1}^{*},$,$k_{i}={\rm Max}\{k_{i}(p, A)|N(p, A)\neq\emptyset$$T_{1}\equiv T_{2}$

を定義

する．

に留意されたい．
命題 31$k_{i}$.

$w_{2}’\in\Delta^{*},$$\alpha’\in\Gamma_{1}^{*},$$\beta’\in$

電に対して，(ii) が成立する．
(i)

.
ならば，
.
ならば，
(iv) が成立する．
(iii),のとき，次の
.
ならば，
.
ならば，
なる前提を考慮すれば，文献 [6],$|Q_{1}|\leq|\alpha|\leq|\alpha’|$(ii)$(q_{01}, Z_{01})^{w’/w_{1}’}=_{T_{1}}(p, \alpha’)$$|\beta|<|\beta’|$

また，のとき，次の (i),$|\beta|\leq|\beta’|$$|\alpha|\leq|\alpha’|$$N(\overline{p}, \beta)\neq\emptyset$(iii) $|Q_{2}|\leq|\beta|\leq|\beta’|$$(q_{02}, Z_{02})_{\tau_{2}}^{w’/w’}\overline{\overline{.}}(\overline{p}, \beta’)$

(iv)
(証明)

$|\alpha|<|\alpha’|$

であり，
なる，ある

$L(p, \alpha’)\neq\emptyset$$w_{2}’$$w_{1}’h’=$ならば，$h=h’$が成が存在し，かつ，

かつ$h’\in\Delta^{\pm*}$(証明)$T_{1}\equiv T_{2}$$L(\overline{p}, \beta’)\neq\emptyset$

立する．

まず，(i) について考える．式 (3.4) が不成立

ならば，定義 26 から，直ちに
乃となる．従って，その対偶として式 (3.4) の成立が保証される．(ii)が同様に成立するため，については，$h=h’$ が得られる．口定義 25, 補題 31(2) から，$|\alpha|\leq|\alpha’|$$|\beta|\leq|\beta’|$Lemma 3.2 の証明と同様にして得られる．口
補題 34$\Delta^{*},$$T_{1}\equiv T_{2}$$p\in Q_{1,\overline{p}}\in Q_{2},$であるとき，ある$\alpha\in\Gamma_{1}^{*},$$\beta\in\Gamma_{2}^{*}$$x\in\Sigma^{*},$ $u,$ $v\in$に対して，$T_{1}\not\equiv$$(q_{01}, Z_{01})^{x}=_{T_{1}}^{/u}(p,\alpha)$$(p, \alpha’)\equiv h’(\overline{p}, \beta’)$

定義 3.1$T_{1},$$T_{2}$$(q_{02}, Z_{02})^{x}=_{T_{2}}^{/v}(\overline{p},\beta)$に依存する各種定数を定義する．
であるとする．このとき，$\tau_{i}={\rm Max}\{|z||(p, A)arrow(q, \theta)a/z\in\mu_{i}\},$$(i=1,2)$$FIRST_{live}(p, \alpha)=FIRST_{live}(\overline{p}, \beta)$$\rho_{i}={\rm Max}\{|\theta||(p, A)arrow(q, \theta)a/z\in\mu_{i}\},$$(i=1,2)$が成立する．

これらの定数より，$\tau={\rm Max}\{\tau_{1}, \tau_{2}\},$と定義する．

$\rho={\rm Max}\{\rho_{1}, \rho_{2}\}$(証明)$T_{1}\equiv T_{2}$なる前提を考慮すれば，文献 [6],Lemma 3.3 の証明と同様にして得られる．口54

p. 1195, 定義 41 参照)

等価性判定アルゴリズム
等価性の判定は，文献 [2] 等のアルゴリズムと同様に，

実時間最終状態受理式 droct 対$T_{1}$,$T_{2}$の初期計算状況に対する等価式 $(q_{01}, Z_{01})\equiv(q_{02}, Z_{02})$ を唯一の節点 (根)とする判定木から，後述の “分岐”’“跳越し”’“スタック縮減” の各操作により，逐次その子節点を導入することによって判定木の展開を行なう．ここで，判定木中の節点は，unchecked, checked, skipping, s-checkedの 4 つの状態 (status) をとる．そして，unchecked
状態，あるいは skipping 状態の節点が存在する間は，
unchecked 状態の節点があれば，その中でサイズの最も小さいものに，さもなければ，skipping 状態の節点の中でサイズの最も小さいものに，順次着目す

る．節点のサイズとは，節点$({\rm Max}\{|\alpha|, |\beta|\}, {\rm Min}\{|\alpha|, |\beta|\})$$(p, \alpha)\equiv h(\overline{p}, \beta)$の場合，なる数値対で定義し，その大小関係は，まず 1 つめ (左側) の数値の大小関係とし，これが等しい場合は，2 つめ (右側) の数値の大小関係で決定するものとする．
さて，推移 (32), (33) に対応して，節点 (34) が判定
木中に導入され，その成立性が着目されたとする．こ$P\in F_{1}$ かっ
こで，である場合，
乃ででなければあるためには，定義 25, 26 より，ならない．このチェックを “終端チェック” と呼ぶ．ま

現時点までに展開された判$T(T_{1} :T_{2})$ 中に 2 節点
定木を $T(T_{1} :T_{2})$ で表す．
,$(p_{1}, \alpha_{1}\gamma_{1})\equiv h_{1}(\overline{p}_{1},\overline{\alpha}_{1}\overline{\gamma}_{1})$$(p_{2}, \alpha_{2}\gamma_{1})\equiv h_{2}(\overline{p}_{2},\overline{\alpha}_{2}\overline{\gamma}_{1})$が存在し，$(p_{1}, \alpha_{1})^{x_{1}/u_{1}}=_{T_{1}}(p_{2}, \alpha_{1}’)$

かつ，$(\overline{p}_{1},\overline{\alpha}_{1})=_{T_{2}}(\overline{p}_{2},\overline{\alpha}_{1}’)x_{1}/v_{1}$ただし，$x_{1}\in\Sigma^{*},$$|\alpha_{1}’|\geq|\alpha_{2}|,$$u_{1},$ $v_{1}\in\Delta^{*},$$u_{1}h_{2}=h_{1}v_{1}$,$|\overline{\alpha}_{1}’|\geq|\overline{\alpha}_{2}|$のような推移対に対応して，この両節点が，$u_{1}\backslash x_{1}/v_{1}$”をラペルとする枝で結ばれた親子関係にある場合，次のように記述する．
$<(p_{1}, \alpha_{1}|\gamma_{1})\equiv h_{1}(\overline{p}_{1},\overline{\alpha}_{1}|\overline{\gamma}_{1})>arrow^{u_{1}\backslash x_{1}/v_{1}T(T_{1}:T_{2})}$$<(p_{2}, \alpha_{2}|\gamma_{1})\equiv h_{2}(\overline{p}_{2},\overline{\alpha}_{2}|\overline{\gamma}_{1})>$.

更に，このような親子関係が，$T_{1}\equiv$$\overline{p}\in F_{2}$$<(p_{i}, \alpha_{i}|\gamma_{1})\equiv h_{i}(\overline{p}_{i},\overline{\alpha}_{i}|\overline{\gamma}_{1})>_{\vec{T(T_{1}:T_{2})}}^{u_{i}\backslash x_{l}/v_{i}}$$h=\epsilon$

た，判定木中に$(p, \alpha’)\equiv h’(\overline{p}, \beta’)$

している場合，$T_{1}\equiv T_{2}$$<(p_{i+1}, \alpha_{i+1}|\gamma_{1})\equiv h_{i+1}(\overline{p}_{i+1},\overline{\alpha}_{i+1}|\overline{\gamma}_{1})>$

なる節点が既に存在

ただし，$u_{i}h_{i+1}=h_{i}v_{i},$であるためには，命題 31 よ$h=h’$ でなければならない．このチェックを出力
り，$(1\leq i\leq m)$のように連続する場合，次のように記述する．

の “一意性チェック” と呼ぶ．このいずれかのチェック$<(p_{1}, \alpha_{1}|\gamma_{1})\equiv h_{1}(\overline{p}_{1},\overline{\alpha}_{1}|\overline{\gamma}_{1})>^{u}=^{\backslash x/v}$と判定を下が不成立である場合，直ちにし，全手続きを終了する．着目節点 (34) が，この両$T_{1}\not\equiv T_{2}$”$T(T_{1}:T_{2})$$<(p_{m+1},\alpha_{rn+1}|\gamma_{1})$チェックの対象外である場合に，後述する “分岐” , “跳越し” , “スタック縮減” の各操作の適用を検討する．な$\equiv h_{m+1}(\overline{p}_{m+1},\overline{\alpha}_{m+1}|\overline{\gamma}_{1})>$

お，着目節点 (34) に対する終端チェックが成立し，かつ $FIRST_{live}(p, \alpha)=FIRST_{live}(\overline{p}, \beta)=\{\epsilon\}$$x=x_{1}x_{2}\ldots x_{m},$ $u=u_{1}u_{2}\ldots u_{m}$ ,
ただし，

である場

合，または，節点 (3.4) と同じラベルの unchecked 状態
ではない節点が判定木中に既に存在している場合，節点 (3.4) の状態を checked にする．

なお，式 (34) のような節点を判定木中に導入する
時点で，まずは後述の “基礎チエック” の成立性を調べる．ある節点に対する基礎チェックが不成立である場

合，補題 33, 34 より
乃が成立するため，直ちにと判定を下し，全手続きを終了する．
と判定され以上の手順において，途中でることなく，unchecked 節点も skipping 節点も存在しとの判定を下す．
なくなった場合，‘$v=v_{1}v_{2}\ldots v_{m}$.

$T(T_{1}:T_{2})$ 中のこれを，なお，上記の各
4.1

”

‘(
$|$

による推移路と呼ぶ．
は省略することもある．
$x\in\Sigma^{*}$

基礎チェック$T_{1}\not\equiv$$T_{1}\not\equiv T_{2}$”$T_{1}\not\equiv T_{2}$$T_{1}\equiv T_{2}$””

定義 4.1 (文献 [11], pp.2683-2684, 定義 41, 文献 [12],定義 42

現時点までに展開された判定木を $T(T_{1}$ :$T(T_{1}:T_{2})$ 中の節点につで表す．
いて，次の条件 (i), (ii) が成立するか否か調べる操作を$T_{2})$$(p, \alpha)\equiv h(\overline{p}, \beta)$

基礎チェックと呼ぶ．

(i) $FIRST_{live}(p, \alpha)=FIRST_{live}(\overline{p}, \beta)$ .
(ii) $N(p, \alpha)\neq\emptyset$ またはの場合，ある$N(\overline{p}, \beta)\neq\emptyset$

6$x’,$ $x”\in\Sigma^{+},$ $u’,$ $u”,$ $v’,$ $v”\in\Delta^{*},$$\alpha’\in\Gamma_{1}^{+},$$\beta’\in\Gamma_{2}^{+}$

に

対して，

43

分岐

本アルゴリズムでは，判定木中に節点が導入された時点で 41 の基礎チェックを行っているため，着目節$<(q_{01}, Z_{01})\equiv(q_{02}, Z_{02})>=u’\backslash x’/v’$$FIRST_{li}ve(p, \alpha)=$点 (3.4) に対して，
FIRSTlive$T(T_{1}:T_{2})$$(\overline{p}, \beta)$

が成立している．

$<(p,\alpha’)\equiv h(\overline{p},\beta’)>=u’’\backslash x’’/v’’T(T_{1}:T_{2})$$<(p,\alpha)\equiv h(\overline{p}, \beta)>$

補題 41(文献 [11], p.2683, 補題 41, 文献 [12],pp. 1194-1195, 補題 41 参照) 判定対象の droct , 乃のある計算状況対に対して，等価式 (3.4) が成立することと，次の (i), (ii)
$T_{1}$

なる推移路が存在するならば，次の (a), (b) が成立す
る．

(a)

.

(b)

$N(p, \alpha’)\neq\emptyset$

のとき，

ならば，
.
ならば，

$|Q_{1}|\leq|\alpha’|\leq|\alpha|$$|\beta’|\leq|\beta|$$N(\overline{p}, \beta’)\neq\emptyset$(i) 全ての

ならば，
.
ならば，

$|Q_{2}|\leq|\beta’|\leq|\beta|$$|\alpha’|<|\alpha|$$a_{i}\in$

FIRSTlive$|\alpha’|\leq|\alpha|$.

$(p, \alpha)=$

FIRSTl$ive(\overline{p}, \beta)$

における推移対，$=\{a_{1}, a_{2}, \ldots, a\downarrow\}\subseteq\Sigma$のとき，$(\overline{p}, \beta)\in Q_{2}\cross\Gamma_{2}^{+}$

が成立することは同値である．

.

$|\alpha’|\leq|\alpha|$$|\beta’|<|\beta|$$(p, \alpha)\in Q_{1}\cross\Gamma_{1}^{+},$

かつ$(p, \alpha)arrow(p_{i}, \alpha_{i})a_{l}/u_{l}T_{1}$$(\overline{p}, \beta)arrow(\overline{p}_{i}, \beta_{i})a_{2:}T_{2}^{/v}$$|\beta’|\leq|\beta|$に対して，ある適当な$h_{i}\in\Delta^{\pm*}$$u_{i}h_{i}=hv_{i}$が存在して，

が成立する．

42(ii) 上記 (i) の場合に対して，以下が成立する．

スタック縮減節点$(p, \alpha)\equiv h(\overline{p}, \beta)$

に対して，$N(p, \alpha)=\emptyset$

かつき，補題 31 より，$(p,\alpha’)=$る
TRANSが存在し，TRANS$N(p, \alpha’)=\emptyset$$1\leq|\alpha’|\leq|Q_{1}|$$\alpha’\in\Gamma_{1}^{+}$

が成立する．同様に，$N(\overline{p}, \beta)=\emptyset$$|\beta’|\leq|Q_{2}|$

TRANS

かつ

$N(\overline{p}, \beta’)=\emptyset$$(\overline{p}, \beta’)=$

TRANS

なる

$(\overline{p}, \beta)$$(p_{i},\alpha_{i})\equiv h_{i}(\overline{p}_{i},\beta_{i}),$であるとな$(p, \alpha)$(証明)$1\leq i\leq l$

.

(4.1)

文献 [lI], 補題 41 および [12], 補題 41 の証

明と同様にして得られる．口であるとき，$1\leq$$\beta’\in\Gamma_{2}^{+}$

が存在し，上記の補題 41(i) の成立性チェックを，“分岐出力チェック” と呼び，チェック成功であるとき，全てのが成立する．

後述する分岐操作と跳越し操作だけでは，判定木が無限に展開して終端しない場合がある．そこで，上記のような場合には，次のスタック縮減操作を適用する．

$i$に対する等価式 (41) を節点 (34) の子節点として加え，着目節点の状態を checked にする．このとき，各々の枝”とする．この操作を分岐と呼ぶ．
”となお，分岐出力チェックが不成功のとき，のラペルを$u_{i}\backslash a_{i}/v_{i}$$T_{1}\not\equiv T_{2}$

現時点までに展開された判定木を $T(T_{1}$ :定義 43$T(T_{1}:T_{2})$ 中の着目節点で表す．
に対して，まず，次の (i), (ii) を行う．

$(p, \alpha)\equiv h(\overline{p}, \beta)$$T_{2})$

判定を下し，全手続きを終了する．
着目節点 (34) に分岐が適用されたとき，その子節点の個数は高々$|\Sigma|$である．

$N(p, \alpha’)=\emptyset$(i) $N(p, \alpha)=\emptyset$ の場合，
なる，最短の$\alpha’\in\Gamma_{1}^{+}$

(ii)

を

$\alpha_{0}$とする．
とする．さもなければ，の場合，なる，最短の$\alpha_{0}=\alpha$

44

跳越し

$N(\overline{p}, \beta’)=\emptyset$$N(\overline{p}, \beta)=\emptyset$

または $|\beta_{0}|<|\beta|$ が成立する場

上記の分岐操作とスタック縮減操作だけでは，判定
木が無限に展開して終端しない場合がある．そこで，文に対してスタック縮減操作

献 [3] 等と同様に跳越しを導入する．なお，以降，現時が適用可能であるという．このとき，等価式
を着目節点の子節点として加え，着目節点の点までに展開された判定木を $T(T_{1}:T_{2})$ で表すことと$\beta’\in\Gamma_{2}^{+}$

を$\beta_{0}$とする．さもなければ，$\beta_{0}=\beta$

ここで，
合，節点

$|\alpha_{0}|<|\alpha|$$(p, \alpha)\equiv h(\overline{p}, \beta)$とする．

$(p, \alpha_{0})\equiv$$h(\overline{p}, \beta_{0})$状態を checked にする．また，これら節点間の枝ラベ“,とする．この操作をスタッ
ク縮減と呼ぶ．なお，枝ラベル中の
は，-推

ノレを “

$\epsilon\backslash \epsilon(\lambda)/\epsilon$$(\lambda\not\in\Sigma)$“$\epsilon(\lambda)$““$\epsilon$

定義 44(跳越しの前提条件 : 文献 [11], p.2684, 定義
4.2, 文献 [12], p. 1195, 定義 4.2 参照) 着目節点 (3.4)$\epsilon$

移ではないことを明示するために便宜上使用しているだけであり，混乱のない限り，単に “する．

と表記する．

が次のように書き表せるとする．
$(p,\omega_{1}\alpha’’)\equiv h(\overline{p},\omega_{2}\beta’’)$

.

(4.2)

7
ただし，

$\alpha=\omega_{1}\alpha’’,$または$\beta’’\neq\epsilon$$\beta=\omega_{2}\beta’’$. 更に，であり，かつ，$T(T_{1}:T_{2})$$\alpha’’\neq\epsilon$

路の中で最も短い入力記号列とする．同様に，この時中に既に分岐が適用

点の $T(T_{1}:T_{2})$ において可能な限り後続節点の追加をされた，$(p,\omega_{1})\equiv h(\overline{p},\omega_{2})$(4.3)$(\omega_{1}\in\Gamma_{1}^{+}, \omega_{2}\in\Gamma_{2}^{+})$

なる節点が存在し，$N(p, \omega_{1})\neq\emptyset$

かつ

(4.4)

$|\omega_{1}|\geq|Q_{1}|$行い，着目節点の状態を skipping にする．その後，節点 (34) に再度着目して跳越しを適用しても，新たな後続節点が追加されず，かつ，後続節点との間の枝ラ
ベルの更新も行われなかった場合，着目節点の状態を
s-checked にする．また，以後判定木が変化する度に，全ての s-checked 節点の状態を kipping に戻して跳越$s$$N(\overline{p}, \omega_{2})\neq\emptyset$

かつ

(4.5)

$|\omega_{2}|\geq|Q_{2}|$であるとき，着目節点 (34) は跳越しの前提条件を満足しているという．ここで，(44) および (45) の条件を満足する，サイズの最も小さい節点 (43) を，この跳越しの “対応節点” と呼ぶ．
定義 45(跳越し適用の可否 : 文献 [11], p.2684, 定義
4.3, 文献 [12], pp.1195-1196, 定義 43 参照)
着目
節点 (34) が跳越しの前提条件を満足しており，更に，ある $x_{0}\in\Sigma^{+},$$\Gamma_{1}^{*},$$\gamma_{02}\in\Gamma_{2}^{*}$$u_{0},$$v_{0}\in\Delta^{*},$$q\in F_{1},\overline{q}\in F_{2},$しの適用可能性を常に監視し，必要に応じて後続節点の追加を行う．
着目節点 (34) に跳越しが適用されたとき，その子節
点 (後続節点) の個数は高々 $|Q_{1}||Q_{2}|$ である．

4.5

等価性判定アルゴリズム

対象とする droct 対の等価性判定アルゴリズムの全手続きを以下に示す．

$\gamma_{01}\in$に対して，対応節点 (4.3) から，次の推移路が存在するとする．

Algorithm

あらかじめ，$1\leq|\alpha|\leq|Q_{1}|$$Q_{1}\cross\Gamma_{1}^{+}$(4.6)$<(p, \omega_{1})\equiv h(\overline{p},\omega_{2})>\frac{\underline{u_{0}\backslash }\ovalbox{\tt\small REJECT}^{x_{0}}/v}{T(T_{1}:T_{2})}$$\gamma_{01}=\epsilon$, または$\gamma_{02}=\epsilon$

または $1\leq|\gamma 01|\leq|Q_{1}|$ かつ $1\leq|\gamma_{02}|\leq|Q_{2}|$,.

このとき，上記推移路 (46) に対応した，着目節点 (34)の両辺の計算状況を起点とする，次の対となる推移$N(p, \alpha)\neq\emptyset$$\leq|\beta|\leq|Q_{2}|$に対して$<(q,\gamma_{01})\equiv(\overline{q},\gamma_{02})>$$u0=hv0$ かつ，
ただし，

に，I

に対して

なる各計算状況 $(p, \alpha)\in$

か否かを求める．同様

なる各計算状況$N(\overline{p}, \beta)\neq\emptyset$$(\overline{p}, \beta)\in Q_{2}\cross\Gamma_{2}^{+}$

か否かを求める．

判定木は，ラベルを$(q_{01}, Z_{01})\equiv(q_{02}, Z_{02})$とする，

unchecked 状態にある根だけから成るものとする．
if $L(q_{01}, Z_{01})=L(q_{02}, Z_{02})=\emptyset$then 根の状態を checked にする
else if 根に対する基礎チェックが失敗する”と判定を下す ; halt fi fithenwhile 判定木中に unchecked または skipping 状態の節点が存在する do
if 判定木中に unchecked 状態の節点が存在する
then 着目節点 $P$ を，unchecked 状態にある，最$T_{1}\not\equiv T_{2}$(4.7)$(p, \omega_{1}\alpha’’)^{x_{0}/u_{0}}=_{T_{1}}(q, \gamma_{1}\alpha’’)$$(\overline{p},\omega_{2}\beta’’)^{x_{0}/v_{0}}=_{T_{2}}(\overline{q}, \gamma_{2}\beta’’)$ただし，$|\gamma_{1}|\geq|\gamma 01|$

かっもサイズの小さい節点とする$|\gamma_{2}|\geq|\gamma_{02}|$が可能である．従って，対応節点 (43) から，(46) のような推移路が存在するとき，着目節点 (34) に対する
跳越しが適用可能であるという．

を，skipping 状態にある，最もサ
イズの小さい節点とする fielse 着目節点$P$のラベ) を $(p, \alpha)\equiv h(\overline{p}, \beta)$ とする$\triangleright$

し，更に，跳越しが適用可能 (定義 45) である場合，着目節点に対して跳越しを適用し，その子節点 (これを“後続節点，，と呼ぶ) として，(4.8)

を $T(T_{1}:T_{2})$ に取り入れ，そこへ至る枝のラベルを$u_{0}\backslash x_{0}/v_{0}$”$\overline{P}\not\in F_{2}$$T_{1}\not\equiv T_{2}$$\overline{p}\in F_{2}$$h\neq\epsilon$$T_{1}\not\equiv T_{2}$$(q, \gamma_{01}\alpha’’)\equiv(\overline{q}, \gamma_{02}\beta’’)$とする．ただし， は (4.6) のような推移$x_{0}$;かつかっ, または，
if”;と判定を下す halt
then
$p\in
F_{1}$
かつ
else ifthen if”と判定を下す ; halt fi fi
thenfi
if $P$ にスタック縮減操作が適用可能である$P$ を
then $P$ にスタック縮減操作を適用し，checked 状態にする (子節点 $P’$ は$P\in F_{1}$着目節点 (34) が跳越しの前提条件 (定義 44) を満足$P$$P\not\in F_{1}$$\overline{P}\in F_{2}$8unchecked 状態にある) ;
着目節点

$P$

を

$P’$

$(p, \alpha)\equiv h(\overline{p}, \beta)$odとし，そのラベルをとする$T_{1}\equiv T_{2}$fi

if $FIRST_{live}(p, \alpha)=FIRST_{live}(\overline{p}, \beta)=\{\epsilon\}$を checked 状態にする
then
else
if が unchecked 状態であるを，判定木中に存在する，ラペルを
then

5

$P$

および
の各々が真であるときの場合に分けて，本アルゴリズムが多項式時間内で終端することと，判定した結果が正しいことを証$T_{1}\equiv T_{2}$$S$とする $P$ 以外のunchecked 状態ではない節点の集合とする
を とする fielse$h’\neq h$ なる節点が存在する
中にifと判定を下す ; haltthenelse if 中に と同じラベルの節点が存在する$S$

終端性正当性および計算量評価
ここでは，

$P$

$(p, \alpha’)\equiv h’(\overline{p}, \beta’)$と判定を下す ;halt”$T_{1}\not\equiv T_{2}$

明する．

$\emptyset$

$S$

5.1

が真である場合$T_{1}\equiv T_{2}$”$T_{1}\not\equiv T_{2}$
$P$

$S$

$T_{1}\not\equiv T_{2}$という判定を下した場合，その判$T_{1}\equiv T_{2}$if 後続節点が追加されたか，ある後続節点との間の枝ラベルが更新されたおよび全ての s-checked 状態のelse $P$ を s-checked 状態にする fi
if 追加された $P$ の全ての後続節点に対して基礎チェックを行った結果，基礎$T_{1}\equiv T_{2}$$P$$T_{1}\equiv$$T_{1}\equiv T_{2}$が真であるとき，可能な限り展開された，全ての節点が checked 状態または s-checked

状態にある判定木を $T(T_{1}:T_{2})$ とする．このとき，次の $(i)\sim$ (iii) が成立する．

(i) $T(T_{1}:T_{2})$ 中の任意の節点をる．ここで，ある定数$(p, \alpha)\equiv h(\overline{p}, \beta)$とす$S_{1}=(\rho_{1}-1)(|Q_{1}||Q_{2}|+1)+|Q_{1}|$ ,$T_{1}\not\equiv T_{2}$

$P$

”

乃が
との判定を下す．以降，真である場合，本アルゴリズムは多項式時間の有限手数で終端することを証明する．

チェック失敗となった節点が存在する”と判定を下す ;haltthenfielse $P$ を skipping 状態にする fiに分岐出力チェックが成功する
else ifthen$P$ に分岐を適用し， をchecked 状態に(
子節点は全てする
unchecked 状態にあが真である場合，本アルゴリズムが有限終端した場合には，正しく

補題 5.1

節点を $skip\rho ing$ 状態にする$)$”

定は明らかに真である．この対偶より，に跳越しを適用し，必要に応じて後続節点を子節点として加える (追加された
後続節点は unchecked 状態にある) ;

る

”

義から，

$P$

then

が真であるとき，本アルゴリズム
はと判定を下し，多項式時間内の有限の手数で終端することを示す．まず，本アルゴリズムの定$T_{1}\equiv T_{2}$$T_{1}\equiv T_{2}$then $P$ を checked 状態にする
else if $P$ が跳越し前提条件を満足する
then if $P$ に跳越しが適用可能である
then

$P$

最初に，

$S_{2}=(\rho_{2}-1)(|Q_{1}||Q_{2}|+1)+|Q_{2}|$について，$|\alpha|\leq S_{1}$$||h||\leq\tau|Q_{1}||Q_{2}|$かつ$|\beta|\leq S_{2}$が成立する．また，が成立する．

(ii) $T(T_{1}:T_{2})$ 中の全ての節点の個数は，次の定数$S_{T}$

以下である．

;$S_{T}=|Q_{1}|(S_{1}+1)|Q_{2}|(S_{2}+1)$

全ての s-checked 状態の節点を $skip\psi ing$$\cross({\rm Max}\{|\Sigma|, |Q_{1}||Q_{2}|\}+1)$

状態に戻す;

if $P$ の全ての子節点に対して基礎チェックを行った結果，基礎チェック失敗と.

(iii) $T(T_{1} :T_{2})$ 中の任意の 2 節点間の枝ラベルを$u\backslash x/v$”とする．ここで，ある定数

なった節点が存在する

then
fl
else
fi fi fi fi$T_{1}\not\equiv T_{2}$$T_{1}\not\equiv T_{2}$”$S_{I}={\rm Max}\{k_{1}S_{1}, k_{2}S_{2}\}$と判定を下す ;hbalt

について，$|x|\leq S_{I},$”と判定を下す ; haltfi$|u|\leq\tau_{1}S_{I},$$|v|\leq\tau_{2}S_{I}$

が成立す

る．

(証明) (i) について，$|\alpha|\leq S_{1}$かっ $|\beta|\leq S_{2}$ が成立す

9ることは，定義 42 45 を考慮することによって，文献 [6], Leriima5.1 の証明と同様にして得られる．ま$\sim$に対して が一意に定また，状態対$||h||\leq\tau|Q_{1}||Q_{2}|$ が得られる．(ii) につることから，
いては，(i) および，分岐，跳越しの各操作による子節点の個数の上限から得られる．(iii) にっいて，枝ラベ$(p,\overline{p})\in Q_{1}\cross Q_{2}$

ル中の入力記号列適用された任意の節点$x\in\Sigma^{*}$$T_{1}\equiv T_{2}$,$|v|\leq\tau_{2}S_{I}$$\gamma\in\Gamma_{1}^{*}$$|Q_{2},$

なる推移が存在するならば，ある$\overline{\gamma}\in\Gamma_{2}^{*}$

が直ちに得られる．
$\square$$|\mu_{1}|,$$k_{1},$$|\mu_{2}|,$$x_{0}\in\Sigma^{*}$$\overline{q}\in F_{2}$,,$u_{0},$$v_{0}\in$に対して，$<(p, \alpha)\equiv h(\overline{p}, \beta)>\frac{\underline{uo\backslash }x_{0}\ovalbox{\tt\small REJECT}/v}{T(T_{1}:T_{2})}$$<(q, \gamma_{0})\equiv(\overline{q},\overline{\gamma}_{0})>$なる推移路が存在する．ただし，$|x_{0}|$

ダの時間内で完了することは容易に証明できる．ここ$k_{i}(i=1,2)$ については，文献 [I3], pp. 171I-l7l2,
で，Lemnla 10 より，が成立することが示さ,

ただし，$u=hv$,

なる推移が可能であり，更に，ある$\Delta^{*}$

に関する多項式オー$k_{2}$$v\in\Delta^{*}$

に対して，$(\overline{p}, \beta)^{x}=_{T_{2}}^{/v}(\overline{q},\overline{\gamma})$が真であるとき，判定木中の一つの節点に対$|\Sigma|,$

に対し，

(5.1)

する分岐，跳越し，スタック縮減の各操作がそれぞれ，$|Q_{1}|,$について，ある$(p, \alpha)^{x}=_{T_{1}}^{/u}(n)(q, \gamma)$$x$$|x|\leq S_{I}$ が成立する．よって，のに更新されるため，,,$(p, \alpha)\equiv h(\overline{p}, \beta)$$q\in F_{1}$$h$が最も長いのは，着目節点に跳越しが適用されたときであり，これは可能な限り短いも$|u|\leq\tau_{1}S_{I}$,$u\in\Delta^{*}$$hv_{0},$$|\gamma_{0}|\leq|\gamma|,$Claim$E_{n}$$|\overline{\gamma}_{0}|\leq|\overline{\gamma}|$$\leq$$u_{0}=$.

(I) $n=1$ のときの証明$|x|,$$x=a\in\Sigma$よ$k_{i}\leq p_{i}|Q_{i}|^{3}$

れている．また，判定木の展開に応じた跳越し被適用

節点に対する跳越し適用の見直し回数も，節点数 (多項式オーダ) 以下である．更に，判定木中の任意の節点$(p, \alpha)\equiv h(\overline{p}, \beta)$$L(p, \alpha)\neq\emptyset$

,

に対して，

$N(p, \alpha)\neq\emptyset,$および$N(\overline{p}, \beta)\neq\emptyset$,の各々が成立するか$L(\overline{p}, \beta)\neq\emptyset$

否かを調べることも，上記の定数に関する多項式時間内で完了できる．従って，$T_{1}\equiv$

アルゴリズム全体が，$|Q_{1}|,$

り，節点$|\Sigma|,$$|\mu_{1}|,$$|\mu_{2}|$(II)$E_{n+1}$$E_{1},$$E_{2},$$\ldots,$

次に，(1) 節点$(p, \alpha)\equiv h(\overline{p}, \beta)$”が分岐節点のとき

推移 (5.1)を次のように分割する．
$(p, \alpha)arrow(r, \alpha’)^{x’’/u_{(n)}’’}a/u’\tau_{1}\overline{\overline{\tau_{1}.}}(q, \gamma)$$x=ax”,$ $u=u’u”,$
ただし，$r\in Q_{1},$$\alpha’\in p_{1}+$. 節点

は分岐節点であるから，$(\overline{p}, \beta)arrow(\overline{r}, \beta’)a/v’T_{2}$が真である場合が真であるとき，本アルゴリズムはと判定を下し，多項式時間内の有限の手数$T_{1}\not\equiv T_{2}$$T_{1}\not\equiv T_{2}$が真であると仮定して，を考える．

$(p, \alpha)\equiv h(\overline{p}, \beta)$$T_{1}\not\equiv T_{2}$$E_{n}(n\geq 1)$に関する多項式時間内で終端する．

5.2には分岐が適用されている．

従って，題意を得ることは容易に証明できる．

乃が真であるとき，本$|Q_{2}|,$$(p, \alpha)\equiv h(\overline{p}, \beta)$

であり，かつ$<(p, \alpha)\equiv h(\overline{p}, \beta)>arrow^{T(T_{1}:T_{2})u’\backslash a/v’}$

乃がで終端することを示す．前節の証明から，真であるときも，明らかに，本アルゴリズムは多項式$T_{1}\not\equiv$

時間内で終端する．従って，以降 t
き，本アルゴリズムが誤って$T_{1}\not\equiv T_{2}$$(T_{1}\equiv T_{2}$

”

であると

との判定を下すことのないことを示す．
$T_{1}\not\equiv T_{2}$$T_{1}\not\equiv T_{2}$(証明)$Q_{2},$$\beta’\in\Gamma_{2}^{+}$

. 節点

”

跳越し節点のとき，が真であるとき，本アルゴリズと判定を下す．

た場合，$T_{1}\not\equiv T_{2}$$T_{1}\equiv T_{2}$”と判定を下すことなく終端しが真に成立することを証明する．そのためには，十分拡張され展開を止めた時点の判定木
を $T(T_{1}:T_{2})$ とし，任意の正整数$n(\geq 1)\ovalbox{\tt\small REJECT}$

こ対して，次の Claim $E_{n}$ が成立することを証明すれば十分である．
$E_{n}$$T(T_{1}:T_{2})$$(r, \alpha’)\equiv t(\overline{r}, \beta’)$$E_{n}$

本補題の証明のため，その対偶として，本アルゴリズムが

Claim

$u’t$
なる推移路が存在する．ただし，を得る．また，節点

補題 5.2ムは$<(r, \alpha’)\equiv t(\overline{r}, \beta’)>$

中の，分岐または跳越しが$=$$hv’,\overline{r}$$\in$が分岐節点またはを適用することによって題意$(r, \alpha’)\equiv t(\overline{r}, \beta’)$がスタック縮減節点のとき，その子節点には分岐が適用されており，その節点に$E_{n}$(2) 節点$(p, \alpha)\equiv h(\overline{p}, \beta)$を適用することによって題意を得る．

木中に対応節点$\Gamma_{1}^{+},$

が跳越し節点のとき

判定$(p, \omega_{1})\equiv h(\overline{p}, \omega_{2})(\alpha=\omega_{1}\alpha’’)\omega_{1}\in$$\alpha’’\in\Gamma_{1}^{*,\overline{p}\in}Q_{2},$$\beta=\omega_{2}\beta’’,$$\omega_{2}\in\Gamma_{2}^{+},$$\beta’’\in\Gamma_{2}^{*})$

が存在し，(46) のような推移路が存在する．また，(47)のような，対となる推移が可能である．推移 (51) が$(p,\omega_{1}|\alpha’’)^{x}=_{T_{1}}^{/u}(n+1)(q, \gamma_{1}|\alpha’’),$$\gamma=\gamma_{1}\alpha’’$10と表せる場合，対応節点に $E_{n+1}(1)$ を適用することによって題意を得る．また，推移 (51) が$(p,\omega_{1}|\alpha’’)^{x’/u_{(n’)}’}=_{T_{1}}(r, \epsilon|\alpha’’)$[5] E. Tomita, K. Seino, “The extended equivalence
problem for a class of non-real-time deterministic pushdown automata,” Acta Informatica 32,
395-413, 1995.

かっ$(r, \alpha’\prime^{x’’/u_{(n’’)}’’})=_{T_{1}}(q, \gamma)$$x=x’x”,$ $x’,$ $x”\in\Sigma^{+},$ $n’+$と表せる場合 (ただし，を$n”=n+1,$ $u=u’u”,$ $r\in Q_{1})$ , 対応節点に$E_{n’}$

適用した後，節点$(p, \alpha)\equiv h(\overline{p}, \beta)$の後続節点，あるいはその子節点 (後続節点がスタック縮減節点のとき) に$E_{n’’}$

を適用することによって題意を得る．口以上を総合して，次の定理を得る．
定理 5.1

実時間最終状態受理式決定性限定 1 カウン

タ変換器同士の等価性は，その状態集合，スタック記
号集合，入力記号集合，推移規則集合の各要素数に関する多項式時間内で判定可能である．

6

むすび
実時間最終状態受理式 droct 対に対して，その等価性判定が多項式オーダの時間で行えることを示した．より一般的な，-推移を許した最終状態受理式 droct 対に対しても，多項式時間内で等価性判定が行えるか否$\epsilon$

かを示すこと等は，今後の課題である．
謝辞

ムとその最大時間計算量，” 信学論 (D-I), $J74D-I$ ,9, 595-603, 1991.

本研究は科学研究費補助金基盤研究 (C) の支援を受けている．

[6] K. Higuchi, E. Tomita, M. Wakatsuki, “A
polynomial-time algorithm for checking the inclusion for strict deterministic restricted one.
counter automata,” IEICE Tkans. $Inf$. & Syst.,
E78-D, No.4, 305-313, 1995.
[7] K. Higuchi, M. Wakatsuki, E. Tomita, “Apolynomial-time algorithm for checking the inclusion for real-time deterministic restricted onecounter automata which accept by final state,”
IEICE Trans. $Inf$. & Syst., E78-D, No. $939-$
950, 1995.
$S,$[8] G. S\’enizergues, $L(A)=L(B)$ ? decidability results from complete formal systems,” Theoret.
Comput. Sci. 251, Issues 1-2, 1-166, 2001.
[9] Y. Tajima, E. Tomita, M. Wakatsuki, M. Terada, ”Polynomial time learning of simple deterministic languages via queries and a representative sample,” Theoret. Comput. Sci. 329, 203221, 2004.

[10] C. Bastien, J. Czyzowicz, W. Fraczak, W. Rytter, “Equivalence of simple functions,” Theolet.
Comput. Sci. 376, 42-51, 2007.

[11] 清野和司，富田悦次，若月光夫， -推移を許したある決定性プッシュダウン変換器対の等価性判
定，” 信学論 (D), J90-D, 10, 2675-2690, 2007.
$\epsilon$

参考文献[1] O.H. Ibarra, L.E. Rosier, “On the decidabilityof equivalence for deterministic pushdown transducers,“ $Inf$. Processing Letters 13, 89-93, 1981.
[2] E. Tomita, “A direct branching algorithm forchecking equivalence of some classes of deterministic pushdown automata,” Inform. Control 52,
I87-238, 1982.

[3] E. Tomita, K. Seino, “A direct branching algorithm for checking the equivalence of two deterministic pushdown transducers, one of which isreal-time strict,” Theoret. Comput. Sci. 64, 3953, 1989.
[4] 若月光夫，富田悦次，“単純決定性ブッシュダウン
オートマトンの等価性判定の改良分岐アルゴリズ[12] 清野和司，富田悦次，若月光夫，“実時間空スタッ
ク受理式決定性限定ワンカウンタ変換器の多項式時間等価性判定，” 信学論 (D), J91-D, 5, 1188-1201,

2008.
[13] M. Wakatsuki, E. Tomita, ”Polynomial time
identification of strict deterministic restricted
one-counter automata in some class from positive data,” IEICE Trans. $Inf$. & Syst., E91-D,
No.6, 1704-1718, 2008.

[14] 若月光夫，清野和司，富田悦次，西野哲朗，“空スタック受理式決定性限定ワンカウンタ変換器の多項式時間等価性判定アルゴリズム，” 2009 年度冬の LA シンポジウム資料 No.14, 1-10, 2010.