<p>Abstract: Considering the Schrödinger equation $\Delta_x u = i\partial{u}/\partial{t}$, we have a solution $u$ on the form $$u(x, t)= (2\pi)^{-n} \int_{\RR} {e^{i x\cdot \xi}e^{it|\xi|^2}\widehat{f}(\xi)}\, d \xi, x \in \RR, t \in \mathbf{R}$$ where $f$ belongs to the Sobolev space. It was shown by Sjögren and Sjölin, that assuming $\gamma : \mathbf{R}_+ \rightarrow \mathbf{R}_+ $ being a strictly increasing function, with $\gamma(0) = 0$ and $u$ and $f$ as above, there exists an $f \in H^{n/2} (\RR)$ such that $u$ is continuous in $\{ (x, t); t>0 \}$ and $$\limsup_{(y,t)\rightarrow (x,0),|y-x|<\gamma (t), t>0} |u(y,t)|= + \infty$$ for all $x \in \RR$. This theorem was proved by choosing $$\widehat{f}(\xi )=\widehat{f_a}(\xi )= | \xi | ^{-n} (\log | \xi |)^{-3/4} \sum_{j=1}^{\infty} \chi _j(\xi)e^{- i( x_{n_j} \cdot \xi + t_j | \xi | ^a)}, \, a=2,$$ where $\chi_j$ is the characteristic function of shells $S_j$ with the inner radius rapidly increasing with respect to $j$. The purpose of this essay is to explain the proof given by Sjögren and Sjölin, by first showing that the theorem is true for $\gamma (t)=t$, and to investigate the result when we use $$S^a f_a (x, t)= (2 \pi)^{-n}\int_{\RR} {e^{i x\cdot \xi}e^{it |\xi|^a}\widehat{f_a}(\xi)}\, d \xi$$ instead of $u$.</p>

We say that a~graph admits a~nowhere-zero k-flow if we can assign a~direction and a~positive integer (<k) as a~flow to each edge so that total in-flow into $v$ and total out-flow from $v$ are equal for each vertex $v$. In 1954, Tutte conjectured that every bridgeless graph admits a~nowhere-zero 5-flow and the conjecture is still open. Kochol in his recent papers introduces a~computational method how to prove that a~minimal counterexample cannot contain short circuits (up to length 10). In this Thesis, we provide a~comprehensive view on this method. Moreover, since Kochol does not share his implementation and in order to independently verify the method, we provide our source code that validates Kochol's results and extend them: we prove that any minimal counterexample to the conjecture does not contain any circuit of length less than 12. Powered by TCPDF (www.tcpdf.org)

Abstract: Considering the Schrödinger equation $\Delta_x u = i\partial{u}/\partial{t}$, we have a solution $u$ on the form $$u(x, t)= (2\pi)^{-n} \int_{\RR} {e^{i x\cdot \xi}e^{it|\xi|^2}\widehat{f}(\xi)}\, d \xi, x \in \RR, t \in \mathbf{R}$$ where $f$ belongs to the Sobolev space. It was shown by Sjögren and Sjölin, that assuming $\gamma : \mathbf{R}_+ \rightarrow \mathbf{R}_+ $ being a strictly increasing function, with $\gamma(0) = 0$ and $u$ and $f$ as above, there exists an $f \in H^{n/2} (\RR)$ such that $u$ is continuous in $\{ (x, t); t&gt;0 \}$ and $$\limsup_{(y,t)\rightarrow (x,0),|y-x|&lt;\gamma (t), t&gt;0} |u(y,t)|= + \infty$$ for all $x \in \RR$. This theorem was proved by choosing $$\widehat{f}(\xi )=\widehat{f_a}(\xi )= | \xi | ^{-n} (\log | \xi |)^{-3/4} \sum_{j=1}^{\infty} \chi _j(\xi)e^{- i( x_{n_j} \cdot \xi + t_j | \xi | ^a)}, \, a=2,$$ where $\chi_j$ is the characteristic function of shells $S_j$ with the inner radius rapidly increasing with respect to $j$. The purpose of this essay is to explain the proof given by Sjögren and Sjölin, by first showing that the theorem is true for $\gamma (t)=t$, and to investigate the result when we use $$S^a f_a (x, t)= (2 \pi)^{-n}\int_{\RR} {e^{i x\cdot \xi}e^{it |\xi|^a}\widehat{f_a}(\xi)}\, d \xi$$ instead of $u$.

