Temporal relevant logic as the logic basis for reasoning about dynamics of concurrent systems

摘要

Specifying, reasoning, and proving desirable properties of a concurrent system are an important formal technique to achieve the reliability of the system. The logic system that is widely used in the current approaches to specifying, reasoning, and proving properties of a concurrent system is temporal classical logic. This paper proposes a novel research direction, i.e., reasoning about dynamics of concurrent systems prescriptively and predictively using temporal relevant logic. We show that temporal relevant logic is a suitable logical basis that is sounder than temporal classical logic for the purpose to reason about the properties of a concurrent system from some primitive requirements of the system.