Tato práce se zabývá problematikou popisu síťového provozu pomocí automaticky vytvořeného modelu komunikace. Hlavním zaměřením jsou komunikace v řídicích systémech , které využívají speciální protokoly, jako je například IEC 60870-5-104 . V této práci představujeme metodu charakteristiky síťového provozu z pohledu obsahu komunikace i chování v čase. Tato metoda k popisu využívá deterministické konečné automaty , prefixové stromy  a analýzu opakovatelnosti. Ve druhé části této diplomové práce se zaměřujeme na implementaci programu, který je schopný na základě takového modelu komunikace verifikovat síťový provoz v reálném čase.

Tato práce se zaměřuje na konečné automaty nad konečnými slovy a konečnými stromy, a použití těchto automatů při formální verifikaci nekonečně stavových systémů. Práce se nejdříve věnuje rozšíření existujícího přístupu pro verifikaci programů které manipulují s haldou (konkrétně programů s dynamickými datovými strukturami), jenž je založen na stromových automatech. V práci je navrženo několik rozšíření tohoto přístupu, jako například jeho plná automatizace či jeho rozšíření o podporu uspořádaných dat. V práci jsou popsány nové rozhodovací procedury pro dvě logiky, které jsou často používány ve formální verifikaci: pro separační logiku a pro slabou monadickou druhořádovou logiku s následníkem. Obě tyto rozhodovací procedury jsou založeny na převodu jejich problému do automatové domény a následné manipulaci v této cílové doméně. Posledním přínosem této práce je vývoj nových algoritmů k efektivní manipulaci se stromovými automaty, s důrazem na testování inkluze jazyků těchto automatů a manipulaci s automaty s velkými abecedami, a implementace těchto algoritmů v knihovně pro obecné použití. Tyto vyvinuté algoritmy jsou použity jako klíčová technologie, která umožňuje použití výše uvedených technik v praxi.

The main result of this thesis is the generalization of the Kleene-theorem to formal tree-series over commutative semirings (the Kleene theorem states the coincidence between rational and recognizable formal languages). To this end weighted tree-languages are introduced and the Kleene-theorem is proved for them. The desired result for formal tree-series is then obtained through application of a homomorphism that relates weighted tree-languages with formal tree-series. In the second part of the thesis the connections to the theorie of Iteration-theories are discovered. In particular it is shown there that the grove-theory of formal tree-series forms a partial iteration-theory. / Hauptresultat dieser Arbeit ist die Verallgemeinerung des Satzes von Kleene über die Koinzidenz der rationalen und der erkennbaren Sprachen auf den Fall der formalen Baumreihen über kommutativen Semiringen. Zu diesem Zweck werden gewichtete Baumsprachen eingeführt, da sich diese ählich den klassischen Baumsprachen verhalten. Der Satz von Kleene wird also zunächst auf den Fall der gewichteten Baumsprachen verallgemeinert. Das erstrebte Resultat wird dann durch Anwendung eines Homomorphismus', der gewichteten Baumsprachen formle Baumreihen zuordnet, erhalten. Im zweiten Teil der Arbeit werden Kreuzverbindungen zur Theorie der Iterationstheorien aufgezeigt. Insbesondere wird z.B. gezeigt, dass die Grovetheorie der formalen Baumreihen eine partielle Iterationstheorie bildet.

Title: Processing of Turkic Languages Author: Sibel Ciddi Department: Institute of Formal and Applied Linguistics, Faculty of Mathematics and Physics, Charles University in Prague Supervisor: RNDr. Daniel Zeman, Ph.D. Abstract: This thesis presents several methods for the morpholog- ical processing of Turkic languages, such as Turkish, which pose a specific set of challenges for natural language processing. In order to alleviate the problems with lack of large language resources, it makes the data sets used for morphological processing and expansion of lex- icons publicly available for further use by researchers. Data sparsity, caused by highly productive and agglutinative morphology in Turkish, imposes difficulties in processing of Turkish text, especially for meth- ods using purely statistical natural language processing. Therefore, we evaluated a publicly available rule-based morphological analyzer, TRmorph, based on finite state methods and technologies. In order to enhance the efficiency of this analyzer, we worked on expansion of lexicons, by employing heuristics-based methods for the extraction of named entities and multi-word expressions. Furthermore, as a prepro- cessing step, we introduced a dictionary-based recognition method for tokenization of multi-word expressions. This method complements...

