Closure properties for the class of behavioral models

• Author(s): Martins, Manuel A.
• Date: 2007
• Persistent ID: http://hdl.handle.net/10773/5547
• Origin: RIA - Repositório Institucional da Universidade de Aveiro
• Subject(s): Behavioral equivalence; Behavioral specification; Equivalential logic; Hidden equational logic; Leibniz operator; Abstracting; Computer programming; Equivalence classes; Behavioral equivalence; Behavioral specification; Equivalential logic; Hidden equational logic; Leibniz operator; Formal logic
• Document Type: Article
• Language: English

Description

Hidden k-logics can be considered as the underlying logics of program specification. They constitute natural generalizations of k-deductive systems and encompass deductive systems as well as hidden equational logics and inequational logics. In our abstract algebraic approach, the data structures are sorted algebras endowed with a designated subset of their visible parts, called filter, which represents a set of truth values. We present a hierarchy of classes of hidden k-logics. The hidden k-logics in each class are characterized by three different kinds of conditions, namely, properties of their Leibniz operators, closure properties of the class of their behavioral models, and properties of their equivalence systems. Using equivalence systems, we obtain a new and more complete analysis of the axiomatization of the behavioral models. This is achieved by means of the Leibniz operator and its combinatorial properties. © 2007 Elsevier Ltd. All rights reserved. FCT via UIMA