Liveness in broadcast networks

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 clients visits a final state infinitely often. The complexity of the problem has been open. It was shown to be $$\texttt {P}$$ P -hard but in $$\texttt {EXPSPACE}$$ EXPSPACE . We close the gap by a polynomial-time algorithm. The latter 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.

An Emergency Alert Broadcast Based on the Convergence of 5G and ATSC 3.0

We propose a novel emergency alert broadcast mechanism for mobile phone users, which is based on the convergence of 5G and ATSC 3.0. Cellular networks including 5G adopt a broadcast technique for emergency alert. This technique just delivers a text-based message. Moreover, the message only includes a limited number of characters. Therefore, cellular networks cannot afford to provide abundant information in emergency cases. Broadcast networks such as ATSC 3.0 also offer an emergency alert broadcast service. This service can deliver a multimedia-based message in emergency cases. Therefore, the ATSC 3.0 supports more abundant information in the cases of emergency alert broadcasts. Especially, the ATSC 3.0 employs wake-up functionality and location information, which enables the delivery of emergency alerts to idle-state receivers in emergency areas. However, it is unlikely that the wake-up functionality and the location information are directly applicable to mobile phone users due to some practical issues. In order to improve the emergency alert broadcast service in mobile environments, we converge the 5G and the ATSC 3.0 networks, which effectively exploits the advantages of the networks. For the convergence network, we suggest a modified table, which associates the 5G message with the ATSC 3.0 message in the cases of emergency alerts. We also present a novel scenario for delivery of the emergency alert messages. Simulation results show that the convergence significantly enhances the receiver performance for emergency alert broadcast.