日本ソフトウェア科学会第 32 回大会 (2015 年度) 講演論文集

更新可能時間オートマトンの新たな拡張について
上里 友弥

南出 靖彦

本発表では，時間オートマトン（Timed automata）の拡張として知られる，更新可能時間オートマトン（Updatable
timed automata）について，その拡張となる新たな体系を導入し到達可能性問題の決定可能性を証明する．
従来の更新可能時間オートマトンでは，更新の形を限定されたものとした場合に限り，到達可能性問題が決定可能となることが示されている．仮に一般的な形の更新を許した場合には，チューリング完全となり問題は決定不能となる．我々は，新たな体系として，より一般的な更新形式を持つ代わりに，従来の対角線制約（diagonal constraints）
を弱めたものを提案する．この体系に対して新たな証明手法を用いることで，到達可能性問題の決定可能性を示す．
同時に我々の体系は，言語のクラスを拡大すること，すなわち，従来の時間オートマトンでは受理できなかった言語が扱えることも述べる．

We propose a new extension of Updatable Timed Automata (UTA), which extend the formalization ofstandard timed automata, and prove the decidability of the reachability problem of our new extension.
The decidability of the reachability problem for the original formalization of UTA was shown for very restricted sub-classes. This restriction is unavoidable because general UTA can simulate Minsky’s two-countermachines and are Turing-complete. By contrast, our formalization adopts another set of formulae and thismakes our system more expressive with respect to the decidable classes of UTA. Especially, we use a novel
technique to prove the decidability of the reachability problem of our updatable timed automata.

これは，状態 p とクロック x（その値を 0 とする）の

1 はじめに組 ⟨p, {x 7→ 0}⟩ から計算が開始され，1.2 秒経過した

時間オートマトンは，従来の有限オートマトンに，

ところで，イベント a をみたことを意味する．

時間の概念を付け加えたものである．

時間オートマトンの体系的な研究は，Alur と Dill

システムのモデル化の観点からは，有限オートマによる論文 [4] に端を発する．特にこの論文では，モ

トンとは，ある状態 p で，イベント a をみたときに，

デル検査で基礎となる判定問題「到達可能性問題」の

a

次にどの状態 q に移るか，を定める規則 p −→ q から

決定可能性（PSPACE 完全性）が証明された．そのなる計算モデルだといえる．一方で時間オートマトン

後も，時間オートマトンは実時間システムのための重は，直前のイベントと次のイベントの間の経過時間

要な計算モデルであるという認識のもと，非常に様々を考える．また，そのような時間概念を扱うために，な拡張が提案されてきている．これについては，例え従来の状態に加えて有限個の「クロック」を用いる．

ば [11] [18] などのサーベイが参考になる．

以下は時間オートマトンの計算の一例である：
1.2

a⟨p, {x 7→ 0}⟩ −−→ ⟨p, {x 7→ 1.2}⟩ −→ ⟨q, {x 7→ 1.2}⟩.
New Extension of Updatable Timed Automata.
Yuya Uezato, 筑波大学システム情報工学研究科, University of Tsukuba.
Yasuhiko Minamide, 東京工業大学大学院情報理工学研
究科, Department of Mathematical and Computing
Sciences, Tokyo Institute of Technology.

本論では，そのような拡張のうち，Bouyer らによって提案された「更新可能」時間オートマトン [7] と呼ばれる体系を，一層拡張する．時間オートマトンでは，クロック x の値を変更する操作として，その値を 0 にリセットする x := 0 のみが許されていた．一方，更新可能時間オートマトンは，リセット以外の操作—これを更新と呼ぶ—も許す拡張である．Bouyer

らによって研究された体系で到達可能性問題が決定可
能なものは，結果的には，従来の時間オートマトンと2 更新可能時間オートマトン

表現力が変わらないことが示されている [7] [6]．

更 新 可 能 時 間 オ ー ト マ ト ン（Updatable Timed

本論で提案する更新可能時間オートマトンでは，以Automaton，以下で UTA と略す）は，6 つ組 A =下の二点が重要である：(Q, qinit , F, X , Σ, ∆) であり，構成要素は以下の通り

1. 2 章に現れる Lab のような，従来の時間オートマ

である：

トンでは受理できない言語を受理できる．

2. 到達可能性問題が決定可能である．

• Q は状態の有限集合で，qinit ∈ Q と F ⊆ Q はそれぞれ，初期状態及び最終状態の集合を表す．

従って，我々の体系は，時間オートマトンの言語クラ• X はクロックの有限集合を表す．

スを超えた新しい更新可能時間オートマトンである• Σ は有限の入力アルファベットで，∆ は下で詳しといえる．

く見るが，遷移規則を定める有限の集合である．

到達可能性問題の決定可能性証明は，Well-Quasi-

UTA A の計算状況は ⟨q, ν⟩ で表され，q ∈ Q は現在

Ordering という非常に良い性質を持つ順序構造が，の状態，ν : X → Q≥0 は各クロック x ∈ X の現在の我々の体系に現れるということから導かれる．本論

値 ν(x) を保持する割当関数である．

で与える証明は，近年精力的に研究が行われているa,ϕ,up

各遷移規則は p −−−−→ q ∈ ∆ の形をとり，p, q ∈ Q

Well Structured Transition System (WSTS) と呼ばは状態で，入力文字 a ∈ Σ を読んだのちに，れる体系の基礎となる証明手法と，本質的に一致す

1. 制約式 ϕ を現在の計算状況が満たしているかどることにも触れる．特に WSTS の代表的な例である

Lossy Counter Machine からの還元を用いることで，我々の到達可能性問題が Non Primitive Recursive とうか，を検査し；

2. 満たしている場合には，更新式（の集合）up に基づき計算状況を更新する呼ばれる，計算に莫大な時間を要するクラスに属することで遷移を行う．遷移の正確な定義のために，まずことを述べる．

は制約式と更新式を定義する．

1. 1 記法

2. 1 制約式

非負有理数全体を Q≥0 ≜ {r ∈ Q : r ≥ 0} で書くこ

クロックの集合 X 上の制約式全体 C(X ) を，以下とにする．非負有理数 r ∈ Q≥0 について，fr (r) を，rの小数部を表すために用いる．例えば，fr (1.5) = 0.5である．
また，文字 ν を非負有理数上の割当（クロックの持つ値の表現）ν : X → Q≥0 のために用いる．割当を記述するために，記法 ν = {x 7→ 0.5, y 7→ 1.3} を用いる．割当 ν 上のクロック x の値を，非負有理数

r で上書きして，新しい割当を作ることを ν[x := r]で書く．非負有理数 δ と割当 ν について，全てのクロック値を δ だけ増やして得られる割当を ν + δ で書く．正確には (ν + δ)(x) ≜ ν(x) + δ で定義される．
クロックの集合 X について全てに 0 を割り当てた特
殊な割当を 0X で書く：∀x ∈ X . 0X (x) = 0.0．

の文法で与える：
ϕ ::= x ▷◁ k | x ▷◁ y | fr (x) = 0 | fr (x) ▷◁ fr (y)| ¬ϕ | ϕ ∧ ϕ.
ただし，▷◁ ∈ {<, =, >} は二項関係を表す記号で，k ∈ N と x, y ∈ X を満たすことにする．
x ▷◁ y は，時間オートマトンで対角線制約（diagonal constraints）と呼ばれるものの特殊な形で，２つのクロックの値を比較するために用いる．一方でfr (x) = 0 や fr (x) = fr (y) は，クロックの小数部を調べるために用いる．具体的な定義は以下で与え，これらの制約式と既存の体系の比較は，この後に 2.5 節で与える．
割当 ν と制約式 ϕ について，以下の場合分けのもと，ν が ϕ を成立させることを意味して ν |= ϕ と書く：

