An Intrinsic Characterization of Effective Topologies
Prof Dieter Spreen, University of Siegen, Germany
Thursday 4 December 2008, 16h00, M 111 (Seminar Room)
An effective topological space is a two-level structure consisting of two indexed sets: points and basic opens, as well as two enumerable relations between the two levels: membership and convergence. Numbered sets possess a variety of intrinsic topologies defined by their computability structure. We characterize those of them that are compatible with the given topology. As a consequence characterizations for two important types of topologies are obtained.
On the Definition of Computability in Analysis
Prof Klaus Weihrauch, University of Hagen, Germany
Thursday 13 November 2008, 16h00, M 111 (Seminar Room)
Basically, computability is defined for functions on finite words. Computability on other "abstract" sets such as rational numbers or finite graphs is defined via notations, where finite words are used as "names" on which concrete computations are performed (example: decimal numbers). In Computable Analysis concrete computability is generalized from finite words to the set of infinite sequences of symbols which has continuum cardinality. Then computability on "abstract" sets is defined via representations, where infinite sequences are used as "names" on which concrete computations are performed (example: infinite decimal fractions of the real numbers). The concept of computability induced on a set M depends essentially on the representation. If a structure is given on the set M the representation should be compatible with it. In some cases there is a unique computability concept compatible with the structure. In the talk we show that a very poor structure with the requirements that the element relation and set inclusion become provable suffices to define in turn computability on the points, the open sets, computability on the open sets, the compact sets and computability on the compact sets.
Symbolic Verification in Presburger-Definable Infinite-State Transition Systems
Prof Valentin Goranko, University of the Witwatersrand, Johannesburg
Thursday 6 November 2008, 16h00, M 111 (Seminar Room)
Symbolic model checking is a methodology for formal verification, based on symbolic representation of the states and transitions in systems which are to be verified, and on effective symbolic computation of the sets of states satisfying the properties of importance, such as pre- and post-conditions, reachability, safety, liveness, fairness, etc. Symbolic model checking is particularly essential in the case of infinite-state systems, which are not amenable to direct presentation and manipulation.
Presburger transition systems provide a large natural class of infinite state transition systems, suitable for modeling of various situations, such as counter automata, Petri nets, communication protocols, multi-threaded systems, etc. They are based on representation of sets of states and transition relations by means of formulae in Presburger arithmetic which has decidable satisfiability and model checking.
In this talk I will discuss briefly the general topic of formal verification of infinite-state systems, and then will present some recent work on symbolic model checking of the temporal logic of computations CTL* interpreted in a natural class of Presburger transition systems.
Joint work with Alain Finkel and Stephane Demri (LSV, ENS Cachan) and Govert van Drimmelen (Univ of Johannesburg).
Jordan Areas and Grids
PD Dr Norbert Müller, University of Trier, Germany
Thursday 25 September 2008, 16h00, M 111 (Seminar Room)
In constructive analysis, many different ways for the representation of subsets of the Euclidean space are known. Some are useful to actually draw an image of the set, while others concentrate on a precise description of its boundary. Unfortunately, these approaches are not equivalent in general. We present a closer look on the comparison of the two of these presentations especially suited for dealing with Jordan curves and their interiors.
Notions of Independence in Model Theory
Gareth Boxall, University of Leeds, UK
Thursday 14 August 2008, 16h00, M 111 (Seminar Room)
I shall present some history and basic theory around notions of independence in model theory and then focus specifically on a class of first order theories for which I recently established the existence of a notion of independence. This particular example is also part of a general approach to trying to better understand notions of independence.
On Computable Bases in Banach Spaces
Volker Bosserhoff, University of the Armed Forces, Munich, Germany
Thursday 22 May 2008, 16h00, M 111 (Seminar Room)
A sequence in a Banach space is called a (Schauder) basis if, loosely spoken, every element of the space has a unique representation as an infinite linear combination of the elements of the sequence. Complete orthonormal sequences in Hilbert spaces are examples of such bases. Within the framework of computable analysis, Brattka and Dillhage have recently developed a computable theory of compact linear operators on Banach spaces under the assumption that the spaces possess computable bases. We will discuss the question whether a computable Banach space that possesses a basis necessarily possesses a computable basis. It is well known that the answer is "yes" for Hilbert spaces. We will, however, construct a counterexample to the general statement. This construction builds on Enflo's celebrated example of a separable Banach space that lacks the so called approximation property.
Incomputability and Ontological Weight: Reverse Mathematics and Computable Analysis (Finally) Meet
Dr Guido Gherardi, University Bologna, Italy
Thursday 10 April 2008, 16h00, M 111 (Seminar Room)
We discuss the relationships between two different approaches to mathematical complexity: reverse mathematics and computable analysis. These two subjects share several methodological aspects, but they have different philosophical foundations. Reverse mathematics is interested in evaluating the weight of the ontological assumptions needed to prove the existence of mathematical entities. Computable analysis investigates the effective constructions of mathematical objects and possibly estimates the degree of insolvability of mathematical problems.
Nevertheless, we think that reverse mathematics can give useful tools to computable analysis in terms of computational complexity classification. The results obtained may sometimes respect a natural correspondence, but in other case they are to be considered as irreducible. We discuss some examples.
Hamming Weight of the Non-Adjacent-Form under Various Input Statistics
Prof Clemens Heuberger, University of Graz, Austria
Thursday 13 March 2008, 14h00, M 111 (Seminar Room)
Public key cryptography relies on the efficient calculation of one-way functions, for instance, scalar multiplication in the point group of an elliptic curve. One well-known method to perform this operation is the use of a signed binary expansion for the scalar and Horner's scheme. The number of operations is minimized if the Hamming weight (number of non-zero digits) is minimized. This is achieved by the Nonadjacent form, a signed binary expansion without adjacent non-zero digits.
In this talk, the Hamming weight of the non-adjacent form is studied in relation to the Hamming weight of the standard binary expansion. In particular, we investigate the expected Hamming weight of the NAF of a n-digit binary expansion with k ones where k is either fixed or proportional to n. The expected Hamming weight of NAFs of binary expansions with large >= n/2 Hamming weight is studied. Finally, the covariance of the Hamming weights of the binary expansion and the NAF is computed. Asymptotically, these Hamming weights become independent and normally distributed.
(based on joint work with H. Prodinger)
Enumeration Problems for Classes of Self-Similar Graphs
Dr Stephan Wagner, University of Stellenbosch
Friday 22 February 2008, 14h00, M 111 (Seminar Room)
This talk is based on joint work with E. Teufl. I describe a general construction principle for classes of self-similar graphs and show that this construction leads to polynomial systems of recurrences for various counting problems. These questions play a role in the investigation of models stemming from theoretical physics. In some cases (most notably, the enumeration of perfect matchings and spanning trees), remarkable explicit solutions can be found. In other cases, it is possible to find general asymptotic results by means of additional graph-theoretical considerations. In particular, I will demonstrate the application of an independence theorem for matchings in large graphs. Several examples involving classical graph families related to fractals will be discussed.
Probabilistic Analysis of Algorithms: What's It Good For?
Prof Conrado Martínez, Universitat Politècnica de Catalunya, Barcelona, Spain
Tuesday 12 February 2008, 14h00, M 111 (Seminar Room)
Worst-case analysis and asymptotic notations have served us well for over four decades. However, there are two main drawbacks of this type of analysis. First, they might lead to overly pessimistic predictions on the behavior of an algorithm, or they might yield answers too rough for useful comparison of competing alternatives. Secondly, they are not the right tool to analyze randomized algorithms. In this talk, I'll present some of the mathematical techniques that can be used and, by means of some examples based on my recent research, show how these techniques provide useful and interesting answers to relevant problems in Computer Science. In the meanwhile, I hope to offer a glimpse of the mathematically beautiful and challenging problems that arise in this area, and also to convince of the benefits that probabilistic analysis can yield from the practitioner's standpoint.