2019/10/31 by Béatrice Bérard, Bérard, Béatrice, Benedikt Bollig +5
Computer Science · #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1910.14294
openalex publication_date 2019/10/31 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We study the synthesis problem for systems with a parameterized number of\nprocesses. As in the classical case due to Church, the system selects actions\ndepending on the program run so far, with the aim of fulfilling a given\nspecification. The difficulty is that, at the same time, the environment\nexecutes actions that the system cannot control. In contrast to the case of\nfixed, finite alphabets, here we consider the case of parameterized alphabets.\nAn alphabet reflects the number of processes that are static but unknown. The\nsynthesis problem then asks whether there is a finite number of processes for\nwhich the system can satisfy the specification. This variant is already\nundecidable for very limited logics. Therefore, we consider a first-order logic\nwithout the order on word positions. We show that even in this restricted case\nsynthesis is undecidable if both the system and the environment have access to\nall processes. On the other hand, we prove that the problem is decidable if the\nenvironment only has access to a bounded number of processes. In that case,\nthere is even a cutoff meaning that it is enough to examine a bounded number of\nprocess architectures to solve the synthesis problem.\n