Synchronizing words under LTL constraints

Synchronizing a (deterministic, finite-state) automaton is the problem of finding a sequence of actions to be played in the automaton in order to end up in the same state independently of the starting state. We consider synchronization with LTL constraints on the executions leading to synchronization, extending the results of Petra Wolf (2020) [23] by showing that the problem is PSPACE-complete for LTL as well as for restricted fragments (involving only modality F or G), while it is NP-complete for constraints expressed using only modality X.(c) 2023 Elsevier B.V. All rights reserved.