No description available.

Inom linja ̈r algebra har varje vektorrum ett s ̊a kallat dualrum, vilket är ett vektorrum bestående av alla linjära funktioner från det ursprungliga rummet till sin kropp. Att beräkna dimensionen av ett dualrum tillhörande ett ändlig-dimensionellt vektorrum är relativt enkelt, för oändlig-dimensionella vektorrum är det mer komplicerat. Den sats vi ska diskutera, Erdős–Kaplansky Satsen, ämnar lösa den frågan med påståendet att ett dualrum tillhörande ett oändlig-dimensionellt vektorrum har dimension lika med sin kardinalitet.

Society relies on increasingly complex software and hardware systems, hence techniques capable of proving that they behave as expected are of great and growing interest. Formal verification procedures employ mathematically sound reasoning to address this need. This thesis proposes novel techniques for the verification and falsification of expressive specifications on timed and infinite-state systems. An expressive specification language allows the description of the intended behaviour of a system via compact formal statements written at an abstraction level that eases the review process. Falsifying a specification corresponds to identifying an execution of the system that violates the property (i.e. a witness). The capability of identifying witnesses is a key feature in the iterative refinement of the design of a system, since it provides a description of how a certain error can occur. The designer can analyse the witness and take correcting actions by refining either the description of the system or its specification. The contribution of this thesis is twofold. First, we propose a semantics for Metric Temporal Logic that considers four different models of time (discrete, dense, super-discrete and super-dense). We reduce its verification problem to finding an infinite fair execution (witness) for an infinite-state system with discrete time. Second, we define a novel SMT-based algorithm to identify such witnesses. The algorithm employs a general representation of such executions that is both informative to the designer and provides sufficient structure to automate the search of a witness. We apply the proposed techniques to benchmarks taken from software, infinite-state, timed and hybrid systems. The experimental results highlight that the proposed approaches compete and often outperform specific (application tailored) techniques currently used in the state of the art.

No description available.

No description available.

I den här uppsatsen presenteras ett nytt sätt att procedurellt generera pseudo-oändligadungeons som kan traverseras i tre dimensioner. För att hålla genereringen koherent bådeunder och mellan spelsessioner utgår genereringen från ett ”seed”. Ett seed garanterar sammainnehåll på samma plats varje gång miljön genereras. Med en metod som är baserad iL-system genererar vi här en maze dungeon med tvådimensionell grammatikexpansion ochvi undersöker sedan hur duglig den är. Vi försöker få svaret på hur avancerade L-system somkrävs för att nå en nivå av variation som känns tillräcklig för en miljö av pseudo-oändligkaraktär. Variationstestet samlar data från ett urval områden i den färdiggenererade dungeonen.Resultaten visar på att den utvecklade metoden i det här projektet fungerar väl förändamålet. / In this paper we present a novel way of procedurally generating pseudo infinite dungeonsthat can be traversed in three dimensions. To ensure consistent generation both duringand between playing sessions the generation is ”seeded”. Seeded generation guarantees thesame content in the same place every time the environment is generated. Using a methodbased in L-systems we generate a maze dungeon with two dimensional grammar expansionand explore its viability. We try to find the needed complexity of the L-system to achievea level of variation that feels adequate for an environment of pseudo infinite character.The variation tests collect data from sample areas in the generated dungeons. The resultsindicate that the method used in this project works well for the intended purpose.