In 1971, Ganea put forth a conjecture that the LS category of the Cartesian product of a topological space X with a sphere Sn is always exactly 1 higher than the LS category of X by itself. Several special cases of this conjecture were proven in the years following, however the question remained open until 1998 when Iwase produced not just one, but infinitely many counterexamples. In this thesis, we study the methods implemented by Iwase, culminating in the construction of his counterexample.

It is well acknowledged in the AI community that finding a good reward function for reinforcement learning is extremely challenging. Apprenticeship learning (AL) is a class of “learning from demonstration” techniques where the reward function of a Markov Decision Process (MDP) is unknown to the learning agent and the agent uses inverse reinforcement learning (IRL) methods to recover expert policy from a set of expert demonstrations. However, as the agent learns exclusively from observations, given a constraint on the probability of the agent running into unwanted situations, there is no verification, nor guarantee, for the learnt policy on the satisfaction of the restriction. In this dissertation, we study the problem of how to guide AL to learn a policy that is inherently safe while still meeting its learning objective. By combining formal methods with imitation learning, a Counterexample-Guided Apprenticeship Learning algorithm is proposed. We consider a setting where the unknown reward function is assumed to be a linear combination of a set of state features, and the safety property is specified in Probabilistic Computation Tree Logic (PCTL). By embedding probabilistic model checking inside AL, we propose a novel counterexample-guided approach that can ensure both safety and performance of the learnt policy. This algorithm guarantees that given some formal safety specification defined by probabilistic temporal logic, the learnt policy shall satisfy this specification. We demonstrate the effectiveness of our approach on several challenging AL scenarios where safety is essential.

Avec la montée de la connectivité entre les appareils (internet des objets), nouvelles possibilités de coordination entre les différentes entités ont ouvert. En même temps, des résultats récents, issus de la théorie de l'information, ont fourni des limites pour la performance optimale que tout système de coordination pourrait atteindre sous certaines structures d'information. Dans cette thèse, nous développons ces résultats théoriques dans le but de les rendre plus facilement applicable aux problèmes pratiques. À cet égard, la contribution de cette thèse est double : 1) En outre développer les résultats théoriques pour fournir un aperçu de la structure des solutions au problème d'optimisation posés dans les travaux antérieurs, ainsi que la généralisation des résultats. 2) Développer des algorithmes qui exploitent le cadre théorique fourni par les travaux antérieurs pour concevoir des mécanismes de coordination pratiques, décentralisées et robustes. La généralité de l'approche se prête à diverses applications, dont les éléments suivants ont été traités: optimisation de puissance dans les réseaux sans fil, planification de la consommation d'énergie dans les applications de réseau intelligent, ainsi que Witsenhausen contre-exemple, un problème important issu de la théorie du contrôle. Diverses possibilités sont encore à venir pour exploiter le cadre et les outils développés ici. En effet, ils pourraient être utiles même dans des domaines qui ne sont pas abordés dans cette thèse, mais qui nécessitent une coordination entre les agents avec des informations différentes à la disposition de chacun. / With the rise in connectivity between appliances (Internet of Things), new avenues for coordination between various entities have opened up. At the same time, recent information theoretical results have provided bounds for the performance that any coordination scheme could achieve under certain information structures. In this thesis, we further develop those information theoretical results with the aim of making them applicable more easily to practical problems. In this regard, the contribution of this thesis is twofold: 1) Further developing the aforementioned information theoretical results to provide insights into the structure of the solutions to optimization problem posed in them, as well as generalizing some results. 2) Developing algorithms which exploit the theoretical framework provided by Information theory to devise practical, decentralized and robust coordination schemes. The generality of the approach lends itself to various applications, of which the following were treated: power optimization in wireless networks, power consumption scheduling in smart grid applications, as well as Witsenhausen counterexample, an important toy problem in control theory. Various opportunities still lie ahead to exploit the framework and tools developed herein. Indeed, they could be useful even in domains which have not been explored in this thesis but which require coordination between agents with different information available to each.

