Safe reasoning with Logic LTS

Previous work has introduced the setting of Logic Labelled Transition Systems, called Logic LTS or LLTS for short, together with a variant of ready simulation as its fully-abstract refinement preorder, which allows one to compose operational specifications using a CSP-style parallel operator and the propositional connectives conjunction and disjunction.In this article, we show how a temporal logic for specifying safety properties may be embedded into LLTS so that (a) the temporal operators are compositional for ready simulation; (b) ready simulation, when restricted to pairs of processes and formulas, coincides with the logic’s satisfaction relation; (c) ready simulation, when restricted to formulas, is entailment.The utility of this setting as a semantic foundation for mixed operational and temporal-logic specification languages is demonstrated by means of a simple example. We also adopt the concept of may- and must-transitions from modal transition systems for notational convenience, and investigate the relation between modal refinement on modal transition systems and ready simulation on LLTS.