Eine der stärksten Erweiterungen der klassischen Theorie formaler Sprachen und Automaten ist die Einbeziehung von Gewichten oder Vielfachheiten aus einem Halbring. Diese Dissertation untersucht gewichtete Automaten über Strukturen mit Nebenläufigkeit. Wir erweitern die Arbeit von Lodaya und Weil und erhalten so ein Modell gewichteter verzweigender Automaten, in dem die Berechnung des Gewichts einer parallelen Komposition anders als die einer sequentiellen Komposition gehandhabt wird. Die von Lodaya und Weil eingeführten Automaten modellieren Nebenläufigkeit durch Verzweigen. Ein verzweigender Automat ist ein endlicher Automat mit drei verschiedenen Typen von Transitionen. Sequentielle Transitionen überführen durch Ausführen eines Ereignisses einen Zustand in einen anderen. Dagegen sind Gabel- und Binde-Transitionen für das Verzweigen verantwortlich. Läufe dieser Automaten werden beschrieben durch sequentiell-parallele posets, kurz sp-posets. Alle Transitionen des Automaten werden in unserem Modell mit Gewichten versehen. Neben dem Nichtdeterminismus und der sequentiellen Komposition wollen wir nun auch die parallele Komposition quantitativ behandeln. Dafür benötigen wir eine Gewichtsstruktur mit einer Addition, einer sequentiellen und einer parallelen Multiplikation. Solch eine Struktur, genannt Bihalbring, besteht damit de facto aus zwei Halbringen mit derselben additiven Struktur. Weiterhin muss die parallele Multiplikation kommutativ sein. Das Verhalten eines gewichteten verzweigenden Automaten ist dann eine Funktion, die jeder sp-poset ein Element eines Bihalbrings zuordnet. Das Hauptresultat charakterisiert das Verhalten dieser Automaten im Sinne von Kleenes und Schützenbergers Sätzen über das Zusammenfallen der Klassen der erkennbaren und der rationalen Sprachen bzw. formalen Potenzreihen. Darüber hinaus untersuchen wir den Abschluss dieser Verhalten unter allen rationalen Operationen und unter dem Hadamard-Produkt. Letztlich diskutieren wir Zusammenhänge zwischen Reihen und Sprachen im Rahmen verzweigender Automaten. / One of the most powerful extensions of classical formal language and automata theory is the consideration of weights or multiplicities from a semiring. This thesis investigates weighted automata over structures incorporating concurrency. Extending work by Lodaya and Weil, we propose a model of weighted branching automata in which the calculation of the weight of a parallel composition is handled differently from the calculation of the weight of a sequential composition. The automata as proposed by Lodaya and Weil model concurrency by branching. A branching automaton is a finite-state device with three different types of transitions. Sequential transitions transform a state into another one by executing an action. In contrast, fork and join transitions are responsible for branching. Executions of such systems can be described by sequential-parallel posets, or sp-posets for short. In the model considered here all kinds of transitions are equipped with weights. Beside non-determinism and sequential composition we would like to deal with the parallel composition in a quantitative way. Therefore, we are in need of a weight structure equipped with addition, a sequential, and, moreover, a parallel multiplication. Such a structure, called a bisemiring, is actually composed of two semirings with the same additive structure. Moreover, the parallel multiplication has to be commutative. Now, the behavior of a weighted branching automaton is a function that associates with every sp-poset an element from the bisemiring. The main result characterizes the behavior of these automata in the spirit of Kleene's and Schützenberger's theorems about the coincidence of recognizable and rational languages, and formal power series, respectively. Moreover, we investigate the closure of behaviors under all rational operations and under Hadamard-product. Finally, we discuss connections between series and languages within our setting.

