We present a compositional semantics of synchronous systems that captures both safety and liveness properties of such systems. The fair synchronous transition systems (FSTS) model we introduce in this paper extends the basic alpha-STS model [Kesten and Pnueli] by introducing operations for parallel composition, for the restriction of variables, and by addressing fairness. We introduce a weak fairness (justice) condition which ensures that any communication deadlock in a system can only occur through the need for external synchronization. We present an extended version of linear time temporal logic (ELTL) for expressing and proving safety and liveness properties of synchronous specifications, and provide a sound and compositional proof system for it.
A.P. Ravn and H. Rischel, editors, FTRTFT 98: 5th International School and Symposium on Formal Techniques in Real-time and Fault-tolerant Systems, Lecture Notes in Computer Science. Springer-Verlag, 1998. , pages ????.