Dans cette thèse nous donnons une description complète de la dynamique d’une classe L de fonctions de degré un du cercle, supposées de classe (deux fois dérivable) C^2 à l’exception de deux points où seule la continuité est exigée, et telles qu’elles soient constantes sur un des intervalles délimité par ces derniers. De plus sur des demi-voisinages ouverts de ces points elles s’écrivent sous la forme x^l où l est un nombre réel positif appelé l’exposant critique de la fonction. Dans le chapitre 2 nous montrons pour la sous-classe de L des fonctions dont le nombre de rotation est de type borné, l’existence d’une transition dans la géométrie du système lorsque l’exposant critique traverse 2. Le cas plus général de fonctions en L avec nombre de rotation infinie est considéré dans le chapitre 3. Il devient pourtant plus délicat d’émettre des conjectures ; on rencontre parfois des surprises dues à laprésence de phénomènes paraboliques. De plus, nos résultats sur les applications du cercle nous permettent d’étudier l’intéressante théorie des flots de Cherry (chapitre 4). En particulier, on construit un exemple de tel flot qui a ensemble quasi-minimale métriquement non trivial. Nous donnons également une description complète des mesures physiques sur ce flot. Dans le chapitre 5 nous construisons un contrexemple de Denjoy qui est un difféomorphisme (indéfiniment dérivable) C^∞ partout sauf dans un point qui est demi-critique plat pour la fonction. / The principal purpose of this thesis is to give a complete description of the dynamics of a class L of circle maps of degree one, supposed to be (two times differentiable) C^2 everywhere with the exception of two points where the maps are continuous. Moreover the maps are constant on any of the two intervals delimited by this two points. In particular, on a half open neighborhood of this two points the maps can be written as an x^l where the real positive number l is called the critical exponent of the function. In Chapter 2 we prove the existence of a global phase transition when the critical exponent passes through l = 2, for functions of L with rotation number of bounded type. The more general case of function in L with rotation number of unbounded type is studied in Chapter 3. In this case it becomes more delicate to make conjectures ; in fact it often hides surprises due to the presence of underlying parabolic phenomena. Moreover, our results on circle maps give us the opportunity to study the interesting theory of Cherry flows (Chapter 4). In particular we construct an example of such a flow with a metrically non-trivial quasi-minimal set and we give a complete description on the physical measures for this kind of flows. In Chapter 5 we construct a Denjoy counterexample which is a (smooth) C^∞ diffeomorphism away from a half-critical point.

Immer wenn neue Anforderungen an ein System gestellt werden, müssen die Korrektheit und Konsistenz der Systemspezifikation überprüft werden, was in der Praxis in der Regel manuell erfolgt. Eine mögliche Option, um die Nachteile dieser manuellen Analyse zu überwinden, ist das sogenannte Contract-Based Design. Dieser Entwurfsansatz kann den Verifikationsprozess zur Überprüfung, ob die Anforderungen auf oberster Ebene konsistent verfeinert wurden, automatisieren. Die Verifikation kann somit iterativ durchgeführt werden, um die Korrektheit und Konsistenz des Systems angesichts jeglicher Änderung der Spezifikationen sicherzustellen. Allerdings ist es aufgrund der mangelnden Benutzerfreundlichkeit und der Schwierigkeiten bei der Interpretation von Verifizierungsergebnissen immer noch eine Herausforderung, formale Ansätze in der Industrie einzusetzen. Stellt beispielsweise der Model Checker bei der Verifikation eine Inkonsistenz fest, generiert er ein Gegenbeispiel (Counterexample) und weist gleichzeitig darauf hin, dass die gegebenen Eingabespezifikationen inkonsistent sind. Hier besteht die gewaltige Herausforderung darin, das generierte Gegenbeispiel zu verstehen, das oft sehr lang, kryptisch und komplex ist. Darüber hinaus liegt es in der Verantwortung der Ingenieurin bzw. des Ingenieurs, die inkonsistente Spezifikation in einer potenziell großen Menge von Spezifikationen zu identifizieren. Diese Arbeit schlägt einen Ansatz zur Erklärung von Gegenbeispielen (Counterexample Explanation Approach) vor, der die Verwendung von formalen Methoden vereinfacht und fördert, indem benutzerfreundliche Erklärungen der Verifikationsergebnisse der Ingenieurin bzw. dem Ingenieur präsentiert werden. Der Ansatz zur Erklärung von Gegenbeispielen wird mittels zweier Methoden evaluiert: (1) Evaluation anhand verschiedener Anwendungsbeispiele und (2) eine Benutzerstudie in Form eines One-Group Pretest-Posttest Experiments. / Whenever new requirements are introduced for a system, the correctness and consistency of the system specification must be verified, which is often done manually in industrial settings. One viable option to traverse disadvantages of this manual analysis is to employ the contract-based design, which can automate the verification process to determine whether the refinements of top-level requirements are consistent. Thus, verification can be performed iteratively to ensure the system’s correctness and consistency in the face of any change in specifications. Having said that, it is still challenging to deploy formal approaches in industries due to their lack of usability and their difficulties in interpreting verification results. For instance, if the model checker identifies inconsistency during the verification, it generates a counterexample while also indicating that the given input specifications are inconsistent. Here, the formidable challenge is to comprehend the generated counterexample, which is often lengthy, cryptic, and complex. Furthermore, it is the engineer’s responsibility to identify the inconsistent specification among a potentially huge set of specifications. This PhD thesis proposes a counterexample explanation approach for formal methods that simplifies and encourages their use by presenting user-friendly explanations of the verification results. The proposed counterexample explanation approach identifies and explains relevant information from the verification result in what seems like a natural language statement. The counterexample explanation approach extracts relevant information by identifying inconsistent specifications from among the set of specifications, as well as erroneous states and variables from the counterexample. The counterexample explanation approach is evaluated using two methods: (1) evaluation with different application examples, and (2) a user-study known as one-group pretest and posttest experiment.