In this dissertation, we focus on two research topics related to mixture models. The first topic is Adaptive Rejection Metropolis Simulated Annealing for Detecting Global Maximum Regions, and the second topic is Bayesian Model Selection for Nonlinear Mixed Effects Model. In the first topic, we consider a finite mixture model, which is used to fit the data from heterogeneous populations for many applications. An Expectation Maximization (EM) algorithm and Markov Chain Monte Carlo (MCMC) are two popular methods to estimate parameters in a finite mixture model. However, both of the methods may converge to local maximum regions rather than the global maximum when multiple local maxima exist. In this dissertation, we propose a new approach, Adaptive Rejection Metropolis Simulated Annealing (ARMS annealing), to improve the EM algorithm and MCMC methods. Combining simulated annealing (SA) and adaptive rejection metropolis sampling (ARMS), ARMS annealing generate a set of proper starting points which help to reach all possible modes. ARMS uses a piecewise linear envelope function for a proposal distribution. Under the SA framework, we start with a set of proposal distributions, which are constructed by ARMS, and this method finds a set of proper starting points, which help to detect separate modes. We refer to this approach as ARMS annealing. By combining together ARMS annealing with the EM algorithm and with the Bayesian approach, respectively, we have proposed two approaches: an EM ARMS annealing algorithm and a Bayesian ARMS annealing approach. EM ARMS annealing implement the EM algorithm by using a set of starting points proposed by ARMS annealing. ARMS annealing also helps MCMC approaches determine starting points. Both approaches capture the global maximum region and estimate the parameters accurately. An illustrative example uses a survey data on the number of charitable donations. The second topic is related to the nonlinear mixed effects model (NLME). Typically a parametric NLME model requires strong assumptions which make the model less flexible and often are not satisfied in real applications. To allow the NLME model to have more flexible assumptions, we present three semiparametric Bayesian NLME models, constructed with Dirichlet process (DP) priors. Dirichlet process models often refer to an infinite mixture model. We propose a unified approach, the penalized posterior Bayes factor, for the purpose of model comparison. Using simulation studies, we compare the performance of two of the three semiparametric hierarchical Bayesian approaches with that of the parametric Bayesian approach. Simulation results suggest that our penalized posterior Bayes factor is a robust method for comparing hierarchical parametric and semiparametric models. An application to gastric emptying studies is used to demonstrate the advantage of our estimation and evaluation approaches. / Ph. D.

In dieser Arbeit wird eine detaillierte Analysis des konsistenten kinetischen Modells zum Kornwachstum von Fradkov durchgeführt. Dieses Modell beschreibt - basierend auf dem von Neumann--Mullins Gesetz - die Flächenänderung eines Korns abhängig von seiner Topologieklasse, d.h. der Anzahl der Kanten. Topologieänderungen werden durch Kopplungsterme zwischen den Gleichungen für die Anzahldichten der verschiedenen Topologieklassen beschrieben. Daraus resultiert ein unendlich-dimensionales System von Transportgleichungen mit tridiagonaler Kopplungsstruktur. Durch eine spezielle Wahl des Kopplungsgewichts, welche die Gleichungen nichtlinear und räumlich nichtlokal macht, wird das Modell konsistent. Nach einer Einführung wird das Modell von Fradkov im zweiten Kapitel hergeleitet; formale Rechnungen zeigen die Konsistenz des Modells auf. Im dritten Kapitel wird das Kopplungsgewicht a priori beschränkt. Dadurch kann im ersten Teil des vierten Kapitels Existenz und Eindeutigkeit von Lösungen für endlich-dimensionale Systeme gezeigt werden. Weitere Schranken an die Anzahldichten im fünften Kapitel ermöglichen den Grenzübergang hinsichtlich der Anzahl der Gleichungen im zweiten Teil des vierten Kapitels. Die Existenz von Lösungen des unendlich-dimensionalen Systems wird somit über eine geeignete Approximation gezeigt. Energiemethoden liefern Eindeutigkeit und stetige Abhängigkeit von den Daten. Im sechsten Kapitel wird das Langzeitverhalten untersucht. Besonderes Augenmerk liegt dabei auf stationären Lösungen eines reskalierten Systems als Kandidaten für selbstähnliche Lösungen. Abschließend wird das Lewis''sche Gesetz asymptotisch verifiziert. / The subject matter of this thesis is a detailed analysis of the self--consistent kinetic model for grain growth introduced by Fradkov. The model is based on the von Neumann--Mullins law describing the change of area of grains according to their topological class, i.e. the number of edges they have. Topological events are performed by coupling terms between equations for the number densities of different topological classes. The resulting system of transport equations is infinite-dimensional with a tridiagonal coupling structure. Self-consistency of this kinetic model is achieved by introducing a coupling''s weight making the equations nonlinear and nonlocal in space. We start with an introduction in the first chapter. Afterwards in the second chapter we derive Fradkov''s model and carry out formal calculations to illustrate self-consistency. In the third chapter we present a priori calculations mainly allowing us to bound the nonlinearity. This enables us to prove existence and uniqueness of solutions to finite-dimensional systems in the first part of the fourth chapter. Further bounds on the number densities established in the fifth chapter allow for passing to the limit concerning the number of equations in the second part of the fourth chapter. Therefore we prove existence of solutions to the infinite-dimensional system by a suitable approximation procedure. Uniqueness and continuous dependence on the data is then provided by energy methods. The sixth chapter focusses on long-time behaviour and mainly on stationary solutions of a rescaled system as candidates for self-similar solutions. Finally we prove Lewis'' law asymptotically.

