  We study liveness and model checking problems for broadcast networks, a
system model of identical clients communicating via message passing. The first
problem that we consider is Liveness Verification. It asks whether there is a
computation such that one of the clients visits a final state infinitely often.
The complexity of the problem has been open since 2010 when it was shown to be
P-hard and solvable in EXPSPACE. We close the gap by a polynomial-time
algorithm. The algorithm relies on a characterization of live computations in
terms of paths in a suitable graph, combined with a fixed-point iteration to
efficiently check the existence of such paths. The second problem is Fair
Liveness Verification. It asks for a computation where all participating
clients visit a final state infinitely often. We adjust the algorithm to also
solve fair liveness in polynomial time.
  Both problems can be instrumented to answer model checking questions for
broadcast networks against linear time temporal logic specifications. The first
problem in this context is Fair Model Checking. It demands that for all
computations of a broadcast network, all participating clients satisfy the
specification. We solve the problem via the Vardi-Wolper construction and a
reduction to Liveness Verification. The second problem is Sparse Model
Checking. It asks whether each computation has a participating client that
satisfies the specification. We reduce the problem to Fair Liveness
Verification.
