Encoding safety in CLLR

Abstract Graphical representation (representing logical specifications by means of one or several labelled transition systems) is a typical connection between process algebra and temporal logic, the two main paradigms that specify and reason about reactive concurrent systems. In this paper, we encode (represent “graphically”) a fragment of Action-based CTL, proposed by Luttgen and Vogler, in the process calculus CLL R . In this way, safety properties can be described easily, and usual process operators (parallel, choice, etc.), logical operators (conjunction and disjunction) and temporal operators (always, until, etc.) can be mixed freely in CLL R .