一句话：形式化按输入/输出关系描述的规范顺序分解问题，并刻画其在不同表示下的计算复杂度。
论文研究如何将任务按顺序分解为两个先后执行的子任务。作者把任务建模为输入/输出关系，并定义顺序分解问题：判定给定规范是否存在满足顺序组合关系的分解。论文分别在显式给出任务、用布尔电路表示任务、以及用自动关系表示任务三种设定下分析复杂度，证明对应问题分别为 NP 完全、NEXPTIME 完全，并在自动关系设定下给出不可判定的证据。结果说明分解作为系统设计方法在计算上并不简单；此外，若允许人在回路中提供分解提示，问题复杂度会显著降低。
The concept of decomposition in computer science and engineering is considered a fundamental component of computational thinking and is prevalent in design of algorithms, software construction, hardware design, and more. We propose a simple and natural formalization of sequential decomposition, in which a task is decomposed into two sequential sub-tasks, with the first sub-task to be executed before the second sub-task is executed. These tasks are specified by means of input/output relations. We define and study decomposition problems, which is to decide whether a given specification can be sequentially decomposed. Our main result is that decomposition itself is a difficult computational problem. More specifically, we study decomposition problems in three settings: where the input task is specified explicitly, by means of Boolean circuits, and by means of automatic relations. We show that in the first setting decomposition is NP-complete, in the second setting it is NEXPTIME-complete, and in the third setting there is evidence to suggest that it is undecidable. Our results indicate that the intuitive idea of decomposition as a system-design approach requires further investigation. In particular, we show that adding a human to the loop by asking for a decomposition hint lowers the complexity of decomposition problems considerably.
@article{paperbot1717,
title = {Sequential Relational Decomposition},
author = {Dror Fried and Axel Legay and Joël Ouaknine and Moshe Y. Vardi},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 1},
year = {2022},
doi = {10.46298/lmcs-18(1:37)2022}
}