Programme of colloquia with abstracts for the Spring 2007 semester

20 February 2007

Prof. Rudolf Freund, Vienna University of Technology

Curricula and Research Topics in ‘Informatics and Medicine’ at the Vienna University of Technology

Abstract: Recognising the growing importance of computer applications in the fields of medical sciences and healthcare, the new informatics curricula, introduced with the launch of Bachelor’s and Master’s programmes at the Vienna University of Technology in 2001, also included a Bachelor’s and a Master’s degree in “Informatics and Medicine”. The curricula comprise core modules in computer science and medicine, as well as specialised modules in medical applications. Many research projects at the Vienna University of Technology also involve applications in healthcare, ranging from the visualisation of medical data to the development of specialised equipment for people with disabilities. In the second part of my talk, I shall also outline my group’s current research topics in the field of Natural Computing, with a particular focus on results in DNA and Membrane Computing.

27 February 2007

Ing. Tomáš Vojnar, Ph.D., FIT VUT, Brno

Counter Automata in the Verification of Programmes on Lists or Trees

Abstract: We first discuss an automated approach for verifying programmes that manipulate (possibly cyclic and/or shared) singly-linked lists using counter automata as accurate models for the programmes. The control states of our counter automata correspond to abstract heap graphs where list segments without sharing are collapsed, and counters are used to keep track of the number of elements in these segments. This technique enables the verification of various safety properties of the programmes under consideration (such as the absence of null-pointer dereferences, the absence of memory leaks, shape invariance, preservation of list length, etc.) as well as programme termination. We also mention a generalisation of the technique that tracks the sortedness properties of the lists. In the second part of the talk, we then introduce a related technique for verifying tree-manipulating programmes. The technique uses abstract regular tree model checking to obtain invariants of the programmes under consideration (and to check their safety properties). Using the invariants, we construct counter automata that simulate the analysed programmes and use them to check termination. We present techniques for automatically refining the initially obtained counter automata when a spurious lasso-shaped termination counterexample is observed.

These results are a joint effort with Ahmed Bouajjani, Peter Habermehl, and Pierre Moro from LIAFA, Paris, Radu Iosif and Marius Bozga from VERIMAG, Grenoble, and Adam Rogalewicz from FIT VUT, Brno.

6 March 2007

Prof. Zoltan Esik, University of Szeged

An algebraic characterisation of logics on finite trees

Abstract: Algebraic methods have proved very powerful in obtaining *decidable* characterisations of the expressive power of logics on words. For example, every decision procedure for testing first-order definability or definability in Linear Temporal Logic of a regular language is based on testing whether the minimal automaton of the language is aperiodic (counter-free). In this talk, I will present an extension of these algebraic methods to logics on trees and discuss some applications.

13 March 2007

Doc. PhDr. Karel Pala, CSc., Mgr. Pavel Rychlý, Ph.D., FIMU, Brno

Contextual Similarity in Large Text Corpora

Abstract: Extensive text corpora are a highly valuable source of information for natural language processing, linguistics, lexicography, language teaching and other fields. It is always important to examine individual words (phrases, syntactic structures) in different contexts, as it is precisely these different contexts that have a fundamental influence on the meaning of the phenomena under investigation.

Methods and techniques for recognising different types of context will be discussed, as well as applications that utilise both individual contexts and the similarity between different contexts. Furthermore, an algorithm will be presented for the efficient calculation of similarities between all pairs of words based on the statistical characteristics of individual words.

20 March 2007

Assoc. Prof. Ing. Martin Šperka, PhD., FIIT STU, Bratislava

Research in the field of visualisation and augmented reality at FIIT STU in Bratislava

Abstract: An overview of projects in the field of research into new methods of human-computer interaction using multimedia, visualisation, virtual and augmented reality, and focused on various applications with an emphasis on e-learning . The lecture will present some pilot projects from the above-mentioned field.

21 March 2007, B011 14:00

Dr Momtchil Peev, Seibersdorf Research, Vienna

Quantum key distribution and (classical) cryptography

