| 講演抄録/キーワード |
| 講演名 |
2023-03-15 09:55
データ木書換え系の正則保存性 ~ 単項標準形に分解可能なクラス ~ ○坂尾優斗・関 浩之(名大) SS2022-62 |
| 抄録 |
(和) |
言語クラス$mathcal{L}$上の変換$T$が正則保存性を持つとは,任意の正則な言語$L in mathcal{L}$に対して$T$を任意回適用することで得られる言語$T^*(L)$も正則となることをいう.正則保存性はシステムのモデル検査に応用することができる.本稿では,記号とデータ値の対の木構造であるデータ木を変換する系であるDTRSの部分クラスとして,単項DTRSおよびその標準形を定義する.また,データ木言語が正則であるとは,それがレジスタ木オートマトンによって認識されることであると定義する.続いて,標準形DTRSの正則保存性の証明および,単項DTRSの部分クラスである強単項DTRSから標準形への等価変換法を示す. |
| (英) |
Let $T$ be a transformation over a class $mathcal{L}$ of languages. If for any regular language $L in mathcal{L}$, $T^*(L)$ obtained by applying $T$ finite times to $L$ is regular, we say that $T$ has the regularity preservation property. This property can be applied to model checking.
In this paper, we first define monadic DTRS (abbreviated as m-DTRS) and its normal form. A DTRS is a finite set of rules that rewrite data trees, which are trees where a node is labeled with a pair of a symbol and a data value. A data tree language is regular if it is recognized by a register tree automaton. Next, we prove the regularity preservation property of normal form m-DTRS and provide an equivalence translation from strong m-DTRS into normal form m-DTRS. |
| キーワード |
(和) |
正則保存性 / モデル検査 / レジスタ木オートマトン / 単項データ木書換え系 / / / / |
| (英) |
regularity preservation property / model checking / register tree automaton / monadic data tree rewrite system / / / / |
| 文献情報 |
信学技報, vol. 122, no. 432, SS2022-62, pp. 91-96, 2023年3月. |
| 資料番号 |
SS2022-62 |
| 発行日 |
2023-03-07 (SS) |
| ISSN |
Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
| PDFダウンロード |
SS2022-62 |