Cancer cells display characteristic traits acquired in a step-wise manner during carcinogenesis. Some of these traits are autonomous growth, induction of angiogenesis, invasion and metastasis. In this thesis, the focus is on one of the latest stages of tumor progression, tumor invasion. Tumor invasion emerges from the combined effect of tumor cell-cell and cell-microenvironment interactions, which can be studied with the help of mathematical analysis. Cellular automata (CA) can be viewed as simple models of self-organizing complex systems in which collective behavior can emerge out of an ensemble of many interacting "simple" components. In particular, we focus on an important class of CA, the so-called lattice-gas cellular automata (LGCA). In contrast to traditional CA, LGCA provide a straightforward and intuitive implementation of particle transport and interactions. Additionally, the structure of LGCA facilitates the mathematical analysis of their behavior. Here, the principal tools of mathematical analysis of LGCA are the mean-field approximation and the corresponding Lattice Boltzmann equation. The main objective of this thesis is to investigate important aspects of tumor invasion, under the microscope of mathematical modeling and analysis: Impact of the tumor environment: We introduce a LGCA as a microscopic model of tumor cell migration together with a mathematical description of different tumor environments. We study the impact of the various tumor environments (such as extracellular matrix) on tumor cell migration by estimating the tumor cell dispersion speed for a given environment. Effect of tumor cell proliferation and migration: We study the effect of tumor cell proliferation and migration on the tumor’s invasive behavior by developing a simplified LGCA model of tumor growth. In particular, we derive the corresponding macroscopic dynamics and we calculate the tumor’s invasion speed in terms of tumor cell proliferation and migration rates. Moreover, we calculate the width of the invasive zone, where the majority of mitotic activity is concentrated, and it is found to be proportional to the invasion speed. Mechanisms of tumor invasion emergence: We investigate the mechanisms for the emergence of tumor invasion in the course of cancer progression. We conclude that the response of a microscopic intracellular mechanism (migration/proliferation dichotomy) to oxygen shortage, i.e. hypoxia, maybe responsible for the transition from a benign (proliferative) to a malignant (invasive) tumor. Computing in vivo tumor invasion: Finally, we propose an evolutionary algorithm that estimates the parameters of a tumor growth LGCA model based on time-series of patient medical data (in particular Magnetic Resonance and Diffusion Tensor Imaging data). These parameters may allow to reproduce clinically relevant tumor growth scenarios for a specific patient, providing a prediction of the tumor growth at a later time stage. / Krebszellen zeigen charakteristische Merkmale, die sie in einem schrittweisen Vorgang während der Karzinogenese erworben haben. Einige dieser Merkmale sind autonomes Wachstum, die Induktion von Angiogenese, Invasion und Metastasis. Der Schwerpunkt dieser Arbeit liegt auf der Tumorinvasion, einer der letzten Phasen der Tumorprogression. Die Tumorinvasion ensteht aus der kombinierten Wirkung von den Wechselwirkungen Tumorzelle-Zelle und Zelle-Mikroumgebung, die mit die Hilfe von mathematischer Analyse untersucht werden können. Zelluläre Automaten (CA) können als einfache Modelle von selbst-organisierenden komplexen Systemen betrachtet werden, in denen kollektives Verhalten aus einer Kombination von vielen interagierenden "einfachen" Komponenten entstehen kann. Insbesondere konzentrieren wir uns auf eine wichtige CA-Klasse, die sogenannten Zelluläre Gitter-Gas Automaten (LGCA). Im Gegensatz zu traditionellen CA bieten LGCA eine einfache und intuitive Umsetzung der Teilchen und Wechselwirkungen. Zusätzlich erleichtert die Struktur der LGCA die mathematische Analyse ihres Verhaltens. Die wichtigsten Werkzeuge der mathematischen Analyse der LGCA sind hier die Mean-field Approximation und die entsprechende Lattice - Boltzmann - Gleichung. Das wichtigste Ziel dieser Arbeit ist es, wichtige Aspekte der Tumorinvasion unter dem Mikroskop der mathematischen Modellierung und Analyse zu erforschen: Auswirkungen der Tumorumgebung: Wir stellen einen LGCA als mikroskopisches Modell der Tumorzellen-Migration in Verbindung mit einer mathematischen Beschreibung der verschiedenen Tumorumgebungen vor. Wir untersuchen die Auswirkungen der verschiedenen Tumorumgebungen (z. B. extrazellulären Matrix) auf die Migration von Tumorzellen dürch Schätzung der Tumorzellen-Dispersionsgeschwindigkeit in einem gegebenen Umfeld. Wirkung von Tumor-Zellenproliferation und Migration: Wir untersuchen die Wirkung von Tumorzellenproliferation und Migration auf das invasive Verhalten der Tumorzellen durch die Entwicklung eines vereinfachten LGCA Tumorwachstumsmodells. Wir leiten die entsprechende makroskopische Dynamik und berechnen die Tumorinvasionsgeschwindigkeit im Hinblick auf die Tumorzellenproliferation- und Migrationswerte. Darüber hinaus berechnen wir die Breite der invasiven Zone, wo die Mehrheit der mitotischer Aktivität konzentriert ist, und es wird festgestellt, dass diese proportional zu den Invasionsgeschwindigkeit ist. Mechanismen der Tumorinvasion Entstehung: Wir untersuchen Mechanismen, die für die Entstehung von Tumorinvasion im Verlauf des Krebs zuständig sind. Wir kommen zu dem Schluss, dass die Reaktion eines mikroskopischen intrazellulären Mechanismus (Migration/Proliferation Dichotomie) zu Sauerstoffmangel, d.h. Hypoxie, möglicheweise für den Übergang von einem gutartigen (proliferative) zu einer bösartigen (invasive) Tumor verantwortlich ist. Berechnung der in-vivo Tumorinvasion: Schließlich schlagen wir einen evolutionären Algorithmus vor, der die Parameter eines LGCA Modells von Tumorwachstum auf der Grundlage von medizinischen Daten des Patienten für mehrere Zeitpunkte (insbesondere die Magnet-Resonanz-und Diffusion Tensor Imaging Daten) ermöglicht. Diese Parameter erlauben Szenarien für einen klinisch relevanten Tumorwachstum für einen bestimmten Patienten zu reproduzieren, die eine Vorhersage des Tumorwachstums zu einem späteren Zeitpunkt möglich machen.