Datalog ist die relationale Variante der logischen Programmierung und ist eine Standard-Abfragesprache in der Datenbankentheorie geworden. Die Programmkomplexität von Datalog im bisherigen Hauptanwendungsgebiet, auf endlichen Strukturen, ist bekanntermassen in EXPTIME. Wir untersuchen die Komplexität von Datalog auf unendlichen Strukturen, motiviert durch mögliche Anwendungen von Datalog auf unendlichen Strukturen (z.B. linearen Ordnungen) im zeitlichen und räumlichen Schliessen, aber auch durch das aufkommende Interesse an unendlichen Strukturen bei verwandten theoretischen Problemen, wie Constraint Satisfaction Problems (CSP): Im Gegensatz zu endlichen Strukturen können Datalog-Berechnungen auf unendlichen Strukturen unendlich lange dauern, was zur Unentscheidbarkeit von Datalog auf unendlichen Strukturen führen kann. Aber auch in den entscheidbaren Fällen kann die Komplexität von Datalog auf unendlichen Strukturen beliebig hoch sein. Im Hinblick auf dieses Ergebnis widmen wir uns dann unendlichen Strukturen mit der niedrigsten Komplexität von Datalog: Wir zeigen, dass Datalog auf linearen Ordnungen (auch dichte und diskrete, mit oder ohne Konstanten und sogar gefärbte) und Baumordnungen EXPTIME-vollständig ist. Für die Bestimmung der oberen Schranke werden Werkzeuge für Datalog auf Ordnungen eingeführt: Ordnungstypen, Abstandstypen und typdisjunkte Programme. Die Typkonzepte liefern eine endliche Beschreibung der unendlichen Programmergebnisse und könnten auch für praktische Anwendungen von Interesse sein. Wir erzeugen spezielle typdisjunkte Programme, die sich ohne Rekursion lösen lassen. Ein Transfer unserer Methoden auf CSPs zeigt, dass CSPs auf unendlichen Strukturen mit beliebig hoher Zeitkomplexität vorkommen, wie Datalog. / Datalog is the relational variant of logic programming and has become a standard query language in database theory. The (program) complexity of datalog in its main context so far, on finite databases, is well known to be in EXPTIME. We research the complexity of datalog on infinite databases, motivated by possible applications of datalog to infinite structures (e.g. linear orders) in temporal and spatial reasoning on one hand and the upcoming interest in infinite structures in problems related to datalog, like constraint satisfaction problems: Unlike datalog on finite databases, on infinite structures the computations may take infinitely long, leading to the undecidability of datalog on some infinite structures. But even in the decidable cases datalog on infinite structures may have arbitrarily high complexity, and because of this result, we research some structures with the lowest complexity of datalog on infinite structures: Datalog on linear orders (also dense or discrete, with and without constants, even colored) and tree orders has EXPTIME-complete complexity. To achieve the upper bound on these structures, we introduce a tool set specialized for datalog on orders: Order types, distance types and type disjoint programs. The type concept yields a finite representation of the infinite program results, which could also be of interest for practical applications. We create special type disjoint versions of the programs allowing to solve datalog without the recursion inherent in each datalog program. A transfer of our methods shows that constraint satisfaction problems on infinite structures occur with arbitrarily high time complexity, like datalog.

This thesis is concerned with automata over infinite trees. They are given a labeled infinite tree and accept or reject this tree based on its labels. A generalization of these automata with binary decisions are weighted automata. They do not just decide 'yes' or 'no', but rather compute an arbitrary value from a given algebraic structure, e.g., a semiring or a lattice. When passing from unweighted to weighted formalisms, many problems can be translated accordingly. The purpose of this work is to determine the feasibility of solving the inclusion problem for automata on infinite trees and its generalization to weighted automata, the infimum aggregation problem.