Synchronization of Logics |
| |
Authors: | Sernadas Amílcar Sernadas Cristina Caleiro Carlos |
| |
Affiliation: | (1) Departamento de Matemática, IST, Av. Rovisco Pais, 1096 Lisboa, Portugal |
| |
Abstract: | Motivated by applications in software engineering, we propose two forms of combination of logics: synchronization on formulae and synchronization on models. We start by reviewing satisfaction systems, consequence systems, one-step derivation systems and theory spaces, as well as their functorial relationships. We define the synchronization on formulae of two consequence systems and provide a categorial characterization of the construction. For illustration we consider the synchronization of linear temporal logic and equational logic. We define the synchronization on models of two satisfaction systems and provide a categorial characterization of the construction. We illustrate the technique in two cases: linear temporal logic versus equational logic; and linear temporal logic versus branching temporal logic. Finally, we lift the synchronization on formulae to the category of logics over consequences systems. |
| |
Keywords: | combination of logics synchronization on formulae synchronization on models temporal logic equational logic |
本文献已被 SpringerLink 等数据库收录! |
|