Program kolokvií s abstrakty pro semestr Jaro 2001

6. 3. 2001: Doc. Lubos Brim, CSc, FI MU Brno; Automated formal verification; Abstract: Formal verification is an important technique to validating of the correct behaviour of computer systems. One of the most significant recent developments in the area of formal verification is the discovery of algorithmic methods for verifying temporal-logic properties of finite-state models of systems. These automated methods are known as model-checking. Model-checking tools are now routinely used in industrial applications.
In the talk an overview of concepts, algorithms and tools for model-checking will be presented. Some prospective research directions will be discussed.
13. 3. 2001: Prof. Pavel Misha, Oregon University, USA; Fusion-based robust signal processing by humans and machines; Abstract: In my presentation, I will briefly note the wide range of benefits that can be derived from biological and machine data fusion, but I will then focus on fusion in service of pattern recognition. Although many existing automatic pattern recognition systems have achieved considerable success over the past fifty years, most of them lack robustness - the ability to perform as well as possible in unpredictable and changing environments. In contrast, biological system seem to be much more resilient to the environmental changes that are, at least partially, irrelevant to the tasks. The fact that current artificial systems lack the robustness found in natural systems leads to questions that address the basic differences between the natural and the statistically optimal approaches. Our preliminary analysis of these differences led us to hypothesize new methodology for pattern recognition. I will briefly describe a working hypothesis whereby data fusion in conjunction with neural-like computation can be used to achieve more robust pattern recognition performance that that obtained with more traditional approaches. I will illustrate the approach on one or two specific and realistic examples.
20. 3. 2001: Doc. Martin Sperka, FIE Bratislava; Umele umenie: moze stroj vytvorit umelecke dielo?; Abstract: UMELÉ UMENIE Môľe stroj vytvori» umelecké dielo ? Katedra informatiky a výpočtovej techniky, FEI STU Bratislava V prvej casti strucne rekapitulujem vyvoj nazorov na pouzivanie pocitacov a prvé experimenty v umení v ąes»desiatich a sedemdesiatich rokoch, pragmatický prístup k ich pouľívaniu v súčasnosti (ako nástroja v dizajne, architektúre, animovanom filme, video arte a počítačovom sochárstve), a trendy v elektronickom voµnom umení (počítač ako nové médium, interaktívne virtuálne a reálne inątalácie, body art, e-mail art, internet art, cyber art ).
V druhej časti sa budem venova» niektorými úvahám a názorom o moľnostiach simulácie umeleckého procesu (umelé umenie ako paralela k umelému ľivotu a umelej inteligencii) v súvislosti s vývojom vedy a techniky počítačov a kognitívnych vied. Budem analyzova» vývoj vzniku umeleckého artefaktu ako evolučného, učiaceho sa a sociálneho procesu ako aj prezentova» a polemizova» s reakciami a názormi umelcov na túto tému z panelových diskusií v rámci konferencií o elektronickom umení.
27. 3. 2001: Prof. Miroslav Novotny DrSc; Homomorphisms -- why and how?; Abstract: Construction of all homomorphisms of an algebraic structure into a similar algebraic structure may play an important role in many problems: embedding, morphisms in categories, cardinal operations of ordered sets, functional equations. Construction of all homomorphisms can be reduced to the construction of all homomorphisms of a mono-unary algebra into an algebra of the same type. A mono-unary algebra is a set A with a unary operation, i.e. with a mapping of A into itself. The talk includes a construction of all homomorphisms of a mono-unary algebra into another algebra of the same type.
Let (A,o), (A',o') be groupoids, i.e. structures with a binary operation. If we put un[o](x,y) = (y,o(x,y)) for any x, y in A, we obtain a mono-unary algebra (AxA,un[o]). The so called decomposable homomorphisms of (AxA,un[o]) into (A'xA',un[o']) correspond to all homomorphisms of (A,o) into (A',o'). This idea can be extended to the construction of homomorphisms of algebras. Similarly, a binary relation r on a set A can be lifted to the power set of A which creates a unary operation. Homomorphisms with particular properties between the corresponding mono-unary algebras correspond to all strong homomorphisms between relational structures. This idea can be extended to the construction of all homomorphisms between relational structures.
These methods lead us to constructions of homomorphisms of hyperstructures, graphs, and heterogeneous algebras. Some of these constructions appear in Computer Science.
3. 4. 2001: Dr. Hans Hagen, GH Hesselt, The Netherlands; MATHML; Abstract: Posting a document that contains math on the web is not trivial, especially because math has a special kind of markup and uses characters not commonly available. MathML is supposed to fill this gap in web publishing. By coding math in MathML one opens the road to reuse of formulas in multiple applications, like math simulators, problem solving programs and typesetting engines.
For two decades, TeX has dominated the math typesetting world, and TeX is also a good candate for typesetting math coded in MathML. In this presentation the following topics will be covered:
- to what extent can MathML cover our needs
- what are the strong and weak points of MathML
- how easy and/or difficult is it to implement a MathML backend
- how to combine flexibility and consistency in MathML
10. 4. 2001: Doc. Ivan Kopecek, CSc, FI, MU, Brno; Abstraction and complexity (Finite state analysis of speech communication); Abstract: Motto: "The introduction of suitable abstractions is our only mental aid to organize and master complexity." - E. W. Dijkstra
Understanding and mastering human-computer conversation in natural language is one of the most complex, provoking, challenging and exciting problem we face in artificial intelligence. In this talk we present an approach that is trying to apply generality and abstractions of universal algebra to analyzing and mastering complexity of natural language communication. The formal theory based on algebraical finite state analysis will be illustrated on variety of problems, like creating dialogue strategies, modeling emotions and personality, playing hazard games, cloning user models, law problems, supporting speech synthesis and recognition etc.
17. 4. 2001: Prof. Frantisek Plasil CSc, MFF UK, Praha; Component behaviour protocols and connections; Abstract: An overview of the SOFA project (Software Appliances) will be provided with an emphasis on its component model. Attention will be paid to the behavior description of components in SOFA. Based on a notation similar to regular expressions, this description is done via behavior protocols which are used on three levels: interface, frame, and architecture. A protocol conformance relation is defined. Using this relation, the designer can in most cases statically verify that the frame protocol adheres to requirements of the interface protocols, and that the architecture protocol adheres to the requirements of the frame and interface protocols. Underscoring the important differences in the component and connector lifecycles, the principles of the SOFA connector model will be explained.
24. 4. 2001: Doc.Jiri Wiedermann, DRSc. Ustav Informatiky, CAV, Praha; Turingov stroj ve svetle soucasnych vypoctu; Abstract: Klasicka Church-Turingova teze nas ujistuje, ze kazdy algoritmus lze popsat pomoci standardniho Turingova stroje. Nicmene, pro vypocty soucasnych osobnich pocitacu anebo velkych distribuovanych systemu sa toto paradigma nehodi. Vypocty podobnych systemu se lisi od klasickych ve trech smerech: nikdy nekonci, prubezne a nepredvidatelne interaguji se svym okolim a vypocetni system se dynamicky a neprevidatelne vyviji. V prendasce navrhneme rozsireni shora uvede teze tak, aby pokryvala i prave zminene tzv. neuniformni interaktivni vypocty. Rozsirena teze tvrdi, ze kazdy vypocet uvedeneho druhu lze zachytit pomoci interaktivniho Turingova stroja se specialnim typem orakula, ktere nezavisi na danem vstupu, ale pouze na jeho delce. Priklady, ktere rozirena teze pokryva, sahaji od (formalnich) modelu osobnich pocitacu pres internet az po komunity inteligentich mobilnich agentu podlehajici neuniformni evoluci. Dokazeme, ze vysledne vypocetni systemy maji superturingovskou vypocetni silu.
Prednaska vychazi ze spolecne praci autora s J. van Leeuwenem: Turing Machine Paradigm in Contemporary Computing, In: Mathematics Unlimited - 2001 and Beyond, Springer Verlag, 2001, kterou je mozne ziskat ve forme vyzkumne zpravy take z webu via ftp://ftp.cs.uu.nl/pub/RUU/CS/techreps/CS- 2000/2000-33.pdf
15. 5. 2001: Dr. Jan Sefranek, Ustav informatiky, MFF UK, Bratislava; Logika a umela inteligencia; Abstract: Vypoctove modely kognitivnych schopnosti, zalozene na logickej formalizacii, predstavuju jeden z najstarsich pristupov k umelej inteligencii. V pociatkoch tejto discipliny prevladala predstava, ze klasicka logika je postacujuci nastroj (pre odvodzovanie i pre reprezentaciu poznatkov).
Velmi skoro sa vsak ukazalo, ze tento ramec treba prekrocit - je potrebne vytvorit hutnejsiu reprezentaciu poznatkov a odvodzovat aj ne-deduktivne.
Po historickom uvode bude prednaska venovana prave ne-deduktivnemu (hypotetickemu) usudzovaniu. Tento druh usudzovania je predmetom intenzivnej vyskumnej pozornost asi dve desatrocia. Najcastejsie sa na jeho oznacenie pouziva termin nemonotonne usudzovanie. Nemonotonnost je vsak skor symptomom nez esenciou tohoto druhu usudzovania.
Jednou z ciest k pochopeniu nemonotonnosti je adekvatna semantika. Prednaska predstavi povodnu semanticku charakterizaciu nemonotonneho (hypotetickeho) usudzovania pomocou dynamickych Kripkeho struktur.
22. 5. 2001: Dr. Wolfgang Slany, Technische Universitaet, Wien; Shift scheduling problems; Abstract: Generating high-quality schedules for a rotating workforce is a critical task in all situations where a certain staffing level must be guaranteed, such as in industrial plants, hospitals, or airline companies. Results from ergonomics indicate that shift schedules have a profound impact on the health and satisfaction of employees as well as on their performance at work. Moreover, shift schedules must satisfy legal requirements and should also meet the objectives of the employing organization. Shift scheduling comprises several sub-problems such as the allocation of workers to shifts or the design of the shifts themselves that present interesting challenges both from practical (our algorithms are sold in successful commercial packages) as well as theoretical (hardness, approximability) viewpoints. We describe some of our results in both areas. In particular, we studied in depth the (non-)approximability of the shift design problem, a network flow variant that has many applications beyond shift scheduling.
29. 5. 2001: Prof. Kenichi Morita, Hiroshima university; Reversible computing
31. 5. 2001: Kostis Sagonas; HiPE: A High Performance Erlang System; Abstract: Erlang is a concurrent functional programming language designed to ease the development of large-scale distributed soft real-time control applications. It has so far been quite successful in this application domain, despite the fact that its currently available implementations are emulators of virtual machines.
This talk will briefly present the architecture and performance characteristics of HiPE, an open-source native code compiler for Erlang. HiPE is a complete implementation of Erlang, offers flexible integration between emulated and native code, and efficiently supports features crucial for Erlang's application domain such as concurrency. As our performance evaluations show, HiPE is currently the fastest among all Erlang implementations.
More details at http://www.csd.uu.se/projects/hipe