Nicolas Markey

Résumé

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. Synchronization under dynamic constraints. FSTTCS'20] 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.

@article{ipl182()-BFM,
  author =              {Bertrand, Nathalie and Francon, Hugo and Markey,
                         Nicolas},
  title =               {Synchronizing words under {LTL} constraints},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {182},
  year =                {2023},
  month =               aug,
  doi =                 {10.1016/j.ipl.2023.106392},
  abstract =            {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~\textsf{LTL} constraints on the executions
                         leading to synchronization, extending the results
                         of~[Petra~Wolf. Synchronization under dynamic
                         constraints. FSTTCS'20] by~showing that the problem
                         is \textsf{PSPACE}-complete for~\textsf{LTL} as well
                         as for restricted fragments (involving only
                         modality~\textsf{F} or~\textsf{G}), while it is
                         \textsf{NP}-complete for constraints expressed using
                         only modality~\textsf{X}.},
}