On the Logic of TLAp
keywords: Temporal logic, reactive systems, specification, verification, refinement
TLAp is a language intended for the high-level specification of reactive, distributed, and in particular asynchronous systems. Combining the linear-time temporal logic TLA and classical set-theory, it provides an expressive specification formalism and supports assertional verification.
reference: Vol. 22, 2003, No. 3-4, pp. 351–379
