Previous work has introduced the setting of Logic LTS, together with a variant of ready simulation as fully-abstract refinement preorder, which allows one to compose operational specifications using a CSP-style parallel operator as well as the propositional connectives conjunction and disjunction. In this paper, we show how a temporal logic for specifying safety properties may be embedded into Logic LTS so that (a) the temporal operators are compositional for ready simulation and (b) ready simulation, when restricted to pairs of processes and formulas, coincides with the logic's satisfaction relation. The utility of this setting as a semantic foundation for mixed operational and temporal-logic specification languages is demonstrated via a simple example. © Springer-Verlag Berlin Heidelberg 2009.
CITATION STYLE
Lúttgen, G., & Vogler, W. (2009). Safe reasoning with logic LTS. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5404 LNCS, pp. 376–387). https://doi.org/10.1007/978-3-540-95891-8_35
Mendeley helps you to discover research relevant for your work.