TY - JOUR
T1 - SEQUENTIAL RELATIONAL DECOMPOSITION
AU - Fried, Dror
AU - Legay, Axel
AU - Ouaknine, Joël
AU - Vardi, Moshe Y.
N1 - Publisher Copyright:
© D. Fried, A. Legay, J. Ouaknine, and M.Y. Vardi.
PY - 2022
Y1 - 2022
N2 - 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 systemdesign 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.
AB - 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 systemdesign 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.
KW - Automatic Relations
KW - Composition
KW - Decomposition
KW - Positivity
KW - Synthesis
UR - http://www.scopus.com/inward/record.url?scp=85127144155&partnerID=8YFLogxK
U2 - 10.46298/LMCS-18(1:37)2022
DO - 10.46298/LMCS-18(1:37)2022
M3 - ???researchoutput.researchoutputtypes.contributiontojournal.article???
AN - SCOPUS:85127144155
SN - 1860-5974
VL - 18
SP - 37:1-37:29
JO - Logical Methods in Computer Science
JF - Logical Methods in Computer Science
IS - 1
M1 - 1
ER -