In this Doktorarbeit the Lattice Boltzmann scheme, a heuristic method for the simulation of flows in complicated boundaries, is investigated. Its theory is renewed by emphasizing the entropy maximization principle, and new means for the modelling of geometries (including moving boundaries) and the visual representation of evoluting flows are presented. An object oriented implemen- tation is given with communication between objects realized by an interpreter object and communication from outside realized via interprocess communica- tion. Within the new theoretical apprach the applicability of existing Lattice Boltzmann schemes to model thermal flows for arbitrary temperatures is reex- amined. / In dieser Doktorarbeit wird das Gitter-Boltzmann-Schema, eine heuristische Methode fuer die Simulation von Stroemungen innerhalb komplexer Raender, untersucht. Die zugrundeliegende Theorie wird unter neuen Gesichtspunkten, insbesondere dem Prinzip der Entropiemaximierung, betrachtet. Des weiteren werden neuartige Methoden fuer die Modellierung der Geometrie (einschl. beweglicher Raender) und der visuellen Darstellung aufgezeigt. Eine objektorientierte Implementierung wird vorgestellt, wobei die Kommunikation zwischen den Objekten über Interpreter-Objekte und die Kommunikation mit der Aussenwelt ueber Interprozess-Kommunikation gehandhabt wird. Mit dem neuen theoretischen Ansatz wird die Gueltigkeit bestehender Gitter-Boltzmann-Schemata fuer die Anwendung auf Stroemungen mit nicht konstanter Temperatur untersucht.

We study cellular automata as discrete dynamical systems and in particular investigate under which conditions two cellular automata are topologically conjugate. Based on work of McKinsey, Tarski, Pierce and Head we introduce derivative algebras to study the topological structure of sofic shifts in dimension one. This allows us to classify periodic cellular automata on sofic shifts up to topological conjugacy based on the structure of their periodic points. We also get new conjugacy invariants in the general case. Based on a construction by Hanf and Halmos, we construct a pair of non-homeomorphic subshifts whose disjoint sums with themselves are homeomorphic. From this we can construct two cellular automata on homeomorphic state spaces for which all points have minimal period two, which are, however, not topologically conjugate. We apply our methods to classify the 256 elementary cellular automata with radius one over the binary alphabet up to topological conjugacy. By means of linear algebra over the field with two elements and identities between Fibonacci-polynomials we show that every conjugacy between rule 90 and rule 150 cannot have only a finite number of local rules. Finally, we look at the sequences of finite dynamical systems obtained by restricting cellular automata to spatially periodic points. If these sequences are termwise conjugate, we call the cellular automata conjugate on all tori. We then study the invariants under this notion of isomorphism. By means of an appropriately defined entropy, we can show that surjectivity is such an invariant.