Abstract: Quantum key distribution (QKD) is the first real-world application of quantum information theory. On the one hand, QKD is essentially a quantum technology. At the same time, it is a (classical) cryptographic primitive that must be considered within the broader context of classical cryptography. The relationship between QKD and classical cryptography has recently been reviewed in a ‘White paper: Quantum Key Distribution and Cryptography’ by the European Integrated Project SECOQC (http://arxiv.org/abs/quant-ph/0701168). The talk aims to revisit selected topics from the aforementioned recent publication, with an emphasis on the SECOQC concept of ‘Network(s) of secrets’ and, from the author’s perspective, outlines possible future research directions in this field.

27 March 2007

Doc. RNDr. Antonín Kučera, Ph.D., FIMU, Brno

Quantitative analysis of recursive Markov chains

Abstract: Discrete Markov chains are a general model of systems, whose dynamics can be characterised by means of probability distributions on the transitions between the individual states of the system. This lecture will present in more detail a class of recursive Markov chains, which corresponds to the probabilistic extension of pushdown automata. Over the past four years, methods have been developed that make it possible to overcome the fundamental difficulties associated with the quantitative analysis of these chains and, in some cases, to carry out this analysis algorithmically. Possible applications of the results obtained include the efficient analysis of recursive random algorithms, the design of alternative ‘page-ranking’ algorithms for internet search engines, and they can also be utilised outside the field of computer science. Of particular interest is, for example, the connection with the class of so-called multitype branching processes, which are widely used in biology and genetics. The lecture does not assume any prior knowledge of the theory of stochastic processes; key concepts, results and proof techniques will be presented in a simplified form.

3 April 2007

Doc. Dr. Ing. Pavel Zemčík, FIT VUT, Brno

2D image classifiers, their applications and acceleration using DSP and FPGA. 2D Image Classifiers, their application, and acceleration through DSP and FPGA

Abstract:

• Introduction to classification, image classification, combining weak classifiers, the AdaBoost principle, features used in image processing
• Acceleration of AdaBoost in DSP/FPGA, inputs and outputs, differences in the implementation of feature extraction in software and FPGA
• Applications of image classification, demonstration of a system for red-light running detection and speed measurement with number plate recognition for road traffic

• Introduction to classification, image classification, merging of weak classifiers, the AdaBoost principle, features used in image classification
• AdaBoost acceleration in DSP/FPGA, inputs and outputs, features, differences in the implementation of feature extraction in software and FPGA
• Applications of image classification; demonstration of a system for red light infringement detection and speed measurement with number plate recognition for road traffic

10 April 2007

Prof. PhDr. Eva Hajičová, DrSc., Faculty of Mathematics and Physics, Charles University, Prague

Dependency grammar and the deep structure of the sentence

Abstract:

1. A historical perspective: The description of syntactic relations within a sentence, understood as relations between a governing and a dependent constituent: The predicate and its arguments, K.F. Becker (1837), German grammars (often distinguishing a specific relationship between the subject and the predicate; similarly in the Czech Republic, Vl. Šmilauer 1947), L. Tesnière (1959, actants and circumstants)
2. Formal grammar: Definition, the condition of projectivity – how to deal with it (see below, point 7)
3. Comparison with analysis into immediate constituents (intermediate constituents), phrase grammar. A problem similar to non-projective constructions: so-called long-distance dependencies (long-distance dependencies, unbounded dependencies).
4. From phrase grammar, via the introduction of ‘heads’, to the conclusion that all current ‘phrase-based’ descriptions include the concept of a ‘head’, i.e. a governing constituent (and the constituents dependent on it). Question: what is the purpose of dividing a sentence into phrases?
5. The following holds true: the closer a description is to a description of meaning, the more important the relationship between ‘predicate and its arguments’, ‘head’ and ‘dependents’ or similar is (C. Fillmore, J. Robinson, lexically functional grammar). Apparent counterexample: statistical models
6. AČV as a semantically relevant division – the unsuitability of division into phrases: the Prague Functional Generative Description, the introduction of so-called ‘floating constituents’ in categorical grammar (M. Steedman)
7. How to deal with non-projective features in the surface form of a sentence when describing the underlying (deep) structure: they are feature-based; verification of the theory based on the Prague Dependency Corpus (PDT)

17 April 2007

Prof. Dines Bjorner, TU Lyngby, Denmark

Domain Theories and Domain Engineering

Abstract: Before software can be designed, its requirements must be understood. Before requirements can be defined, the underlying (application) domain must be understood.

These two principles inevitably mean that proper, professional software development ideally proceeds in three phases: Domain Engineering (D) ---> Requirements Engineering (R) ---> Software Design (S), whereby the correctness of the software design is a matter of D, S |-- R; that is, proving that the software, S, meets its requirements, R, in the context of the domain, D. The ‘models’ relation, |--, formally means that a proof of the correctness of S with respect to R often has to rely on explicitly stated assumptions about the domain.

In this seminar, we shall primarily discuss Domains – and merely indicate how one can safely proceed from a domain description to a set of requirements.

We shall outline informal and formal approaches to domain descriptions and introduce the model concepts of domain facets: the intrinsic facet, the support technology facet, the management and organisation facet, the rules and regulations (and the derived script) facet, and the human behaviour facet. Throughout, we will illustrate these points with examples drawn from classical domains such as transport (railways) and others.

In ‘transforming’ domain descriptions into part of requirements specifications, we shall touch upon such (algebraic) operations as domain projection, domain instantiation, domain determination, domain extension and requirements fitting.

Finally, we shall discuss the broader role of Domain Theories and Domain Engineering – whilst suggesting a wealth of research topics...

24 April 2007

Prof. Dalibor Fronček, University of Minnesota Duluth

Want to schedule a (un)fair tournament?

Abstract: Suppose you want to organise a round-robin tournament involving 8 teams but do not have enough time to play all 28 matches. You may decide that each team will play just 5 matches rather than the usual 7. Now you need to choose which matches to omit. It certainly makes a difference if the team ranked No 4 misses the matches against the teams ranked No 1 and 2, whilst the team ranked No 5 misses the matches against the teams ranked No 7 and 8. Overall, team No 5 then faces much stronger opponents than No 4.

We will explore ways to make such a tournament as fair as possible and also how to make it unfair. We will show that these two tasks are in fact complementary and that by achieving one, we also achieve the other. To do this, we introduce some concepts from graph theory, including ‘vertex-magic vertex labelling’, and show how graph theory can help us solve the scheduling problem.

15 May 2007

Dr Rudolf Hanka, University of Cambridge

Content-Based Indexing and Browsing of Medical Images

Abstract: With the rapid growth of digital imaging modalities producing a broad spectrum of multimedia data types, medical database management is becoming increasingly complex. How to manage these sophisticated data within a medical image database with the aim of increasing the efficiency of clinical applications is a challenging research issue. The talk will describe the basis of the I-Browse system developed for this purpose at the Medical Informatics Unit in Cambridge.