認識可能級数と代数的級数のための計数アルゴリズム

CHU Bao Trung; HASHIMOTO Kenji; SEKI Hiroyuki

文献

J-GLOBAL ID：201802216367167752 整理番号：18A1365212

認識可能級数と代数的級数のための計数アルゴリズム

Counting Algorithms for Recognizable and Algebraic Series

出版者サイト複写サービスで全文入手 {{ this.onShowCLink("http://jdream3.com/copy/?sid=JGLOBAL&noSystem=1&documentNoArray=18A1365212&COPY=1") }}
高度な検索・分析はJDreamⅢで {{ this.onShowJLink("http://jdream3.com/lp/jglobal/index.html?docNo=18A1365212&from=J-GLOBAL&jstjournalNo=U0469A") }}

著者 (3件)： , ,
資料名：
巻： E101.D 号： 6 ページ： 1479-1490(J-STAGE) 発行年： 2018年
JST資料番号： U0469A ISSN： 1745-1361 資料種別：逐次刊行物 (A)
記事区分：原著論文発行国：日本 (JPN) 言語：英語 (EN)

形式級数は,各単語を係数または重みと呼ばれる値と関連づけることによる形式言語の自然拡張である。それらの中で,認識可能級数と代数的級数は,それぞれ正規言語と文脈自由言語の拡張と見なすことができる。単語wの係数は,w上の操作に必要なコスト,wを放出する確率のような量を表すことができる。形式級数の可能な応用の一つは,ソフトウェアの定量分析における文字列計数である。本論文で著者らは,形式級数の計数問題を定義し,問題のアルゴリズムを提案した。オートマトンまたは文法に対するメンバシップ問題は,所定の級数における所定の単語の係数を計算する問題に対応する。それゆえ,著者らは次の2つの方法における形式級数のための計数問題を定義した。著者らは,形式級数Sと自然数dに対して,CC(S,d)はSにおける長さdの全単語の係数の和であり,SC(S,d)はSにおける非ゼロ係数を持つ長さdの単語数であると定義した。著者らは,所定の認識可能級数Sと自然数dに対して,ηを単一状態遷移行列演算に必要な時間の上限した時に,CC(S,d)はO(ηlog d)時間で計算でき,Sの状態遷移行列が乗算に対して可換であるならば,SC(S,d)はdの多項式時間で計算できることを示した。著者らは,この概念をツリー級数に拡張し,それらを効率的に計算する方法を論じた。また著者らは,代数級数Sについて,dの二乗時間でCC(S,d)を計算するアルゴリズムを提案した。著者らは,C言語の構文を表現したものを含むいくつかの文脈自由文法SのCC(S,d)を計算するために,提案したアルゴリズムのCPU時間を示した。脆弱性分析のための文字列計数に対する提案アルゴリズムの適用性を調べるために,Kaluzaベンチマークに対する文字列計数に関する結果も示した。(翻訳著者抄録)

, , , , , , , , , , , ,

著者キーワード (4件)： , , ,

その他の計算機利用技術 , データ保護

引用文献 (35件)：

[1] P.A. Abdulla, M.F. Atig, Y.-F. Chen, L. Holík, A. Rezine, P. Rümmer, and J. Stenman, “String constraints for verification,” 26th International Conference on Computer Aided Verification (CAV 2014), pp.150-166, 2014. 10.1007/978-3-319-08867-9_10
[2] P.A. Abdulla, M.F. Atig, Y.-F. Chen, L. Holík, A. Rezine, P. Rümmer, and J. Stenman, “Norn: an SMT solver for string constraints,” 27th International Conference on Computer Aided Verification (CAV 2015), pp.462-469, 2015. 10.1007/978-3-319-21690-4_29
[3] M. Alkhalaf, T. Bultan, and J.L. Gallegos, “Verifying client-side input validation functions using string analysis,” 34th International Conference on Software Engineering (ICSE 2012), pp.947-957, 2012. 10.1109/icse.2012.6227124
[4] A. Aydin, L. Bang, and T. Bultan, “Automata-based model counting for string constraints,” 27th International Conference on Computer Aided Verification (CAV 2015), pp.255-272, 2015. 10.1007/978-3-319-21690-4_15
[5] L. Bang, A. Aydin, Q.-S. Phan, C.S. Păsăreanu, and T. Bultan, “String analysis for side channels with segmented oracles,” ACM International Symposium on the Foundations of Software Engineering (FSE 2016), pp.193-204, 2016. 10.1145/2950290.2950362

, ,

前のページに戻る