Eine der stärksten Erweiterungen der klassischen Theorie formaler Sprachen und Automaten ist die Einbeziehung von Gewichten oder Vielfachheiten aus einem Halbring. Diese Dissertation untersucht gewichtete Automaten über Strukturen mit Nebenläufigkeit. Wir erweitern die Arbeit von Lodaya und Weil und erhalten so ein Modell gewichteter verzweigender Automaten, in dem die Berechnung des Gewichts einer parallelen Komposition anders als die einer sequentiellen Komposition gehandhabt wird. Die von Lodaya und Weil eingeführten Automaten modellieren Nebenläufigkeit durch Verzweigen. Ein verzweigender Automat ist ein endlicher Automat mit drei verschiedenen Typen von Transitionen. Sequentielle Transitionen überführen durch Ausführen eines Ereignisses einen Zustand in einen anderen. Dagegen sind Gabel- und Binde-Transitionen für das Verzweigen verantwortlich. Läufe dieser Automaten werden beschrieben durch sequentiell-parallele posets, kurz sp-posets. Alle Transitionen des Automaten werden in unserem Modell mit Gewichten versehen. Neben dem Nichtdeterminismus und der sequentiellen Komposition wollen wir nun auch die parallele Komposition quantitativ behandeln. Dafür benötigen wir eine Gewichtsstruktur mit einer Addition, einer sequentiellen und einer parallelen Multiplikation. Solch eine Struktur, genannt Bihalbring, besteht damit de facto aus zwei Halbringen mit derselben additiven Struktur. Weiterhin muss die parallele Multiplikation kommutativ sein. Das Verhalten eines gewichteten verzweigenden Automaten ist dann eine Funktion, die jeder sp-poset ein Element eines Bihalbrings zuordnet. Das Hauptresultat charakterisiert das Verhalten dieser Automaten im Sinne von Kleenes und Schützenbergers Sätzen über das Zusammenfallen der Klassen der erkennbaren und der rationalen Sprachen bzw. formalen Potenzreihen. Darüber hinaus untersuchen wir den Abschluss dieser Verhalten unter allen rationalen Operationen und unter dem Hadamard-Produkt. Letztlich diskutieren wir Zusammenhänge zwischen Reihen und Sprachen im Rahmen verzweigender Automaten. / One of the most powerful extensions of classical formal language and automata theory is the consideration of weights or multiplicities from a semiring. This thesis investigates weighted automata over structures incorporating concurrency. Extending work by Lodaya and Weil, we propose a model of weighted branching automata in which the calculation of the weight of a parallel composition is handled differently from the calculation of the weight of a sequential composition. The automata as proposed by Lodaya and Weil model concurrency by branching. A branching automaton is a finite-state device with three different types of transitions. Sequential transitions transform a state into another one by executing an action. In contrast, fork and join transitions are responsible for branching. Executions of such systems can be described by sequential-parallel posets, or sp-posets for short. In the model considered here all kinds of transitions are equipped with weights. Beside non-determinism and sequential composition we would like to deal with the parallel composition in a quantitative way. Therefore, we are in need of a weight structure equipped with addition, a sequential, and, moreover, a parallel multiplication. Such a structure, called a bisemiring, is actually composed of two semirings with the same additive structure. Moreover, the parallel multiplication has to be commutative. Now, the behavior of a weighted branching automaton is a function that associates with every sp-poset an element from the bisemiring. The main result characterizes the behavior of these automata in the spirit of Kleene's and Schützenberger's theorems about the coincidence of recognizable and rational languages, and formal power series, respectively. Moreover, we investigate the closure of behaviors under all rational operations and under Hadamard-product. Finally, we discuss connections between series and languages within our setting.

This master thesis deals with design of automation control system for operationally experimental malt-house. The first part deals with general description of all production stages of malting and brief description about the Research Institute of Brewering and Malting. It also generally characterizes the used hardware and software for automation control system. The second part of this thesis describes the types of programmable logic controllers and the selection of optimal variant for application of the operationally experimental malt-house. Master thesis in the third and fourth part contains a brief description about the methodology and the creation of control program and visualisation for automatic control system of the operationally experimental malt-house. The output of the master thesis is a complete control program and visualisation of the controlled application of the operating malt-house.