Fundamenta Informaticae - Volume 150, issue 3-4

Authors: Baelde, David | Carayol, Arnaud | Matthes, Ralph | Walukiewicz, Igor

Article Type: Other

DOI: 10.3233/FI-2017-1468

Citation: Fundamenta Informaticae, vol. 150, no. 3-4, pp. i-ii, 2017

Authors: Grathwohl, Niels Bjørn Bugge | Henglein, Fritz | Kozen, Dexter

Article Type: Research Article

Abstract: We give a natural complete infinitary axiomatization of the equational theory of the context-free languages, answering a question of Leiß (1992).

Keywords: Context free languages, Kleene algebra, algebraically complete semirings, Conway semirings, μ-semiring

DOI: 10.3233/FI-2017-1469

Citation: Fundamenta Informaticae, vol. 150, no. 3-4, pp. 241-257, 2017

Authors: Berardi, Stefano | de’ Liguoro, Ugo

Article Type: Research Article

Abstract: We consider the problem of finding pre-fix points of interactive realizers over arbitrary knowledge spaces, obtaining a relative recursive procedure. Knowledge spaces and interactive realizers are an abstract setting to represent learning processes, that can interpret non-constructive proofs. Atomic pieces of information of a knowledge space are stratified into levels, and evaluated into truth values depending on knowledge states. Realizers are then used to define operators that extend a given state by adding answers and possibly forcing us to remove some: in the learning process states of knowledge change non-monotonically. Existence of a pre-fix point of a realizer is equivalent …to the termination of the learning process with some state of knowledge which is free of patent contradictions and such that there is nothing to add. In this paper we generalize our previous results in the case of level 2 knowledge spaces and deterministic operators to the case of ω-level knowledge spaces and of non-deterministic operators. Show more

DOI: 10.3233/FI-2017-1470

Citation: Fundamenta Informaticae, vol. 150, no. 3-4, pp. 259-280, 2017

Authors: Dawar, Anuj | Holm, Bjarki

Article Type: Research Article

Abstract: We define a general framework of partition games for formulating two-player pebble games over finite structures. The framework we introduce includes as special cases the pebble games for finite-variable logics with and without counting. It also includes a matrix-equivalence game , introduced here, which characterises equivalence in the finite-variable fragments of the matrix-rank logic of [Dawar et al. 2009]. We show that one particular such game in our framework, which we call the invertible-map game , yields a family of polynomial-time approximations of graph isomorphism that is strictly stronger than the well-known Weisfeiler-Leman method. We show that the equivalence …defined by this game is a refinement of the equivalence defined by each of the games for finite-variable logics. Show more

DOI: 10.3233/FI-2017-1471

Citation: Fundamenta Informaticae, vol. 150, no. 3-4, pp. 281-316, 2017

Authors: Mio, Matteo | Simpson, Alex

Article Type: Research Article

Abstract: The paper explores properties of the Łukasiewicz μ -calculus , or Łμ for short, an extension of Łukasiewicz logic with scalar multiplication and least and greatest fixed-point operators (for monotone formulas). We observe that Łμ terms, with n variables, define monotone piece-wise linear functions from [0, 1]n to [0, 1]. Two effective procedures for calculating the output of Łμ terms on rational inputs are presented. We then consider the Łukasiewicz modal μ -calculus, which is obtained by adding box and diamond modalities to Łμ . Alternatively, it can be viewed as a generalization …of Kozen’s modal μ -calculus adapted to probabilistic nondeterministic transition systems (PNTS’s). We show how properties expressible in the well-known logic PCTL can be encoded as Łukasiewicz modal μ -calculus formulas. We also show that the algorithms for computing values of Łukasiewicz μ -calculus terms provide automatic (albeit impractical) methods for verifying Łukasiewicz modal μ -calculus properties of finite rational PNTS’s. Show more

Keywords: Łukasiewicz logic, Probabilistic μ-Calculus, Model Checking, PCTL

DOI: 10.3233/FI-2017-1472

Citation: Fundamenta Informaticae, vol. 150, no. 3-4, pp. 317-346, 2017

Authors: Jeannin, Jean-Baptiste | Kozen, Dexter | Silva, Alexandra

Article Type: Research Article

Abstract: Functional languages offer a high level of abstraction, which results in programs that are elegant and easy to understand. Central to the development of functional programming are inductive and coinductive types and associated programming constructs, such as pattern-matching. Whereas inductive types have a long tradition and are well supported in most languages, coinductive types are subject of more recent research and are less mainstream. We present CoCaml, a functional programming language extending OCaml, which allows us to define recursive functions on regular coinductive datatypes. These functions are defined like usual recursive functions, but parameterized by an equation solver. We …present a full implementation of all the constructs and solvers and show how these can be used in a variety of examples, including operations on infinite lists, infinitary γ-terms, and p -adic numbers. Show more

Keywords: Functional programming, coinductive types, recursive types, coalgebra

DOI: 10.3233/FI-2017-1473

Citation: Fundamenta Informaticae, vol. 150, no. 3-4, pp. 347-377, 2017

Authors: Cîrstea, Corina

Article Type: Research Article

Abstract: We consider state-based systems modelled as coalgebras whose type incorporates branching, and show that suitably adapting the definition of coalgebraic bisimulation yields a general and uniform account of the linear-time behaviour of a state in such a coalgebra. By moving away from a boolean universe of truth values, our approach can measure the extent to which a state in a system with branching is able to exhibit a particular linear-time behaviour. This instantiates to measuring the probability of a specific behaviour occurring in a probabilistic system, or measuring the minimal cost of exhibiting a given behaviour in the case of …weighted computations. Show more

Keywords: coalgebra, linear time, trace

DOI: 10.3233/FI-2017-1474

Citation: Fundamenta Informaticae, vol. 150, no. 3-4, pp. 379-406, 2017

Authors: Milius, Stefan | Litak, Tadeusz

Article Type: Research Article

Abstract: Motivated by the recent interest in models of guarded (co-)recursion, we study their equational properties. We formulate axioms for guarded fixpoint operators generalizing the axioms of iteration theories of Bloom and Ésik. Models of these axioms include both standard (e.g., cpo-based) models of iteration theories and models of guarded recursion such as complete metric spaces or the topos of trees studied by Birkedal et al. We show that the standard result on the satisfaction of all Conway axioms by a unique dagger operation generalizes to the guarded setting. We also introduce the notion of guarded trace operator on a category, …and we prove that guarded trace and guarded fixpoint operators are in one-to-one correspondence. Our results are intended as first steps leading, hopefully, towards future description of classifying theories for guarded recursion. Show more

DOI: 10.3233/FI-2017-1475

Citation: Fundamenta Informaticae, vol. 150, no. 3-4, pp. 407-449, 2017

Article Type: Other

Citation: Fundamenta Informaticae, vol. 150, no. 3-4, pp. 451-452, 2017