In the past, research on publish/subscribe has concentrated on informal analyses and systems offering best-effort functionality. However with the increasing popularity of publish/subscribe, the need for a formal treatment and for system giving more stringent guarantees rises. We use propositional linear temporal logic to derive a requirement specification for publish/subscribe systems guaranteeing message completeness. In a message-complete publish/subscribe system, the system eventually acknowledges subscriptions and guarantees the delivery of notifications matching acknowledged subscriptions. After deriving the requirement specification which consists of a safety and a liveness property, we describe a possible implementation of message-complete publish/subscribe systems using a system specification based on fair transition systems. The implementation is realized in a modular way using a system not guaranteeing message-completeness. This way, message-completeness is kept orthogonal to the routing algorithms which are used to route notifications from producers to interested consumers.