Reasoning About Conditional Progress Properties

In some otherwise attractive formalisms, it can be difficult or even impossible to specify progress in such a way that a component of a distributed system can be proved correct independent of its environment. This problem arises because the nested dependencies between the component and its environment cannot be conveniently expressed in the formalism. A typical example is a communication protocol, which is supposed to provide reliable data transfer even over channels that are unboundedly lossy: the channels only deliver messages if the protocol transmits them often enough, while the protocol only guarantees reliable service if the channels deliver sufficiently many messages. This paper investigates the extent to which such progress specifications can be dealt with using predicate calculus and a single temporal operator (leads-to) having a simple proof theory. It turns out that under the proper semantic interpretation, many progress specifications expressing complex dependences can be r..