一句话:将非周期语言的可判定性推广到有理转换,证明可判定转换是否属于给定同余类,并得一阶可定义性 PSPACE-完全。
有理字语言可由有限状态自动机、有理表达式、有限同余或 MSO 逻辑等价定义;非周期语言作为稳健子类,可由无计数器自动机、无星表达式、非周期有限同余或 FO 逻辑定义。其代数刻画可判定正则语言是否非周期。本文将这一可判定性结果推广到有理转换,即有限状态转换器定义的字到字函数。已有工作也提出了有理转换的逻辑与代数刻画。本文主要结果是:给定一个有限状态转换器,可以判定其定义的有理转换是否属于某个可判定的同余类。作者还建立了从语言上的逻辑-代数等价到转换上的等价的迁移结果。由此可判定有理转换是否一阶可定义,并证明该问题 PSPACE-完全。
Rational word languages can be defined by several equivalent means: finite state automata, rational expressions, finite congruences, or monadic second-order (MSO) logic. The robust subclass of aperiodic languages is defined by: counter-free automata, star-free expressions, aperiodic (finite) congruences, or first-order (FO) logic. In particular, their algebraic characterization by aperiodic congruences allows to decide whether a regular language is aperiodic. We lift this decidability result to rational transductions, i.e., word-to-word functions defined by finite state transducers. In this context, logical and algebraic characterizations have also been proposed. Our main result is that one can decide if a rational transduction (given as a transducer) is in a given decidable congruence class. We also establish a transfer result from logic-algebra equivalences over languages to equivalences over transductions. As a consequence, it is decidable if a rational transduction is first-order definable, and we show that this problem is PSPACE-complete.
@article{paperbot735,
title = {Logical and Algebraic Characterizations of Rational Transductions},
author = {Emmanuel Filiot and Olivier Gauwin and Nathan Lhote},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 4},
year = {2019},
doi = {10.23638/lmcs-15(4:16)2019}
}