In this paper we develop a new method for describing in temporal logic in a compositional manner sequential composition, its iterated version (loops) and its interaction with (nested) parallelism. The logic we will use will be a linear time logic with as sole temporal operator the until. We will illustrate this method in the construction of a compositional proof system for a CSP-like language. We will prove this system to be sound and (relative) complete.
Boer, de, F. S. (1990). Compositionality in the temporal logic of concurrent systems (extended abstract). Future Generation Computer Systems, 6(3), 287-299. https://doi.org/10.1016/0167-739X(90)90025-9