Programme of colloquia with abstracts for the Spring 2003 semester

4 March 2003

Doc. Lubos Brim, CSc, Faculty of Informatics, Masaryk University, Brno

Parallel and distributed model checking

Abstract: Model checking has already proved its usefulness in system verification. It is successfully applied to find subtle bugs in complex systems. However, it is limited to medium-sized systems due to its high space requirements. Many approaches to overcome this problem have been suggested. In recent years, there has been growing interest in parallelising and/or distributing model checking with the aim of achieving greater memory capacity and computational power. In this talk, we will survey some of the approaches to distributing model checking algorithms. We will consider enumerative algorithms that handle reachability, as well as LTL, CTL and Mu-calculus model checking.

18 March 2003

Prof. Miroslav Sveda, FIT, Brno University of Technology

Reuse of formal specifications for the design of embedded systems

Abstract: Formal methods appear too costly for widespread industrial use. Common paradigms dictate the use of reuse in such cases. We will present the reuse of behavioural specifications utilising state or timed-state sequences, and their closed-form descriptions via finite-state or timed automata, using two case studies based on real design projects: (1) a petrol station dispenser controller and (2) a multiple lift control system. In the talk, we will focus both on the identification of reusable component specifications and on their retrieval, adaptation and storage, supported by case-based reasoning.

25 March 2003

Doc. Antonin Kucera, Faculty of Informatics, Masaryk University, Brno

Factors and Filtration of Transient Systems

Abstract: Semantic equivalences between a process and the modal logic of that process define two techniques for reducing the state space of transient systems that, at first glance, appear unrelated. The first is the factorisation of the state space according to a given semantic equivalence; the second is the filtration of a transitional system according to a given modal logic formula. We shall demonstrate how these two techniques are related and what further observations can be drawn from this connection. The lecture does not require any specialised knowledge; we shall start from the basic concepts of automata theory and formal logic. Finally, we shall suggest possible extensions of the results presented.

1 April 2003

Prof. Milos Druckmuller, DrSc, Brno University of Technology

Visualisation of the solar corona

Abstract: Imaging the solar corona during a total solar eclipse is one of the most technically challenging tasks in astronomical photography. This is due to the extreme difference in brightness between the near and distant parts of the corona and the very low contrast of coronal structures. This lecture examines current methods for imaging the solar corona using adaptive filters.

8 April 2003

RNDr Petr Savicky CSc, Institute of Astronomy, Czech Academy of Sciences, Prague

Decision Trees and Forests for Data Analysis

Abstract: Classical statistical methods for classifying multidimensional data require that the data, at least to some extent, satisfy certain assumptions, such as a Gaussian distribution of individual classes (LDA, QDA) or their linear separability (logistic regression). If the data deviate significantly from these assumptions and cannot be transformed to satisfy any of them, non-parametric methods are used, such as decision trees, which are among the most successful methods in this category.
The lecture will focus on experimental results relating to decision trees in two respects:
We will show that replacing the commonly used heuristic of minimising error on the training set (recursive splitting) with full optimisation can lead to both an improvement and a deterioration in generalisation error, depending on the specific task. This issue relates to the fundamental principles of machine learning, as minimising the model’s error on the training set forms the basis of the vast majority of data analysis methods.

Techniques for constructing classifiers consisting of a large number of trees (classification forests) will be explained, and the results of a comparative study using simulated physical data (distinguishing between signal and noise in the newly constructed MAGIC gamma-ray telescope). The advantage of combined tree-based classifiers is evident in these data, even when compared with other types of methods.

15 April 2003

Prof. Roland Vollmar, University of Karlsruhe

Informatics for visually impaired people

Abstract: The Study Centre for Blind and Visually Impaired Students at the University of Karlsruhe has been in existence for around ten years. It was founded with the aim of enabling blind people to study Informatics (and other subjects), in accordance with the UNESCO Salamanca Statement, which states that ‘every child has a fundamental right to education and must be given the opportunity to achieve and maintain an acceptable level of learning’.
Over the past ten years, there have been many challenges, but there have also been changes regarding the technical resources available to support our students and the various teaching methods employed. In this talk, we will describe and analyse our experiences.

22 April 2003

