Safety Verification of Wait-Only Non-Blocking Broadcast Protocols
Broadcast protocols are programs designed to be executed by networks of processes. Each process runs the same protocol, and communication between them occurs in synchronously in two ways: broadcast, where one process sends a message to all others, and rendez-vous, where one process sends a message to at most one other process. In both cases, communication is non-blocking, meaning the message is sent even if no process is able to receive it. We consider two coverability problems: the state coverability problem asks whether there exists a number of processes that allows reaching a given state of the protocol, and the configuration coverability problem asks whether there exists a number of processes that allows covering a given configuration. These two problems are known to be decidable and Ackermann-hard. We show that when the protocol is Wait-Only (i.e., it has no state from which a process can both send and receive messages), these problems become P-complete and PSPACE-complete, respectively.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Safety Verification and Control for Collision Avoidance at Road Intersections
This paper presents the design of a supervisory algorithm that monitors safety at road intersections and overrides drivers with a safe input when necessary. The design of the supervisor consists of two parts: safety veri…
BlockingCollision AvoidanceSchedulingNon-Blockingness Verification of Bounded Petri Nets Using Basis Reachability Graphs -- An Extended Version With Benchmarks
In this paper, we study the problem of non-blockingness verification by tapping into the basis reachability graph (BRG). Non-blockingness is a property that ensures that all pre-specified tasks can be completed, which is…
Verification of Nonblockingness in Bounded Petri Nets With Minimax Basis Reachability Graphs
This paper proposes a semi-structural approach to verify the nonblockingness of a Petri net. We construct a structure, called minimax basis reachability graph (minimax-BRG): it provides an abstract description of the rea…
BlockingLearning to Wait: Synchronizing Agents with the Physical World
Real-world agentic tasks, unlike synchronous Markov Decision Processes (MDPs), often involve non-blocking actions with variable latencies, creating a fundamental \textit{Temporal Gap} between action initiation and comple…
Impact of UAVs Equipped with ADS-B on the Civil Aviation Monitoring System
In recent years, there is an increasing demand for unmanned aerial vehicles (UAVs) to complete multiple applications. However, as unmanned equipments, UAVs lead to some security risks to general civil aviations. In order…
BlockingPosition