  We investigate the fine-grained complexity of liveness verification for
leader contributor systems. These consist of a designated leader thread and an
arbitrary number of identical contributor threads communicating via a shared
memory. The liveness verification problem asks whether there is an infinite
computation of the system in which the leader reaches a final state infinitely
often. Like its reachability counterpart, the problem is known to be
NP-complete. Our results show that, even from a fine-grained point of view, the
complexities differ only by a polynomial factor.
  Liveness verification decomposes into reachability and cycle detection. We
present a fixed point iteration solving the latter in polynomial time. For
reachability, we reconsider the two standard parameterizations. When
parameterized by the number of states of the leader L and the size of the data
domain D, we show an (L + D)^O(L + D)-time algorithm. It improves on a previous
algorithm, thereby settling an open problem. When parameterized by the number
of states of the contributor C, we reuse an O*(2^C)-time algorithm. We show how
to connect both algorithms with the cycle detection to obtain algorithms for
liveness verification. The running times of the composed algorithms match those
of reachability, proving that the fine-grained lower bounds for liveness
verification are met.
