Encoding safety in \(\mathrm{CLL}_R\) (Q2055960)

This paper falls into a line of work trying to integrate methods of formal specification with process algebras and temporal logics. It uses two formalisms created for this respect, namely logic-labeled transition systems [\textit{G. Lüttgen} and \textit{W. Vogler}, Theor. Comput. Sci. 373, No. 1--2, 19--40 (2007; Zbl 1111.68085)], an extension of ordinary labeled transition systems that better supports reasoning about processes' ready behaviour, and the authors' own process calculus \(\mathrm{CLL}_R\) that extends the well-known process algebra CSS with conjunction and disjunction on process terms. The main result of the paper is then a translation of the universal-path fragment of action-based CTL into \(\mathrm{CLL}_R\) (as a syntactic representation of particular logic-labeled transition systems) that characterises ready simulation in the following sense. Let \(\varphi\) be a formula of this fragment and \(p_\varphi\) be its translation into a process term. Then for any process term \(q\) we have that \(q \models \varphi\) iff \(q\) is ready-simulated by \(p_\varphi\). This result is established through a series of technical lemmas. To follow the constructions in detail, some preliminary knowledge on the common techniques used in process algebra is helpful.