Ettekanded

Neil Ghani: Introduction to category theory

Ettekande kiled. [ps.gz, 4up.ps.gz]

Kokkuvõte: Over the last 25 years category theory has become widespread throughout theoretical computer science. I will give a series of lectures which aim to give those attending a broad understanding of motivations underlying the subject, the key definitions and some of its major applications and examples within theoretical computer science. In more detail, I will cover

  1. Basic definitions and motivations of categories functors and natural transformations
  2. Universal properties, representability, limits and colimits and adjunctions
  3. Semantics of lambda calculi using CCC's and fibrations
  4. Universal algebra, monads and higher order datatypes
  5. Labelled transition systems, bisimulation and coalgebra

Juhan Ernits: Java programmide verifitseerimine

Ettekande kiled. [pdf]

Kokkuvõte: Java programmide verifitseerimine mudelikontrolli abil on arenenud teooriast praktiliste rakendusteni. Vaatluse all on Kansase Ülikoolis välja töötatud Java mudelikontrolli tööriist Bandera. Programmide teisendusel mudelikontrolliülesandeks tuleb lahendada mitmeid probleeme. Nende seas on programmi esitamine mudelina, olekuruumi piiramine, verifitseerimistingimuste esitamine ning tulemuse interpreteerimine. Kasutusel olevate tehnikate seas on lähtuvalt verifitseerimisülesandest sõltumatute muutujate taandamine, abstraktsioon ning mudeli teisendamine keeltesse BIR ning Promela. Probleemide ning lahendusvariantide mitmekesisusest lähtuvalt on välja kujunenud Bandera modulaarne arhitektuur. Teoreetilise poole illusteerimiseks teeme läbi näite Bandera abil.

Peeter Laud: Esimesed sammud krüptograafiliste protokollide arvutuslikus mõttes korrektse konfidentsiaalsusanalüüsi suunal

Ettekande kiled. [pdf]

Kokkuvõte: Krüptograafiline protokoll kujutab endast kindla kujuga teadete vahetamist protokolli osapoolte vahel. Protokolli eesmärgiks võib olla mingi sõnumi edastamine ühelt osapoolelt teisele, nii et selle sõnumi sisu ründaja jaoks saladuseks jääks. Ründaja võib sõnumit teada saada üritades vahetatavaid teateid pealt kuulata, peale selle võib ta neid teateid ka kinni pidada ja ise uusi teateid saada.

Meid huvitab, kas ründajal on võimalik edastatava sõnumi kohta midagi teada saada või jääb sõnum konfidentsiaalseks. Veendumaks konfidentsiaalsuse säilimises, püüame me protokolliteksti analüüsida. Olemasolevad analüüsid lähtuvad protokollisemantikast ja turvalisuse definitsioonist, mis põhinevad termialgebratel (nn. Dolev-Yao mudelil), mis aga ei pruugi reaalset elu hästi modelleerida. Meie esitame oma ettekandes mõned protokolliteisendused. Ühest küljest ei muuda need teisendused seda, mis moodi see protokoll paistab ründajale, seega säilitab esialgne protokoll edastatava sõnumi konfidentsiaalsuse parajasti siis, kui seda teeb muudetud protokoll. See "ründajale paistmise samasus" on põhjendatav lähtudes protokollisemantikast ja turvalisuse definitsioonist, mis põhinevad bitijadadel ja stohhastilistel polünomiaalses ajas töötavatel algoritmidel, selline semantika modelleerib reaalset elu küllaltki hästi. Teisest küljest on muudetud protokolli tekstist (loodetavasti) otseselt järeldatav, et edastatav sõnum ei leki ründajale.

Krüptimise väljund - krüptotekst - tavaliselt ei ole vastavast avatekstist sõltumatu (vähemalt senini, kuni võti on avatekstist lühem). Sellegipoolest ütleb meie intuitsioon, et krüptitud kujul võib salajasi asju avalikuks teha, mingit infoleket see ei põhjusta. Asi on selles, et krüptotekst on talle vastavast avatekstist arvutuslikult sõltumatu - mitte ükski kiire algoritm ei ole suuteline aru saama, et nendevaheline sõltuvus olemas on.

Maido Remm: Genotüpiseerimine ja bioinformaatika - bioloogilised ja arvutuslikud probleemid

Ettekande kiled. [pdf]