In the recent trends, automated systems are increasingly seen to be embedded in human life with the increase of human dependence on software to perform safetycritical tasks like airbag deployment in automobiles to real-time mission planning in UAVs (Unmanned Aircraft Vehicles). The safety-critical nature of the aerospace domain demands for a software without any errors to perform these tasks. Therefore the field of computer science needs to address these challenges by providing necessary formalisms, techniques, and tools that will ensure the correctness of systems despite their complexity. DO-178C/EC-12C is a standard that governs the certification of software for airborne systems in commercial aircraft. The additional supplement DO- 333 enables us to use the formal methods in our technique of verifying the autonomous behaviour of UAV’s. The Mission Manager system is primarily responsible for the execution of behaviour sequence in online and offline mission planning of UAV. This work presents the process of software verification by making use of formal modelling using model checking of the Mission Manager component of ARTIS (Autonomous Rotorcraft Testbed for Intelligent Systems) UAV by gaining advantages from a generic modelling approach. The main idea is to make use of the designed generic models into specific cases like ARTIS in our case. The generic models are designed using the ALFU(R)S (Autonomy Levels For Unmanned Rotorcraft System) framework that delineates the commonalities of several UAVs considered around the world which also includes the ARTIS UAV. Furthermore this work walks through every process involved in model checking like requirements extraction and documentation using a template based method, requirements specification using the temporal logics like LTL and CTL, developing a formal model using NuSMV as a model checking tool to analyze the requirements against the model for the Mission Manager component of MiPlEx (Mission Planning and Execution). Additionally as a validation approach, test sequences are generated by using trap properties or negation properties. This aids for a test generation approach by harnessing counterexample generating capabilities of the NuSMV Model Checker.

In the recent trends, automated systems are increasingly seen to be embedded in human life with the increase of human dependence on software to perform safetycritical tasks like airbag deployment in automobiles to real-time mission planning in UAVs (Unmanned Aircraft Vehicles). The safety-critical nature of the aerospace domain demands for a software without any errors to perform these tasks. Therefore the field of computer science needs to address these challenges by providing necessary formalisms, techniques, and tools that will ensure the correctness of systems despite their complexity. DO-178C/EC-12C is a standard that governs the certification of software for airborne systems in commercial aircraft. The additional supplement DO- 333 enables us to use the formal methods in our technique of verifying the autonomous behaviour of UAV’s. The Mission Manager system is primarily responsible for the execution of behaviour sequence in online and offline mission planning of UAV. This work presents the process of software verification by making use of formal modelling using model checking of the Mission Manager component of ARTIS (Autonomous Rotorcraft Testbed for Intelligent Systems) UAV by gaining advantages from a generic modelling approach. The main idea is to make use of the designed generic models into specific cases like ARTIS in our case. The generic models are designed using the ALFU(R)S (Autonomy Levels For Unmanned Rotorcraft System) framework that delineates the commonalities of several UAVs considered around the world which also includes the ARTIS UAV. Furthermore this work walks through every process involved in model checking like requirements extraction and documentation using a template based method, requirements specification using the temporal logics like LTL and CTL, developing a formal model using NuSMV as a model checking tool to analyze the requirements against the model for the Mission Manager component of MiPlEx (Mission Planning and Execution). Additionally as a validation approach, test sequences are generated by using trap properties or negation properties. This aids for a test generation approach by harnessing counterexample generating capabilities of the NuSMV Model Checker.