Prof. Frantisek Plasil, CSc, Faculty of Mathematics and Physics, Charles University, Prague

Deriving ‘the whole picture’ behaviour from use cases

Abstract: Although widely used, traditional use case modelling does not provide explicit means to capture and test the behavioural compliance of the entities involved in a particular use case model. We introduce a simple formal model, called Generic UC View, which identifies key abstractions and the relations between them, thereby enabling reasoning about behavioural compliance. We analyse textual use case modelling as an instance of Generic UC View and identify the missing relations. To address this, we introduce Pro-cases as another instance of Generic UC View, based on behaviour protocols. Pro-cases feature all the required relations and enable reasoning about behavioural compliance in component composition.

29 April 2003

Prof. Ludek Smolik, Uni Seigen

Random Numbers in Cryptography and How to Generate Them

Abstract: Modern cryptographic algorithms are now tested by a wide professional audience. This is a generally accepted practice and serves to examine the performance and security of new algorithms. On the other hand, the bearers of secrets are exclusively cryptographic keys, and they must be handled with due care. One of the literally key issues in cryptography is the generation of completely random and unpredictable keys, or, more generally, random numbers. Not every method currently used for generating random numbers is suitable from the perspective of the required level of security. This lecture will present a method that utilises the unpredictable nature of quantum phenomena, such as the instant of radioactive decay. Quantum phenomena are currently the only known and accepted source of true, non-deterministic randomness and are suitable for the implementation of devices for generating cryptographic keys or bit sequences of the highest level of trust.

6 May 2003

Dr Ladislav Hluchy CSc, Director of the Institute of Informatics, Slovak Academy of Sciences, Bratislava

Virtual Organisation for Flood Forecasting

Abstract: Floods cause a great deal of material damage as well as loss of life. Floods that occur suddenly, without adequate warning, are particularly dangerous. Flood forecasting involves computationally intensive simulations of meteorological, hydrological and hydraulic problems. As part of the project ‘datA fusioN for Flood Analysis and decision Support – ANFAS, 5FP IST-1999-11676 (2000–03), addressed complex HPCN hydraulic modelling based on finite elements and volumes. The hydraulic modelling was validated on a section of the Váh river basin using DTM and DSM models obtained via LIDAR technology. Currently, the Institute of Hydrology of the Slovak Academy of Sciences is involved in the project ‘Development of a Grid Environment for Interactive Applications – CROSSGRID 5FP IST-2001-32243 (2002–05), within the framework of which it designed and implemented a cascade simulation comprising meteorological forecasting (precipitation amounts), hydrological forecasting (discharge rates) and hydraulic forecasting (water depth and velocity in the flooded area). The main objective of this project is to establish a virtual organisation linking its relevant members. In my presentation, I will outline the most important results from both projects.

13 May 2003

RNDr. Ivana Černá, CSc.

Model Checking: Approaches to the State Explosion Problem

Abstract: The need for validation to ensure the correctness of the design is a major challenge in the system development process, and nowadays the need for effective verification techniques is critical. This need has given rise to what is commonly referred to as ‘Formal Verification’. Specifically, the model checking method offers a number of advantages over traditional approaches to this problem, such as simulation, testing and deductive reasoning. Unfortunately, the model checking method also has a drawback: its performance depends on the size of the system’s state space, and the number of states to be explored can grow exponentially.
Alleviating the state explosion problem is a challenging area of research in model checking. We present an approach that utilises a classification of the properties to be verified and propose two new distributed algorithms that effectively use type information to speed up the verification process.

20 May 2003

Dr Rudolf Hanka, Cambridge University, UK

Semantic context recognition for large-scale medical image archives

Abstract: The demand for the automatic recognition and retrieval of medical images for screening, reference and management is growing faster than ever. This talk will describe an intelligent content-based image retrieval (CBIR) system that integrates both iconic and semantic content for histological image analysis. The system was jointly developed by the Medical Informatics Unit at the University of Cambridge and the Department of Computer Science at City University, Hong Kong. It combines low-level image processing technology with high-level semantic analysis of medical image content through various processing modules within the system architecture. Furthermore, as a by-product of semantic analysis, the system enables textual annotations to be generated for unknown images. As an image browser, in addition to retrieving images by example, the system also supports natural language queries.