• ν(x) ▷◁ k のとき，ν |= x ▷◁ k と書く．

制約であり；• ν(x) ▷◁ ν(y) のとき，ν |= x ▷◁ y と書く．

• up は更新式の集合で，各クロック x ∈ X につい• fr (ν(x)) = 0 のとき，ν |= fr (x) = 0 と書く．同様に，fr (ν(x)) ▷◁ fr (ν(y)) のとき，ν |= fr (x) ▷◁ fr (y)て，丁度一つの制約式 up(x) を持つ．

UTA における遷移は，以下の形式で表される：(δ,a)⟨p, ν⟩ −−−→ ⟨q, ν ′ ⟩.

と書く．

• ν |= ϕ で「ない」とき，ν |= ¬ϕ と書く．

これは，現時刻から δ ∈ Q≥0 時間経過した後に，入• ν |= ϕ1 かつ ν |= ϕ2 のとき，ν |= ϕ1 ∧ ϕ2 と書く．

力記号 a を読んだ結果として，⟨q, ν ′ ⟩ が得られるこ(δ,a)とを意味する．従って，遷移 ⟨p, ν⟩ −−−→ ⟨q, ν ′ ⟩ は，

2. 2 更新式と割当の更新

以下が満たされる時に成立する：

クロック x ∈ X に対する更新式 θ は，新しいクロッ
ク x を含む制約式 θ ∈ C(X ∪ {x}) である．クロックx の更新式 θ は，更新に際してクロック x の値をどの

a,ϕ,up• 遷移規則 p −−−−→ q ∈ ∆ が存在し，• 時 間 δ ∈ Q≥0 が 経 過 後 に ，制 約 が 満 た さ れ(ν + δ) |= ϕ，ように変更するかを定めている．形式的には，X 上• ν ′ が更新によって得られる ν ′ ∈ up(ν + δ)．

の割当 ν について，新しい値の候補を以下で定める：

制約が満たされない場合だけでなく，更新が可能でな

θ(ν) ≜ {r ∈ Q≥0 : ν ∪ {x 7→ r} |= θ}.

い場合 up(ν + δ) = ∅ にも，遷移が生じないことに

X 上の割当 ν について，各クロック xi ∈ X についての更新式 θi ∈ C(X ∪ {xi }) からなる集合

注意されたい．
計算列 π は 1 つ以上の遷移の合成からなる：(δ0 ,a0 )(δ1 ,a1 )(δn ,an )up = {x1 7→ θ1 , x2 7→ θ2 , . . . , xn 7→ θn }⟨q0 , ν0 ⟩ −−−−→ ⟨q1 , ν1 ⟩ −−−−→ · · · −−−−−→ ⟨qn , νn ⟩.

を考える．このとき，更新式の集合 up を用いた割当

計算列 π から，時間付き語 tw(π) ∈ (Σ × Q≥0 )∗ が定

ν の更新を以下で定める：

義される：

′

′

up(ν) ≜ {ν : ∀i ∈ [1..n]. ν (xi ) ∈ θi (ν)}.

tw(π) ≜ (δ0 , a0 )(δ1 , a1 ) · · · (δn , an ).
特に，初期計算状況 ⟨qinit , 0X ⟩ から始まり，何らか

この定義は以下のように読むことができる：• クロック xi 上の更新式 θi は，現在の割当に基づく，の終了状態 qfinal ∈ F で終わる計算列(δ0 ,a0 )(δn ,an )新しい xi の値の定め方を与える：ν ′ (xi ) ∈ θi (ν).

⟨qinit , 0X ⟩ −−−−→ · · · −−−−−→ (qfinal , ν)

• 従って，新たな割当 ν ′ は，同時に全ての更新式

を受理計算列と呼ぶ（終端点での割当 ν は何でも良い）．UTA A の言語を，受理計算列の定める時間付を満たす必要がある．
例えば，次の更新式集合()

up = { x < x ∧ fr (x) = fr (x) ,(き語の全体からなる集合として定義する：

)

y=y }

L(A) ≜ {tw(π) : π は A の受理計算列 }.

は，（注意．一般的な時間オートマトンの定義では，時間• クロック x について整数部分を 1 以上減らし，• クロック y は変更しない付き語を，イベントの発生時刻とのペアで定義する：

tw(π) = (a0 , δ0 )(a1 , δ0 + δ1 ) · · · (an , Σni=0 δi ).

ということを意味する．従って，以下のような更新が

ただし，これと本論文の定義では，本質的な差はな可能である：
up({x 7→ 2.4, y 7→ 1.0}) =い．本論文では，この後で言語例を考える時に，その{}{x 7→ 1.4, y 7→ 1.0}, {x 7→ 0.4, y 7→ 1.0} .

説明を簡単にしたかったために上の定義を採用した．
）
到達可能性問題. 時間オートマトンでの到達可能性問
題の定義にならって，本論文での UTA A での到達可

2. 3 遷移規則と計算列
a,ϕ,upUTA A の遷移規則は p −−−−→ q の形をとり，特に• p, q ∈ Q は状態で，a ∈ Σ は入力文字を表し；• ϕ ∈ C(X ) は遷移を許すかどうかを調べるための能性問題を定める．

A の 2 つの状態 qstart と qgoal について，qstart から qgoal への到達可能性問題とは，(δ0 ,a0 )(δn ,an )∃ν. ⟨qstart , 0X ⟩ −−−−→ · · · −−−−−→ ⟨qgoal , ν⟩

が成立するかどうかを判定する問題である．3 章以降
で，到達可能性問題の決定可能性を示す．

れる．
一方で，入力 (1, a)(1, a)(0, b)(0, b)(0, b) を考える．

(1, a)(1, a)(0, b)(0, b) までを読んだとすると，計算状
況は必ず ⟨q2 , {x 7→ 0, y 7→ 0}⟩ となる：

2. 4 UTA の言語の例(1,a)(1,a)(0,b)(0,b)⟨q0 , 0{x,y} ⟩ −−−−−−−−−−−−→ ⟨q1 , {x 7→ 0, y 7→ 0}⟩.

次の言語 Lab を受理する UTA を考える：
mnLab ≜ {(1, a)(1, a) . . . (1, a) (0, b) . . . (0, b) :この時，例えば(0,b)⟨q1 , {x 7→ 0, y 7→ 0}⟩ −−−→ ⟨q1 , {x 7→ 0, y 7→ −1}⟩

0 < m ≤ n}.
この言語は丁度 1 秒毎に a が現れ，一方で b は時間とできると良いが，クロック値の領域は「非負有理経過なしに a の個数以下現れるような，時間付き語

数」に限られているため，更新に失敗する：

全体からなるものである．Lab は 2 つのクロック x, yを持つ UTA で受理される：b, ϕb , upya, ϕa , upx

q0b, ϕb , upy

よって (1, a)(1, a)(0, b)(0, b)(0, b) は受理されない．
上の言語 Lab は，時間経過をせずに複数の b を処理するという意味で，実時間システムのモデル化といq1う観点からは，少し不自然な例である．ここで，もう