Kokkuvõte: Ettekandes kirjeldan inimeste massilise genotüpiseerise käigus tekkivaid arvutuslikke probleeme ja mõningaid lahendusi neile probleemidele. Peamisteks teemadeks on: a) kvaliteetsete PCRi praimerite automaatne leidmine b) PCRi praimerite multipleks c) kromosoomide arvutuslik lahutamine (haplotüüpide leidmine) d) konserveerunud haplotüübi blokkide leidmine genoomist e) haigus-geen assotsiatsioonide leidmine.

Tarmo Uustalu: Gödeli meeldetuletus

Ettekande kiled. [pdf, 2up.ps.gz]

Kokkuvõte: Ettevalmistusena prof Gregory Chaitini loengutele talvekoolis märtsis räägime Gödeli mittetäielikkusteoreemidest. Põhiajend on, et neist ei kuule ülikoolistuudiumi jooksul mitte iga arvutiteadlane. Teine on, et nende täiesti matemaatiliste teoreemide ümber levib kõvasti müstikat ja parafilosoofiat; et mõista, mida see matemaatika tegelikult ütleb ja mida mitte, tuleb sõnastuste ja aruluskäikudega olla üsna täpne. Vaatame üle Gödeli esimese ja teise mittetäielikkusteoreemi, samuti Tarski tõe defineerimatusteoreemi.

Jüri Vain: Verification of hybrid dynamical systems

Ettekande kiled. [pdf]

Kokkuvõte: Hybrid dynamical systems (HS) are systems with interacting continuous and discrete components. That requires more than one modeling language to characterize their dynamics: topology, differential equations, automata theory. The key formalism for modeling of hybrid systems is hybrid automata that is an infinite extension of finite state automata. Almost ten years the most popular verification technique for HSs has been model checking (MC). Since MC is an algorithmic method it can terminate and be effective only in case of finite state structures. Thus, finite abstraction techniques are playing central role in verifying HS. In this talk different HS abstraction relation (e.g., forward-, backward simulation, and bisimulation) are explained and their appropriateness for model checking discussed. At last, decidability results of reachability problem for basic hybrid automata classes are presented and open problems explained.

Varmo Vene: Mendler-style Recursion Schemes for Inductive Types

Kokkuvõte: In functional programming, foldr is a standard operator that encapsulates a simple pattern of recursion for processing lists. It satisfies several nice properties, hence facilitates reasoning and optimization of programs. Similar fold operators can be defined for variety of other datatypes. In particular, the categorical modelling of inductive types as initial algebras allows define a single generic fold operator for all inductive types. However, this "conventional" approach to inductive types does not scale well for other operators which encapsulate more complex recursion patterns. Resulting operators are neither very intuitive nor easy to use.

We propose an alternative way of defining generic recursion operators, originating from N.P.Mendler's work in type theory (LICS'87). It uses parametricity to enforce the "correct usage" of recursive argument. Mendler-style operators enjoy similar properties as corresponding conventional ones, but also allow to specify functions in a style very similar to direct recursion.

Jaak Vilo: Mining the Functional Genomics Data

Ettekande kiled. [pdf]

Kokkuvõte: I will present my research into mining the functional genomics data, i.e. the gene expression, protein-protein interaction, and sequence data. I will talk about the algorithmic challenges in those analyses, one of which is the pattern discovery, i.e. the identification of novel interesting sequence features (signals) that help us to decrypt the inner workings of the biomolecular machinery, the basis of all the organic life.

Jan Willemson: Covering the Path Space: A Casebase Analysis for Mobile Robot Path Planning

Ettekande kiled. [pdf]

M. Kruusmaa, J. Villemson. Covering the Path Space: A Casebase Analysis for Mobile Robot Path Planning. [pdf]

Kokkuvõte: This paper presents a theoretical analysis of a casebase used for mobile robot path planning in dynamic environments. Unlike other case-based path planning approaches, we use a grid map to represent the environment that permits the robot to operate in unstructured environments. The objective of the mobile robot is to learn to choose paths that are less risky to follow. Our experiments with real robots have shown the efficiency of our concept. In this paper, we replace a heuristic path planning algorithm of the mobile robot with a seed casebase and prove the upper and lower bounds for the cardinality of the casebase. The proofs indicate that it is realistic to seed the casebase with some solutions to a path-finding problem so that no possible solution differs too much from some path in the casebase. This guarantees that the robot would theoretically find all paths from start to goal. The proof of the upper bound of the casebase cardinality shows that the casebase would in a long run grow too large and all possible solutions cannot be stored. In order to keep only the most efficient solutions the casebase has to be revised at run-time or some other measure of path difference has to be considered.

Helger Lipmaa
Tarmo Uustalu
Varmo Vene
Viimane uuendus 01.02.2003