Fundamenta Informaticae - Volume 114, issue 1

Authors: Avron, Arnon | Konikowska, Beata

Article Type: Research Article

Abstract: We examine the issue of collecting and processing information from various sources, which involves handling incomplete and inconsistent information. Inspired by the framework first proposed by Belnap, we consider structures consisting of information sources which provide information about the values of formulas of classical propositional logic, and a processor which collects that information and extends it by deriving conclusions following from it according to the truth tables of classical logic, applied forward and backward. Our model extends Belnap's in allowing the sources to provide information also about complex formulas. As that framework cannot be captured using finite ordinary logical matrices, …if we want to represent each of the relevant logics with a single matrix, we employ Nmatrices for that purpose. In opposition to the approach proposed in our earlier work, we assume that the information sources are reasonable, i.e. that they provide information consistent with certain coherence rules. We provide sound and complete sequent calculi admitting strong cut elimination for the logic of a single information source, and (several variants of) the logic generated by the source and processor structures described above. In doing this, we also provide new characterizations for some known logics. We prove that, in opposition to the variantwith unconstrained information sources considered earlier, the latter logic cannot be generated by structures with any bounded number of sources. Show more

Keywords: Information processing, incomplete information, inconsistent information, finite logics, many-valued logics, non-deterministic logical matrices, sequent calculi

DOI: 10.3233/FI-2011-615

Citation: Fundamenta Informaticae, vol. 114, no. 1, pp. 1-30, 2012

Authors: Celani, Sergio | Jansana, Ramon

Article Type: Research Article

Abstract: The minimum system of Positive Modal Logic SK+ is the (∧, ∨, □, ◊, ⊥, $\top$)-fragment of the minimum normal modal logic K with local consequence. In this paper we develop some of the model theory for SK+ along the yet standard lines of the model theory for classical normal modal logic. We define the notion of positive bisimulation between two models, and we study the notions of m-saturated models and replete models. We investigate the positive maximal Hennessy-Milner classes. Finally, we present a Keisler-Shelah type theorem for positive bisimulations, a characterization of the first-order formulas …invariant for positive bisimulations, and two definability theorems by positive modal sequents for classes of pointed models. Show more

DOI: 10.3233/FI-2011-616

Citation: Fundamenta Informaticae, vol. 114, no. 1, pp. 31-54, 2012

Authors: Chiniforooshan, Ehsan | Kari, Lila | Xu, Zhi

Article Type: Research Article

Abstract: Repetition avoidance has been intensely studied since Thue's work in the early 1900's. In this paper, we consider another type of repetition, called pseudopower, inspired by the Watson-Crick complementarity property of DNA sequences. A DNA single strand can be viewed as a string over the four-letter alphabet {A,C,G, T}, wherein A is the complement of T, while C is the complement of G. Such a DNA single strand will bind to a reverse complement DNA single strand, called its Watson-Crick complement, to form a helical double-stranded DNA molecule. The Watson-Crick complement of a DNA strand is deducible from, and thus …informationally equivalent to, the original strand. We use this fact to generalize the notion of the power of a word by relaxing the meaning of “sameness” to include the image through an antimorphic involution, the model of DNA Watson-Crick complementarity. Given a finite alphabet Σ, an antimorphic involution is a function θ : Σ* → Σ* which is an involution, i.e., θ2 equals the identity, and an antimorphism, i.e., θ(uv) = θ(v)θ(u), for all u ∈ Σ* . For a positive integer k, we call a word w a pseudo-kth-power with respect to θ if it can be written as w = u1 ... uk , where for 1 ≤ i, j ≤ k we have either ui = uj or ui = θ(uj ). The classical kth-power of a word is a special case of a pseudo-kth-power, where all the repeating units are identical. We first classify the alphabets Σ and the antimorphic involutions θ for which there exist arbitrarily long pseudo-kth-power-free words. Then we present efficient algorithms to test whether a finite word w is pseudo-kth-power-free. Show more

Keywords: pseudopower, pseudosquare, pseudocube, antimorphic involution, pattern avoidance

DOI: 10.3233/FI-2011-617

Citation: Fundamenta Informaticae, vol. 114, no. 1, pp. 55-72, 2012

Authors: Guerra, Esther | de Lara, Juan

Article Type: Research Article

Abstract: QVT is the standard for model transformation defined by the OMG in the context of the Model-Driven Architecture. It is made of several transformation languages. Among them, QVT-Relations is the one with the highest level of abstraction, as it permits developing bidirectional transformations in a declarative, relational style. Unfortunately, the standard only provides a semiformal description of its semantics, which hinders analysis and has given rise to ambiguities in existing tool implementations. In order to improve this situation, we propose a formal, algebraic semantics for QVT-Relations check-only transformations, defining a notion of satisfaction of QVT-Relations specifications by models.

Keywords: Model-Driven Engineering, Model Transformation, QVT-Relations, Category Theory

DOI: 10.3233/FI-2011-618

Citation: Fundamenta Informaticae, vol. 114, no. 1, pp. 73-101, 2012

Authors: Yu, Jia | , Fanyu | Kong, | Cheng, Xiangguo | Hao, Rong | Fan, Jianxi

Article Type: Other

DOI: 10.3233/FI-2011-619

Citation: Fundamenta Informaticae, vol. 114, no. 1, pp. 103-103, 2012