雙向有限狀態傳感器之有限值與分解分析

On the Finite-Valuedness and the Decomposition of Two-Way Finite Transducers

顏玓德(Di-De Yen)

指導教授 ： 顏嗣鈞

國立臺灣大學/電機資訊學院/電機工程學研究所/博士(2021年)

https://doi.org/10.6342/NTU202100353

摘要

在這篇論文中，我們探討了傳感器(transducer)輸出值的相關問題。如果存在一常數，使得對所有可能的輸入字串，一傳感器輸出值的各數最多為該常數，則我們稱此傳感器為有限值傳感器。若該常數為1，則我們稱此傳感器為單值傳感器。若一傳感器不為有限值傳感器，則為無限值傳感器。在此篇論文中，我們證明了對雙向傳感器而言，存在一演算法可判定任一雙向傳感器是否為有限傳感器。我們更進一步證明的，所有的雙向傳感器都可分解成有限多個單值傳感器。另外，我們也探討了象徵式傳感器(symbolic finite transducer)的輸出值問題。

在一篇1990的文獻中，韋伯(Weber)透過定義了兩個可描述任一有限傳感器(finite transducer)的準則，證明了對有限傳感器而言，有限值問題是可判定的。在此篇論文中，我們將此二準則推廣成雙向傳感器的版本，並證明了此二準則亦可用來判定一雙向傳感器是否為有限值傳感器。為了證明，對任一雙向傳感器，其有限值問題是可判定的。我們亦證明了，對任一傳感器是否符合此二準則是可判定的。但由於雙向傳感器計算路徑的複雜，為了得到此一結果，我們引入了模式(pattern)的概念，用以分析與分類各種計算路徑。

對有限傳感器而言，任一有限值傳感器都可被分解成有限多個單值傳感器。在此篇論文中，對雙向傳感器，我們亦證明得到相同的結果。但此分解過程卻較有限傳感器的分解過程複雜許多。分解步驟主要可分為三部分。第一個部分中，我們將雙向傳感器轉換成輸出值只有使用一種符號的有限傳感器。但此轉換保證了雙向傳感器的計算路徑都能完整地被保留在此有限傳感器的計算路徑之中。接著我們將該有限傳感器分解成有限多個傳感器，且每一傳感器所對映到的雙向傳感器的輸出值都是單一值的。最後，我們使用de Souza在一篇2013文獻中所介紹的方法，將所有的有限傳感器再次轉換成雙向單值傳感器。

在文章的最後一部分，我們探討了符號式傳感器的輸出值問題。符號式傳感器是有限傳感器模型的一種推廣模型。由於每一個符號式傳感器的過度(transition)都代表了有限傳感器的一組過度的集合(此集合可為無限集)，因此一符號式傳感器能更簡潔的表達一字串所形成的二元關係(binary relation)。符號式傳感器的單值問題已在文獻中被完整的探討過。在此篇文章中，我們分別討論了k-值問題與有限值問題。

關鍵字

輸出值 ； 分解 ； 有限狀態傳感器 ； 雙向 ； 模式 ； 串流式有限狀態傳感器

並列摘要

A transducer is finite-valued if the maximal number of different outputs for any input string is bounded by a constant and is k-valued (resp., single-valued) if the constant is k (resp., one). This dissertation studies the valuedness problem for transducers. It answers an open problem in the affirmative that the finite-valuedness problem for two-way finite transducers is decidable. Also this dissertation derives the decomposability of finite-valued two-way finite transducers and studies the valuedness problem for symbolic finite transducers.

In his 1990 paper, Weber gave two criteria to characterize the finite-valuedness of one-way finite transducers in terms of transducer's structure. As the structural criteria can be checked easily, the decidability of finite-valuedness follows immediately. As crossing sequences in two-way automata often play similar roles as states in their one-way counterparts, we consider analogous criteria in the setting of crossing sequences for two-way finite transducers. We show that the crossing sequence version of Weber's criteria also characterize the finite-valuedness of two-way finite transducers and are decidable properties.

For the derivation of the criteria, we consider the patterns of two-way computations and divide them into classes. Although the crossing sequence version of Weber's criteria capture the finite-valuedness of two-way finite transducers, the derivation of the finite-valuedness problem's decidability is non-trivial. First, there are infinitely many crossing sequences. Unlike the study of finite automata, we cannot just assume that the length of the crossing sequences is bounded by the number of the states, a constant, and consider only finitely many crossing sequences. For each two-way finite transducer, we can effectively verify whether a transducer is a bounded-crossing transducer. If a two-way finite transducer is bounded-crossing, we can just consider a finite number of crossing sequences; otherwise, it is not finite-valued. We then derive the crossing sequence version of Weber's criteria and show that the criteria are decidable properties for bounded-crossing transducers by reduced them into the emptiness problem of reversal-bounded multi-counter machines.

As shown by Weber, finite-valued one-way finite transducers enjoy a nice property that they can be decomposed into finitely many single-valued ones. In this dissertation, we establish an analogous decomposability result by showing that every finite-valued two-way finite transducer can also be decomposed into finitely many single-valued ones. The process of decomposition is divided into steps. First, the two-way transducer is transformed into a unary one-way finite transducer with all the two-way computation information being kept. Then, the unary one-way transducer is decomposed into finitely many ones, and each of the transducers corresponds to a single-valued two-way transducer. Finally, we apply a technique called pathfinding, introduced by de Souza, to the one-way finite transducers and convert them into two-way transducers.

Symbolic finite transducers are extensions of classical finite transducers. A transition of a symbolic finite transducer represents a (possibly infinite) set of transitions of a classical one. This setting allows symbolic finite transducers to succinctly recognize transductions. At the end of the dissertation, we study the valuedness problem for symbolic finite transducers. It is known that, for symbolic finite transducers over decidable label theory, the single-valuedness problem is decidable. We show that, in the same setting, the k-valuedness problem is decidable. Then we extend the Weber's criteria for the characterization of symbolic finite transducers' finite-valuedness.

並列關鍵字

valuedness ； decomposition ； transducer ； two-way ； pattern ； streaming string transducer

參考文獻

[1] R. Alur. Streaming string transducers. In L. D. Beklemishev and R. de Queiroz, editors, Logic, Language, Information and Computation, pages 1–1, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg.

[2] R. Alur and J. V. Deshmukh. Nondeterministic streaming string transducers. In L. Aceto, M. Henzinger, and J. Sgall, editors, Automata, Languages and Programming, pages 1–20, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg.

[3] R. Alur and P. Černý. Expressiveness of streaming string transducers. In K. Lodaya and M. Mahajan, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), volume 8 of Leibniz International Proceedings in Informatics (LIPIcs), pages 1–12, Dagstuhl, Germany, 2010. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.

[4] F. Baschenis, O. Gauwin, A. Muscholl, and G. Puppis. One-way definability of sweeping transducers. Dec. 2015.

[5] F. Baschenis, O. Gauwin, A. Muscholl, and G. Puppis. One-way definability of two-way word transducers. Logical Methods in Computer Science, 14:1–54, 2018.