ただし，遷移規則中の制約式や更新式は以下で定義さ

) (

(

) (

少し現実的な次の言語 L′ab についても言及しておく：
mnL′ab ≜ {(1, a) . . . (1, a) (r1 , b)(r2 , b) . . . (rm , b) :れているとする：
ϕa ≡ x = 1, ϕb ≡ x = 0,(

upy ({x 7→ 0, y 7→ 0}) = ∅.

)upx ≡ { x = 0 ,y = y },

upy ≡ { x = x ,y < y ∧ fr (y) = fr (y) }.

)0 < m ≤ n, (Σmi=1 ri ) = 1}.
この言語は，1 秒毎に文字 a が現れ（その個数を n とする），続く「1 秒間」に b が n 個以下連続する文字例として，2 つの時間付き語 (1, a)(1, a)(0, b) と列全体を表している．先と同様に，時間経過の計測の(1, a)(1, a)(0, b)(0, b) についての計算を考える．初期

ためのクロック x と，a の個数を記録するためのク

計算状況 ⟨q0 , 0{x,y} ⟩ で考えるべき遷移規則は，

ロック y を用いて，同じアイディアによって UTA でa,ϕa ,upx

受理することができる．

q0 −−−−−−→ q0
であり，この遷移規則は，丁度 1 秒経過した時に限りまた，Lab の別の方向の拡張として，使用するク

遷移を許し，その際に経過時間の計測を行うためのク

ロックの個数を増やすことで，次の言語も受理できる：

ロック x を 0 にリセットする．従って，Labc ≜ {(1, a) . . . (1, a) (0, b) . . . (0, b) (0, c) . . . (0, c) :(1,a)

0 < m ≤ n, 0 < l ≤ n}.
Lab は，a の個数 n について，これよりも少ない b の(1,a) (1,a)

連続からなる時間付き語全体であった．Labc は，更⟨q0 , 0{x,y} ⟩ −−−→ ⟨q0 , {x 7→ 0, y 7→ 1}⟩が成立し，⟨q0 , 0{x,y} ⟩ −−−−−−→ ⟨q0 , {x 7→ 0, y 7→ 2}⟩

n

m

l

に別の文字 c について，これを拡張したものであり，までが成立する．
b,ϕb ,upy−−−−−→ q1
次の入力 (0, b) で使用する遷移規則 q0 −3 つのクロックを持つ UTA で受理できる．

は，時間が一切経過していない場合に限り遷移を許し，その際に個数を記憶しているクロック y を「1 以上の整数値分」減らす操作を行う．よって(0,b)⟨q1 , {x 7→ 0, y 7→ 2}⟩ −−−→ ⟨q1 , {x 7→ 0, y 7→ 0}⟩が成立し，この時，結果として (1, a)(1, a)(0, b) が受理される．また，(0,b)⟨q1 , {x 7→ 0, y 7→ 2}⟩ −−−→ ⟨q1 , {x 7→ 0, y 7→ 1}⟩(0,b)−−−→ ⟨q1 , {x 7→ 0, y 7→ 0}⟩も成立し，この時は (1, a)(1, a)(0, b)(0, b) が受理さ

2. 5 従来の体系との比較
我々の更新可能時間オートマトンの位置づけを示す
ために，Alur と Dill による時間オートマトン [4] と，Bouyer らによる更新可能時間オートマトン [7] との比較を行う．以下の表 1 が，簡単な要約である．

Alur と Dill によって [4] で導入された時間オートマトン（Timed automata）は, 更新可能時間オート
マトンの制限として説明できる．正確には，更新式表1
体系

時間オートマトンの比較

制約式

x ▷◁ kTA [4]

更新式

x = x,

受理できないことが示される．ところが，この 2 つ
到達可能性

PSPACE 完全

x=0
Diag. [5] [4]Bouyer [7]x ▷◁ k,x − y ▷◁ k=TAx ▷◁ k,TA +x − y ▷◁ kx≤kx ▷◁ k,TA +x − y ▷◁ kx>kx ▷◁ kfr (x) = 0,

復補題から直ちに得られる．
次に，時間オートマトンに対角線制約（Diagonal

PSPACE 完全

constraints）と呼ばれる制約式を許した拡張を考える．Diagonal constraints とは x − y ▷◁ k （ここでPSPACE 完全

k ∈ N）という形をした式であり，これを用いることで，2 つのクロックの値の差について調べることがで

決定不能

TA +

決定不能

x − y ▷◁ k

きる．通常の時間オートマトンについては，diagonal

constraints を許す拡張でも，その表現力に変化がな
いことが良く知られている [5] [4]．
最後に，Bouyer らの更新可能時間オートマトン

x ▷◁ k, x ▷◁ y,
本論文の言語が正規言語でないことは，正規言語に関する反同左

Non.Prim.Rec

fr (x) ▷◁ fr (y)をみる．Bouyer らは，更新可能時間オートマトンの「制約に使用可能な式」と「更新に使用可能な式」の2 つをパラメータとし，（上の表のように）様々な組合を，値を変更しない (x = x) か，値 0 へのリセット(x = 0) のみに制限し，制約式は，即値との比較（例えば 1 < x や 2 = y ）に制限することで得られる体系である．この体系では，到達可能性問題が，時間オー
トマトンの大きさに関して PSPACE 完全であることが証明されている [4]．
先の言語 Lab を受理する UTA の構成においては，更新操作が要となっていたため，従来の時間オートマ
トンで受理することは困難に思える．実際に，Lab は
従来の時間オートマトンでは受理できない．
補題 1. Lab , L′ab , 及び Labc は時間オートマトンでは受理できない．

せによって得られる体系の到達可能性問題の決定可能性及び，表現力を調べた [7]．更新可能時間オート
マトンにおいては，一般の diagonal constraints（例えば x − y = 1）と，ある定数より大きな値への更新

x > k の組合せで，2 計数機械を十分に模倣できることを示した．そのようなチューリング完全な拡張を与える一方で，Bouyer らは制約式と更新式の組合せを強く制限することで，到達可能性問題が決定可能なクラスも与えている．しかし，そのようなクラスの表現力は，それ以前に知られていた「ϵ 遷移を許す」時間
オートマトン [5] に含まれることも同時に示された．
実は上でみた言語 Lab などは，補題 1 の証明と同Proof. Alur と Dill による次の結果 [4] を用いる：

様にして，ϵ 遷移を許す時間オートマトンでも受理で時間オートマトン A の言語 L(A) に関して，

きないことが示される．

Untime(L(A)) は正規言語である．

補題 2. Lab , L′ab , 及び Labc は ϵ 遷移を許した時間

Untime は，時間付き語から，タイムスタンプを忘却するような関数であり，例えば，上の 3 つの言語について以下が成立する：
Untime(Lab ) = Untime(L′ab ) =mn{aa . . . a bb . . . b : 0 < m ≤ n},mの決定可能な部分体系でも受理されない．
加えて，我々の更新可能時間オートマトンで ϵ 遷移を許したとしても，本論で与える到達可能性解析アルゴリズムを適用できる．すなわち，我々の更新可能時
間オートマトンは，その到達可能性問題が決定可能で

Untime(Labc ) =n

オートマトンでは受理できない．従って，Bouyer ら

l{a . . . a b . . . b c . . . c : 0 < m ≤ n, 0 < l ≤ n}.
従って，これら 2 つの言語が正規言語でないことを示せば，上の結果の対偶から，時間オートマトンではありながら，表現力について Bouyer らの時間オート
マトンの体系を超えたものであることが分かる．
我々の体系で Lab といった言語を受理できる最大の要因，もしくは Bouyer らの体系との決定的な違い
は，Bouyer らの研究では扱われなかった，以下の 2
つの式に注目したことである：• δ = (p, q, Upd(x)) の場合：
δ(C) ≜ {⟨q, ν[x := r]⟩ : ⟨p, ν⟩ ∈ C, r ∈ Q≥0 }.
• δ = (p, q, Time) の場合：
δ(C) ≜ {⟨q, ν + δ⟩ : ⟨p, ν⟩ ∈ C, δ ∈ Q≥0 }.

• k = 0 の場合の x − y ▷◁ k の式，すなわち x ▷◁ yのみを許す．

• δ = (p, q, Test(φ)) の場合：

• ク ロック 値 の 小 数 部 分 を 検 査 す る た め の 式
fr (x) = 0 や fr (x) ▷◁ fr (y) を許す．

δ(C) ≜ {⟨q, ν⟩ : ⟨p, ν⟩ ∈ C, ν |= φ}.
何らかの遷移規則 δ ∈ ∆ のもとで ⟨q, ν ′ ⟩ ∈ δ({⟨p, ν⟩})実は，上の表で決定不能と書かれた部分では，本質的が成立するときに ⟨p, ν⟩ ⇒ ⟨q, ν ′ ⟩ と書く．複数のスに k > 0 の場合の対角線式を用いて，2 計数機械の模テップで遷移可能な場合を ⟨p, ν⟩ ⇒∗ ⟨q, ν ′ ⟩ と書く．

倣を行っている．Bouyer らの論文では，k = 0 の場

UTA の到達可能性問題を解くためには，UTS を考合に限った時についてどうなるかは，言及されていな

えれば十分であることが，次の補題から保証される．

かった．

補題 3. 与えられた UTA A = (Q, qinit , F, X , Σ, ∆)また，x ▷◁ y の形式と，小数部分の検査のための式と 2 状態 qstart と qgoal について，以下を等価にする，の，2 つを同時に採用することが重要である．本論で′′UTS S = (Q′ , X , ∆′ )（と 2 状態 qstart, qgoal）を構成

はその証明を与えることはしないが，どちらか 1 つすることができる：

だけの採用では，従来の時間オートマトンと表現力が• A で，⟨qstart , 0X ⟩ から状態 qgoal へ到達できる．

変わらないことが示される．

′′• S で，⟨qstart, 0X ⟩ から状態 qgoal
へ到達できる．

表には現れていないが，additive constraints と呼従って，UTS S の到達可能性問題が決定可能とな

ばれる，対角線制約とは異なる形式の制約と，更新ることを示せば良いことが分かる．しかし，この証明の組合せについて論じた研究もある [13]．この研究では本質的でないところで複雑となってしまうので，証は言語のクラスについての議論を行ってはいないが，明のアイディアを述べるためにも，UTS を一層単純化

Alur と Dill が示したものと同様に，Untime 関数のした，更新可能離散時間遷移系（Updatable Discrete

像が正規言語となるため，Lab などを受理することはTimed Transition System，UDTS）を考え，この到できない．

達可能性判定アルゴリズムを先に与える．UDTS は，lossy counter machine と呼ばれる計算モデルを模倣
2. 6 更新可能時間遷移系

することができ，それ自身で興味深い体系となって本節では，UTA の到達可能性問題を解くために，いる．

より単純な計算モデルを考える．
更新可能時間遷移系（Updatable Timed Transi-

3 更新可能離散時間遷移系

tion System，UTS）S は 3 つ組 (Q, X , ∆) である．

更 新 可 能 離 散 時 間 遷 移 系（Updatable Discrete

ここで Q と X は，それぞれ UTA と同じように，状Timed Transition System，UDTS）D は，UTS と態の有限集合とクロックの有限集合である．到達可能

同じく 3 つ組 (Q, X , ∆) で，Q は有限の状態集合，X性問題を解くにあたり，入力アルファベットは必要ではクロックの有限集合，∆ は遷移規則の有限集合でないため，UTS にはアルファベットはない．

ある．

UTS の 計 算 状 況 ⟨q, ν⟩ は ，状 態 q ∈ Q と 割UDTS の計算状況 ⟨q, µ⟩ は，状態 q ∈ Q と，自然

当 ν : X → Q≥0 の 組 で あ る ．遷 移 規 則 δ は ，

数上の割当 µ : X → N である．自然数上の割当に限(p, q, Upd(x)), (p, q, Time), (p, q, Test(φ)) ∈ ∆ の 3

定するところが，UTS とは異なる．遷移規則 δ は，種類がある．計算状況の集合 C について，記法 δ(C)(p, q, Upd(x)), (p, q, Time), (p, q, Test(φ)) ∈ ∆ の 3

により遷移を定義する：

種類がある．計算状況の集合 C について，記法 δ(C)により遷移を定義する：

• δ = (p, q, Upd(x)) の場合：
δ(C) ≜ {⟨q, µ[x := n]⟩ : ⟨p, µ⟩ ∈ C, n ∈ N}.

について，停止性を保証する良い性質が現れる．次節以降でこのことをみていく．

• δ = (p, q, Time) の場合：
δ(C) ≜ {⟨q, µ + 1⟩ : ⟨p, µ⟩ ∈ C}.
• δ = (p, q, Test(φ)) の場合：

3. 1 計算状況集合の記号表現
後ろ向き到達可能性解析では，各 step において，

δ(C) ≜ {⟨q, µ⟩ : ⟨p, µ⟩ ∈ C, µ |= φ}.

計算状況集合 R0 へ到達しうる計算状況の集合を拡大

Test(φ) では，その時点での割当を検査するが，する操作を行っている．そのため，計算状況の「集UDTS では自然数上の割当のみを考えているので，φ合」を記号的に表現し，個々の要素ではなく記号表現

は以下の文法で与えられると考えても良い：

を操作したい．そこで，本節では，以下の性質を満た

φ ::= x ▷◁ k | x ▷◁ y | ¬ϕ | ϕ ∧ ϕ.
D は構成要素が有限の計算モデルであるから，制約式に現れる最大の自然数 M が定まる：

す表現形式を探す．
望まれる性質. E を計算状況の表現，JEK を E の表す計算状況全体の集合，pre(JEK) を 1-step の遷移M ≜ max{k : “x ▷◁ k” が ∆ 中に現れる }.

で JEK に入る計算状況全体とする．この時，E から

この M は次節以降で用いられるが，直感的に言えば，次を満たす有限個の（空かもしれない）表現の集合∆ 中の制約式では，クロック値が M を超えた場合に{E1 , E2 , . . . , En } が計算可能である：

具体的な値を調べられないことを意味する．
本章では，次の定理を示す．

pre(JEK) =∪i

JEi K.

まず，制約式で区別不能な計算状況をひとまとめに定理. UDTS D と 2 つの位置 qinit , qfinal について，

する，ということが考えられる．すなわち，ある表現

到達可能性問題 ⟨qinit , 0X ⟩ ⇒∗ ⟨qfinal , µ⟩ は決定可能

E の要素 ⟨q, µ1 ⟩, ⟨q, µ2 ⟩ ∈ JEK について，UDTS Dである（終端点の µ は何でも良いとする）．

の全ての制約式 φ に関して

我々の到達可能性判定アルゴリズムは，状態 qfinal
からの後ろ向き到達可能性解析を行うもので，概略的には次のようにまとめられる：• 状態 qfinal にさえ到達することができれば良いµ1 |= φ ⇐⇒ µ2 |= φが成立するべきである．D において，既に制約式中の最大の定数 M を定義した．その際にも述べたが，D では M を超えた値を x ▷◁ k の形の式で調べること

ので，集合 R0 = {⟨qfinal , µ⟩ : µ ∈ X → N} にはできない．従って，M を超えたクロック値につい⟨qinit , 0X ⟩ が入っているかどうかを調べる．

ては，正確な値を保持しておく必要はない．その一方• もし入っていないのであれば，1-step の計算で集で，式 x ▷◁ y によって，2 つのクロックが等しいか，

合 R0 に入る計算状況全体の集合 R1 = pre(R0 ) ={c : c ⇒ c′ , c′ ∈ R0 } を計算し，⟨qinit , 0X ⟩ ∈ R1
かどうかを調べる．

• ま た し て も 入って い な い の で あ れ ば ，2-stepの計算で集合 R0 に入る計算状況全体の集合

R2 = pre(R1 ) を計算し，⟨qinit , 0X ⟩ ∈ R2 かど
うかを調べる．
以上の操作の繰り返しが判定アルゴリズムの骨子である．このアルゴリズムには，⟨qinit , 0X ⟩ から qfinalへ到達できない場合に，手続きが停止しないという問題点がある．しかし，更新可能離散時間遷移系（及び更新可能時間遷移系）では，後ろ向き到達可能性解析

もしくは大小の関係などは調べることはできる．そこで，M を超えた部分では順序関係だけを覚える，ということを念頭に次の preshape と呼ぶ表現を考える：

P : H0, x1 , x2 IH1IHx3 , x4 IHx5 I.
以降では（D から計算した）M が 1 であるとし，2 以上の自然数値を含まない preshape だけを考える．

Preshape では，あるバッグ H· · ·I で，ひとまとめにされるクロック（と M 以下の定数）が全て等しいとし，同時にバッグのならびが，クロックの大小関係を表すものとする．したがって，この preshape P

は，以下の割当の集合を表す：
JP K = {µ : {x1 , . . . x5 } → N :µ |= 0 = x1 = x2 , µ |= x3 = x4
µ |= 1 < x3 , µ |= x3 < x5 }.
Preshape は割当集合のための記号表現だが，状態 qと組合せて，J⟨q, P ⟩K で「計算状況」の集合を与える：

J⟨q, P ⟩K ≜ {⟨q, µ⟩ : µ ∈ JP K}.
Preshape の利点は，次の命題にある．
命題 1. P を preshape とする．このとき，∆ に出現する任意の制約式 φ について，以下が成立する：∀µ1 , µ2 ∈ JP K. µ1 |= φ ⇐⇒ µ2 |= φ.
同時に，規則 δ = (p, q, Test(φ)) ∈ ∆ について，以下を満たす（空かもしれない）有限集合 {P1 , . . . , Pn }が計算可能：

δ −1 (J⟨q, P ⟩K) =この考察に基づき，preshape を，M を超えた部分についてバッグ間の距離情報を持つように細分化した，shape と呼ぶものを考える．各 shape S は，以下の形式で書かれる：

S : H0, x0 IH1, x1 I <a Hx2 , x3 I <b Hx4 I.
M を超えた部分について，直前のバッグとどれだけ離れているかを，index a, b ∈ N によって表現する．
この時 S は，以下の割当の集合を表現する：
JSK = {µ : µ |= 0 = x0 ∧ 1 = x1 ∧ x2 = x3 ,µ |= 1 + a < x2 , µ |= x2 + b < x4 }.
任意の preshape は，全ての index を 0 とする shapeで表すことができる．

Preshape の代わりに shape を用いると，先の状況を回避できることを確認する：∪

J⟨p, Pi ⟩K.
i

1. 再び Upd(x) によって H0IH1I <0 HxI <0 HyI と命題 2. Preshape P と，規則 δ = (p, q, Time) ∈ ∆なる計算状況全体を考える．

について，以下を満たす（空かもしれない）有限集合

JH0IH1I <0 HxI <0 HyIK = {µ : µ |= 1 < x < y}{P1 , . . . , Pn } が計算可能：であるから，以下の計算状況の集合

δ−1(J⟨q, P ⟩K) =∪i

J⟨p, Pi ⟩K.

すなわち，preshape は Test(φ) や Time 遷移規則
についての pre の計算を正確に表現できることを意{µ ∈ {x, y} → N : µ |= 2 < y}を，複数の shape で表現できればよい．

2. shape を用いると，味する．一方で，preshape では，M を超えた部分の{µ : µ |= 2 < y} = JS1 K ∪ JS2 K ∪ · · · ∪ JS5 K

クロック間の「距離」に相当する情報を失っているたで表現できる．ただし，S1 から S5 は以下で定め，Upd(x) についての pre に相当する計算が正確に義する：
S1 = H0, xIH1I <1 HyI,

表現できない．これは以下で確かめられる．

1. 規則 (p, q, Upd(x)) によって J⟨q, H0IH1IHxIHyI⟩Kとなる計算状況全体を考える．

JH0IH1IHxIHyIK = {µ : µ |= 1 < x < y}であるから，そのような計算状況全体は{⟨p, µ⟩ : µ |= 2 < y}であることが分かる．

2. すなわち，y が「3 以上」の値を取る全てを表現する必要がある．しかし，preshape ではバッグ間の距離を表現することができないため，これを正確に表現することができない．

3. 例えば，x と y が同じ値を持つ計算状況の集合
は，H0IH1IHx, yI でしか表現できないが，

JH0IH1IHx, yIK = {µ : µ |= x = y ∧ 1 < x}となってしまい，{x 7→ 2, y 7→ 2} などの，望まない割当が紛れる．

S2 = H0IH1, xI <1 HyI,

S3 = H0IH1I <0 HxI <0 HyI,
S4 = H0IH1I <1 Hx, yI,
S5 = H0IH1I <1 HyI <0 HxI.

Shape は preshape を細分化したものであるため，
既に preshape で成立していた Test(φ) や Time に関する性質は保存され，加えて細分化によって，Upd(x)についての一歩前の計算状況全体も正確に表現できるようになる．その結果として，我々の望む性質が次の補題で実現される．
補題 4. 状態と shape の任意の組 ⟨q, S⟩ について，以下を満たす（空かもしれない）有限の shape の集合{⟨p1 , S1 ⟩, . . . , ⟨pn , Sn ⟩} を計算できる：
pre(J⟨q, S⟩K) =∪i

J⟨pi , Si ⟩K.

特に Pre(⟨q, S⟩) = {⟨p1 , S1 ⟩, . . . , ⟨pn , Sn ⟩} と書くことにする．

Preshape に代わって shape を採用することで上の準的な順序 (N, ≤) と，次元 d の自然数ベクトル上の補題を得るが，その一方で別の問題として，shape

直積順序 (Nd , ≤) がある．我々の shape 上の順序 ≼全体の集合が，index のために加算無限程度のサイ

は，自然数ベクトル上の直積順序を元にして導入した

ズとなってしまう．しかし，shape 上に well-quasi-

ものであり，これから次の補題が示される．

ordering を定めることができ，これによって後ろ向

補題 5. Shape 上の ≼ は well-quasi-ordering である．

き到達可能性解析アルゴリズムが得られることを次

また，2 つの w.q.o. から作った直積順序が w.q.o.

節でみる．

を満たすという Dickson の補題 [12] により，状態と

shape 上の次の直積順序が w.q.o になることも分かる．
3. 2 Shape 上の Well-quasi-ordering

補題 6. 状態と shape の組 ⟨q, S⟩ と ⟨q ′ , S ′ ⟩ につい2 つの shape S1 と S2 について，index を忘れるとて，以下の順序 ≼ は w.q.o. になる：

同じ preshape になる場合に，S1 ∼ S2 と書く．すな⟨q, S⟩ ≼ ⟨q ′ , S ′ ⟩ ⇐⇒ q = q ′ かつ S ≼ S ′ .

わち以下のような S1 と S2 については，S1 ∼ S2 がこの w.q.o を用いて，後ろ向き到達可能性解析アル

成立する：
S1 = H0, · · ·IH1, · · ·I <a1 H· · ·I <a2 H· · ·I,

S2 = H0, · · ·IH1, · · ·I <b1 H· · ·I <b2 H· · ·I.
S1 ∼ S2 について ⟨a1 , a2 , . . . , an ⟩ と ⟨b1 , b2 , . . . , bn ⟩をそれぞれ S1 と S2 の index とする．このとき，すべての i ∈ [1..n] について ai ≤ bi が成立しているな
らば，もしくは同じことであるが Nn 上の直積順序で⟨a1 , a2 , . . . , an ⟩ ≤ ⟨b1 , b2 , . . . , bn ⟩ ならば，S1 ≼ S2と書く．
このとき，≼ が shape 上の半順序（partial order）
であることは明らかである．また，バッグ間の距離

Hx, · · ·I <d Hy, · · ·I は，x + d < y を要求することを思い出すと，shape 上の順序 S1 ≼ S2 では，S1 でのバッグ間の距離 ai が，S2 での距離 bi 以下 ai ≤ bi であるから，割当の集合としては S1 の方が大きいこと

ゴリズムを与えた上で，その停止性を証明する．

3. 3 後ろ向き到達可能性アルゴリズム
3 章の冒頭で述べた，後ろ向き到達可能性解析アルゴリズムを，補題 4 を用いて shape 上で形式化していく．
まず，R0 = {⟨qfinal , µ⟩ : µ ∈ X → N} について

R0 = J⟨qfinal , I1 ⟩K ∪ · · · ∪ J⟨qfinal , In ⟩Kを特徴付ける有限個の shape {I1 , . . . , In } を計算しておく．
次に，現時点で到達すると分かっている計算状況の集合 X から，X ∪ pre(X) を求める計算に相当する
関数 Expand を定義する．
1: function Expand({C1 , C2 , . . . , Cn })2:

R := {C1 , C2 , . . . , Cn }命題 3. 2 つの shape S1 と S2 について，S1 ≼ S2 な

3:for i = 1 to n do

らば，JS2 K ⊆ JS1 K が成立する．

4:を意味する．

特に，shape 上の半順序 ≼ は，well-quasi-ordering[12] [2] [10] と呼ばれるものになっている．これは，次5:6:for each D ∈ Pre(Ci ) do
if R は C ≼ D とする C を持たない thenR := R ∪ {D}return R

節で与える，後ろ向き解析アルゴリズムの停止性を7:

示す上で鍵となる性質であり，正確には次で定義さこの関数は，既に qfinal に到達することが分かっていれる．半順序集合 (X, ⪯) で ⪯ が well-quasi-ordering

る計算状況の集合 {C1 , C2 , . . . , Cn } を，補題 4 を用

（w.q.o.）になるのは，次を満たすとき：

いて，1 ステップ分拡大する．2 つの shape S1 , S2 が

• X 上の任意の無限列 (xi )i = x1 , x2 , x3 , . . . につS1 ≼ S2 であるときに，JS2 K ⊆ JS1 K が成立すること

いて，index の組 (m, n) で m < n かつ xm ⪯ xn

は既にみた通りであるから，既に到達すると分かってを満たすものが存在する．

いる C ∈ R よりも，≼ として大きな D を新たに含

Well-quasi-ordering の代表的な例は，自然数上の標めることは「無駄」であるために，これを省いている3. 4 Well Structured Transition System とことに注意されたい．
このとき，Expand は明らかに単調増加関数であるから，
Expand({⟨qfinal , I1 ⟩, . . . , ⟨qfinal , In ⟩})の関連

Well-quasi-ordering の導入から補題 8 が得られ，⊊到達可能性解析アルゴリズムの停止性が保証された．

Expand ({⟨qfinal , I1 ⟩, . . . , ⟨qfinal , In ⟩})..
.

⊊この形での停止性保証を行う議論の流れそのもの

Expand ({⟨qfinal , I1 ⟩, . . . , ⟨qfinal , In ⟩})

=

2

k

は，既に存在しており，本論で新たに与えたものではExpand({⟨qfinal , I1 ⟩, . . . , ⟨qfinal , In ⟩})のような不動点の存在を保証することができれば，次k+1ない．具体的には，近年精力的に研究が行われている Well structured transition system (WSTS) [2] [10]と呼ばれる体系で現れている．詳細については引用しの補題により，⟨qinit , 0X ⟩ を含む記号表現が含まれてた文献を参考にしてもらうことにして，WSTS でも，いるかどうかを調べることで，到達可能性が解ける．

本論で考えるような初期計算状況から状態への到達可

補題 7. 次の 2 つは同値である：

能性問題（これは [2] [10] では coverability problem• ある µ で ⟨qinit , 0X ⟩ ⇒∗ ⟨qfinal , µ⟩ が成立する．

とも呼ばれている）のための，後ろ向き到達可能性解• 不動点 Expandk ({⟨qfinal , I1 ⟩, . . . , ⟨qfinal , In ⟩}) =析アルゴリズムの停止性が，w.q.o によって保証され{C1 , . . . , Cm } について，⟨qinit , 0X ⟩ ∈ JCi K とする．そこで考える後ろ向き到達可能性解析アルゴリズ

る Ci が存在する．

ムは，本論で与えた，既知の集合に対する無駄のない

実は，Expand のような「無駄のない」拡大につ

拡大と本質的に同じことを行う．ただし，我々の更新

いて，かならず不動点が存在することが，well-quasi-

可能離散時間遷移系そのものは，直接 WSTS になる

ordering の定義から示される．

わけではないことも述べておく．5 章では，より具体

補題 8. (X, ⪯) を well-quasi-ordering 付きの集合と的に，WSTS の一例である Lossy counter machine

する．X の部分集合 Y について，無駄のない拡大をを用いることで，更新可能離散時間遷移系の到達可能

次で定義する：性問題の計算量について言及する．

Y ⋐ Y ∪ {x} ⇐⇒ ∀y ∈ Y.¬(y ⪯ x).
このとき，以下のようなY0 ⋐ Y1 ⋐ Y2 ⋐ · · ·4 更新可能時間遷移系の到達可能性解析
3 章の N を領域とする更新可能離散時間遷移系の無駄のない拡大を行う無限列は存在しない．

ための到達可能性解析アルゴリズムを踏まえ，Q≥0

Proof. 背 理 法 で 示 す．任 意 の i ≥ 0 に つ い て ，を領域とする更新可能時間遷移系のための到達可能

yi+1 ∈ Yi+1 \ Yi を選ぶことができ，これを用いて性解析アルゴリズムを与える．

無限列 y1 , y2 , . . . , ym , . . . , yn , . . . を作る．⪯ は w.q.o

前節で考えた shape は，自然数上の割当のなす集合

なので，この列の中に m < n で ym ⪯ yn とするもを記号表現したものであり，特にこの上の well-quasi-のが存在しなくてはならない．しかし，yn が追加さ

ordering が，解析アルゴリズムの停止性のために重れる理由は，y ⪯ yn となる y が存在しないことに他要であった．本節では，まず shape を，非負有理数

ならない筈なので，矛盾する．

上の割当のなす集合を表現するために設計し直す．この目的のために，時間オートマトンの理論で有用な道

逆に，無駄のない拡大での無限列が存在しなければ，(X, ⪯) が w.q.o になることも導ける．
ここまでの議論をまとめると，次の結果が得られる．
定理 1. 更新可能離散時間遷移系 D で，到達可能性
問題は決定可能である．

具である，region abstraction の手法を用いる．

4. 1 Region abstraction
抽象化手法である region abstraction は，時間オー
トマトンの到達可能性問題の決定可能性を示すために Alur と Dill によって導入された [4]．

従来の region abstraction では，与えられた割当 ν

このとき，Rshape は，後ろ向きの計算について正確について，小数部分の実際の値を捨て，代わりにクであり，補題 4 に対応する性質が成立する．

ロックの小数部分の「ならび」だけを覚える．例えば，

補題 9. 状態と Rshape の任意の組 ⟨q, R⟩ についν = {v 7→ 1.2, w 7→ 0.5, x 7→ 0.2, y 7→ 1.0, z 7→ 1.6}て，以下を満たす（空かもしれない）有限の集合という割当は，以下のように抽象化される：{⟨p1 , R1 ⟩, . . . , ⟨pn , Rn ⟩} を計算できる：

R(ν) = {(y, 2)}0 {(x, 1), (v, 2)}{(w, 1)}{(z, 2)}.

pre(J⟨q, R⟩K) =∪i

J⟨pi , Ri ⟩K.

R(ν) におけるクロックの列びは，ν の小数部分に対応し，整数部分の値だけが残されていることに注意さ

4. 2 RShape 上の Well-Quasi-Ordering

れたい．特に，一番左の集合 {. . .}0 によって，小数2 つの Rshape R1 = (S1 , F1 ) と R2 = (S2 , F2 ) に部分が丁度 0 のクロックを表すようにする．この記

ついて，以下を満たす時に，R1 ≼ R2 と書く：

法は，どちらかといえば [1] におけるものを基にして• S1 と S2 が index を忘れると一致し；いるが，Alur と Dill が考えた region abstraction と• S1 と S2 の index 列をそれぞれ ⟨a1 , a2 , . . . , an ⟩，本質的な差はない．
制約式の，特に小数部分を調べる原子式は fr (x) = 0
ないし fr (x) ▷◁ fr (y) であり，この範囲を調べるだけ⟨b1 , b2 , . . . , bn ⟩ とすると，∀i ∈ [1..n]. ai ≤ bi が成立し，

• F1 = F2 が成立する．

であれば上のような抽象化で十分であることは分か

このとき，R1 ≼ R2 ならば JR2 K ⊆ JR1 K が成立し，る．実際，次の命題が成立する．

かつ well-quasi-ordering となる．

命題 4. 2 つの割当 ν1 , ν2 が R(ν1 ) = R(ν2 ) を満た

従って，前節で考えたものと同じ到達可能性解析ア

すとき，任意の制約式 φ について以下が成立する：

ルゴリズムによって，更新可能時間遷移系の到達可能

ν1 |= φ ⇐⇒ ν2 |= φ.
我々の目的のために，R(ν) を，shape と小数部のならびの組で表現する．これを Rshape と呼ぶことにし，各 Rshape R = (S, F ) は次のような形をして性問題を解くことができる．
定理 2. 更新可能時間遷移系 S の到達可能性問題は決定可能である．
この定理と，補題 3 によって，主定理が得られる．
定理 3. 更新可能時間オートマトン A の到達可能性

いる：

S = H0IHxIHwIH1, yI <a HvI <b HzI,
F = {y}0 {x, v}{w}{z}.
（ここでは，M = 1 としていることに注意．
）
有理数上の値の抽象化を行うので，自然数上の値の抽象化とは異なり，H0IHxIHwIH1, yI といったことが起こりうることに注意されたい．

Rshape (S, F ) は，クロック値の情報を先と同じよ
うに shape S で表現し，更に小数部分を調べる制約式に対応するために，小数部分の情報を別に持っているにすぎない．従って，Rshape R = (S, F ) の表す
計算状況全体は，JRK = JSK ∩ JF K で与えられ，この例については JSK と JF K は以下で定義される：
JSK = {ν : ν |= y = 1, ν |= 0 < x < w < 1,

ν |= (1 + a) < v, ν |= (v + b) < z},
JF K = {ν : ν |= fr (y) = 0, ν |= fr (x) = fr (v),ν |= fr (y) < fr (x) < fr (w) < fr (z)}.

問題は決定可能である．

5 到達可能性問題の計算量について
更新可能時間オートマトンの到達可能性問題が決定可能であることを示したので，ここでは，その計算量についての考察を行う．
補題 3 として，更新可能時間オートマトンの到達可能性問題が，更新可能時間遷移系の対応する問題に還元されることをみた．実は，この逆も成立する．
補題 10. 与えられた UTS S = (Q, X , ∆) と 2 状
態 qstart と qgoal について，以下を等価にする，UTA

A = (Q′ , qinit , qfinal , X ′ , Σ, ∆′ ) を構成できる：• S で，⟨qstart , 0X ⟩ から状態 qgoal へ到達できる．
• A で，⟨qinit , 0X ′ ⟩ から状態 qfinal へ到達できる．
従って，ここでは，本論文で与えた 3 つの体系のうちで，最も簡単な「更新可能離散時間遷移系」における，到達可能性問題の時間計算量について考えること

PSPACE 完全 [4] であることが知られており Bouyerにする．更新可能離散時間遷移系における到達可能

らの更新可能時間オートマトンで決定可能なクラス

性解析アルゴリズムの停止性は，well-quasi-orderingについても，計算量は PSPACE 完全 [7] [8] であるこ

上での無駄のない拡大が必ず停止することを保証すとが分かっている．従って，我々の更新可能時間オーる補題 8 によるものであった．しかし，この補題はい

トマトンは，元になった体系に比べて，その到達可能

つか停止するということだけを保証し，どの程度の性問題が非常に難しくなっていることが分かる．

ステップを要するかについては保証していないため，
これを元にした計算量の解析は困難である．

6 まとめと今後の課題

そこで我々は，Lossy counter machine (LCM) と本論では，Alur と Dill による時間オートマトンに呼ばれる体系の到達可能性問題について既に知られ対して，更新の概念を導入した Bouyer らの更新可能ている，計算量の下界に関する結果を用いる．LCM

時間オートマトンという体系に関する，新たな拡張を

は，計数機械の定義をもとにして得られる計算モデ提案した．特に我々の更新可能時間オートマトンは，

ルで，一般には複数のカウンタを考える．よく知られ時間オートマトンの言語クラスを拡大するものであるているように，計数機械では 2 個以上のカウンタをことを，具体的な言語 Lab を分析して確認すること持つ場合にはチューリング完全となるが，LCM ではができた．また，そのような表現力の拡張を行うにも「値を loss する」ために，カウンタが幾つあったとし関わらず，その到達可能性問題は決定可能であるといても，到達可能性問題が決定可能になることが知られうことを，well-quasi-ordering という順序を見出すている．体系の正確な定義や到達可能性問題の定義にことによって証明した．しかしながらその計算量は，

ついては， [14] [16] などを参考にしてもらうことにしlossy counter machine の到達可能性問題からの還元て，ここでは [17] で示された次の定理を用いる．

により，全域帰納関数を用いなければならない程度に定理 (LCM の時間計算量の下界 [17]). LCM の到達巨大であることが示された．

可能性問題は，LCM のサイズを n とした時に，決定性チューリング機械で F (n) 時間必要となる．ただし，ここで F とは，「原始帰納的ではない」ような全域帰納的関数である．
また，本論では LCM の定義を与えないために正確

今後の理論的な課題として，以下のことを考えている．
一つに，更新可能離散時間遷移系の到達可能性問
題の計算量上界を調べるということがある．実は，lossy counter machine の到達可能性問題は，Classな議論を述べられないが，以下が成立する．

of Ackermannian problems Ack と呼ばれるクラス

補題 11. 任意の LCM から，そのサイズに関して線に属することが判明している [15]．そこで，これと同形時間で，これを模倣する更新可能離散時間遷移系をじ証明手法で，我々の体系も Ack に属するかどうか構成することができる．すなわち，LCM の到達可能を分析したい．

性問題は，線形時間で，更新可能離散時間遷移系の到達可能性問題に帰着可能である．
従って，これらを組み合わせると，時間計算量の下一つに，Abdulla らによって導入された Dynamic

lossy channel system (DLCS) と呼ばれる体系 [3] との比較を行うことがある．DLCS は，Timed lossy

界について，次の定理が得られる．

channel system と呼ばれる体系の到達可能性問題の定理 4. 更新可能離散時間遷移系のサイズを n とし決定可能性証明のために用いられ，DLCS 自身の到た時に，到達可能性問題を解くには，決定性チューリ

達可能性問題の決定可能性も，well-quasi-ordering をング機械で F (n) 時間必要である．上と同様に，関数用いたものとなっている [3]．この体系と我々の更新

F は，原始帰納的でない全域帰納的関数のクラスに可能時間遷移系には，類似した点が見受けられる．例

属する．

えば，DLCS には，lossy channel system（や lossy

時間オートマトンの到達可能性問題の計算量は，

counter machine）にはない，チャンネルそのものを

データとして取り扱う機能が備わっている．一方で，我々の体系でも，更新を用いることでクロックの値を失うことなくコピーすることが可能であった．そこ
で，これらの体系を分析することで，より一般的な体系を与えることに取り組みたい．
一つに，我々の更新可能時間オートマトンを，ス
タックを伴う形で拡張するということがある．最近になって，時間オートマトンとプッシュダウンオートマ
トンの考えを組み合わせたもので，その到達可能性
問題が決定可能な体系が幾つか提案されている [1] [9]．
しかしこれらの体系では，本論でみたような更新操作を考慮していない．そこで，我々の更新可能時間オー
トマトンをこの方向で拡張した時に，到達可能性問題が依然として決定可能であるかどうかを分析したい．

参 考 文 献[ 1 ] Abdulla, P., Atig, M., and Stenman, J.: DenseTimed Pushdown Automata, LICS ’12, IEEE, 2012,
pp. 35–44.
[ 2 ] Abdulla, P., Čerāns, K., Jonsson, B., and Tsay,
Y.: Algorithmic Analysis of Programs with Well
Quasi-ordered Domains, Inf. & Comp., Vol. 160,
No. 1–2(2000), pp. 109–127.
[ 3 ] Abdulla, P. A., Atig, M. F., and Cederberg,
J.: Timed Lossy Channel Systems, FSTTCS’12,
LIPIcs, 2012, pp. 374–386.
[ 4 ] Alur, R. and Dill, D.: A theory of timed automata, TCS, Vol. 126, No. 2(1994), pp. 183–235.
[ 5 ] Bérard, B., Diekert, V., Gastin, P., and Petit, A.: Characterization of the Expressive Powerof Silent Transitions in Timed Automata, Fundam.
Inf., Vol. 36, No. 2(1998), pp. 145–182.
[ 6 ] Bouyer, P., Dufourd, C., Fleury, E., and Petit, A.: Expressiveness of Updatable Timed Au-

tomata, MFCS’00, LNCS, Vol. 1893, Springer,
2000, pp. 232–242.
[ 7 ] Bouyer, P., Dufourd, C., Fleury, E., and Petit, A.: Updatable timed automata, TCS, Vol. 321,
No. 2–3(2004), pp. 291–345.
[ 8 ] Bouyer, P., Dufourd, C., Fleury, E., and Petit, A.: Are Timed Automata Updatable?, CAV’00,
LNCS, Vol. 1855, Springer, 2000, pp. 464–479.
[ 9 ] Clemente, L. and Lasota, S.: Timed pushdown
automata revisited, LICS ’15, IEEE, 2015, pp. 738–749.
[10] Finkel, A. and Schnoebelen, P.: Well-structured
transition systems everywhere!, TCS, Vol. 256,
No. 1–2(2001), pp. 63–92.
[11] Fontana, P. and Cleaveland, R.: A Menagerie
of Timed Automata, ACM Comput. Surv., Vol. 46,
No. 3(2014), pp. 40:1–40:56.
[12] Higman, G.: Ordering by divisibility in abstract
algebras, Proc. London Math. Soc., Vol. 2(1952),
pp. 326–336.
[13] Manasa, L., Krishna, S., and Nagaraj, K.: Updatable Timed Automata with Additive and Diagonal Constraints, Logic and Theory of Algorithms,
LNCS, Vol. 5028, Springer, 2008, pp. 407–416.
[14] Mayr, R.: Undecidable problems in unreliable computations, TCS, Vol. 297, No. 1—3(2003),
pp. 337–354.
[15] Schmitz, S.: Complexity Hierarchies Beyond Elementary, Manuscript arXiv:1312.5686v2 [cs.CC],
2013.
[16] Schnoebelen, P.: Lossy Counter Machines Decidability Cheat Sheet, RP’10, LNCS, Vol. 6227,
Springer, 2010, pp. 51–75.
[17] Schnoebelen, P.: Revisiting Ackermann-Hardness
for Lossy Counter Machines and Reset PetriNets, MFCS’10, LNCS, Vol. 6281, Springer, 2010,
pp. 616–628.
[18] Waez, M. T. B., Dingel, J., and Rudie, K.:
A survey of timed automata for the developmentof real-time systems, Computer Science Review,Vol. 9(2013), pp. 1–26.