Una coinstitución para la lógica de comportamiento abstracto
Jaime Andrés Castaño Perea, Guillermo Ortíz Rico · Dialnet (Universidad de la Rioja) · 2014
Recently, the specification of a problem in computer sciences–an intermediate step between the given problem and its implementation as a software system that guarantees its solution– uses universal algebra and coalgebra theories for its description. This stage includes a syntactic and a semantic component, having a logic system as result. In [3], the case of many-sorted equational logic is studied for the purpose of specification problems. Dually, in [9] an abstract behavioral logic, which models processes and coalgebraic systems behavior is studied. In both logics, the syntactic and semantic components are connected via a satisfaction relation, characterized by the following principle: the truth of formulas is invariant under language translations. In a general and modern framework, we use the institutions in algebraic specification and coinstitutions in coalgebraic specification. We research a particular case of behavioral abstract logic presented in [9], in which coalgebras are restricted to polinomial functors. We identify the respective algebraic coinstitution, detail all its components, and explicitly present the satisfaction relation as the final result.