We propose a fully automated and dynamic method for generating likely invariants from multithreaded programs and then leveraging these invariants to infer atomic regions and diagnose concurrency errors in the software code. Although existing methods for dynamic invariant generation perform reasonably well on sequential programs, for multithreaded programs, their effectiveness often reduces dramatically in terms of both the number of invariants that they can generate and the likelihood of them being true invariants. We solve this problem by developing a new dynamic invariant generator, which consists of a new LLVM based code instrumentation tool, an INSPECT based thread interleaving explorer, and a customized inference engine inside Daikon. We have evaluated the resulting system on public domain multithreaded C/C++ benchmarks. Our experiments show that the new method is effective in generating high-quality invariants. Furthermore, the state and transition invariants generated by our new method have been proved useful both in error diagnosis and in identifying likely atomic regions in the concurrent software code. / Master of Science

Stateless model checking is a technique for testing and verifying concurrent programs, based on exploring the different ways in which operations executed by the processes of a concurrent program can be scheduled. The goal of the technique is to expose all behaviours that can be a result of scheduling non-determinism. As the number of possible schedulings is huge, however, techniques that reduce the number of schedulings that must be explored to achieve verification have been developed. Dynamic partial order reduction (DPOR) is a prominent such technique. This dissertation presents a number of improvements to dynamic partial order reduction that significantly increase the effectiveness of stateless model checking. Central among these improvements are the Source and Optimal DPOR algorithms (and the theoretical framework behind them) and a technique that allows the observability of the interference of operations to be used in dynamic partial order reduction. Each of these techniques can exponentially decrease the number of schedulings that need to be explored to verify a concurrent program. The dissertation also presents a simple bounding technique that is compatible with DPOR algorithms and effective for finding bugs in concurrent programs, if the number of schedulings is too big to make full verification possible in a reasonable amount of time, even when the improved algorithms are used. All improvements have been implemented in Concuerror, a tool for applying stateless model checking to Erlang programs. In order to increase the effectiveness of the tool, the interference of the high-level operations of the Erlang/OTP implementation is examined, classified and precisely characterized. Aspects of the implementation of the tool are also described. Finally, a use case is presented, showing how Concuerror was used to find bugs and verify key correctness properties in repair techniques for the CORFU chain replication protocol. / UPMARC / RELEASE

Der Bezirk Xilingol wurde als geeignetes Beispiel ausgewählt, weil es zu einem großen Flächenanteil von Grassteppe bedeckt ist und fast alle Phasen der Umweltpolitik Chinas durchlaufen hat. Es wurden zwei deutlich voneinander abgrenzbare Phasen identifiziert, von 1975 bis 2000 und von 2000 bis 2015. Während der ersten Phase, bis 2000, war Landdegradation der dominante Landnutzungswandelprozess, der 11.4 % der Gesamtfläche betraf. In dieser Phase war die menschliche Einflussnahme der Hauptfaktor in acht Landkreisen, die sich ändernden Wasserverhältnisse war es in sechs Landkreisen. Während der zweiten Phase, ab 2000, setzte ein spürbare Erholung des Zustandes auf 12 % des Gesamtgebietes ein, während die Degradation jedoch weiter voranschritt und zusätzliche 9,5 % des Landes veränderte. Während dieser Phase wurde die Städtebildung zum dominanten Treiber für die Landdegradierung in sieben Landkreisen, während der Einfluss menschlicher Störungen und der Wasserverfügbarkeit wieder zurückging. Nach der Identifizierung der Haupttreiber für die Landdegradation, wurde die komplexe Beziehung zwischen verschiedenen Treibern und der Grassteppen-Degradation untersucht. Die Ergebnisse zeigten, dass die Beziehung zwischen dicht bedeckter, moderat bedeckter, und spärlich bedeckter Grassteppe und die Dichte des Schafbesatzes für die Degradationsdynamik in der Grassteppe verantwortlich waren. In dieser Arbeit wurden die Methoden der Clusteranalyse, der Partial-Order-Theorie, und der Hasse Diagramme eingesetzt, um die Haupttreiber der Landdegradation auf Landkreisebene zu identifizieren. Dann wurde ein Ansatz aus dem maschinellen Lernen, XGBoost (eXtreme Gradient Boosting) verwendet, um die Dynamik der Grassteppen-Degradation vorauszusagen. Darüber hinaus wurde SHAP (SHapley Additive exPlanations) eingesetzt, um das von XGBoost erstellte Black-Box-Modell zu in seine Bestanteile zu zerlegen und für jedes Degradations-Pixel in der Karte den Haupttreiber zu extrahieren. / The aims of this thesis are to gain an integrated and systematic understanding of the processes and determinants of land degradation on the Mongolian Plateau. Xilingol was chosen as a suitable example, mainly since it is covered by vast grassland, and has experienced almost all ecological policies that have been implemented in China. Two distinct phases were identified in this region: 1975-2000 and 2000-2015. During the first phase (up to 2000), land degradation was the dominant land use change process, accounting for 11.4% of the total area. During this phase, human disturbance was the major driver in eight counties, whereas the water condition was the dominant driver in six counties. During the second phase (post-2000), land restoration increased (12.0% of the total area), whereas degradation continued, resulting in a further 9.5% of degraded land. During this phase, urbanisation became the dominant driver of land degradation in seven counties, while effects resulting from human disturbance and water availability decreased after 2000. After identifying the major drivers of degradation, the complex relationships between drivers and grassland degradation were captured. The results indicated that the distance to dense, moderately dense grass and sparse grass and sheep density were responsible for the grassland degradation dynamics. In this thesis, a clustering method, partial order theory and Hasse diagram techniques were first used to identify the major drivers of land degradation at the county level. Subsequently, an approach from machine learning, XGBoost (eXtreme Gradient Boosting), was used to predict the dynamics of grassland degradation. Moreover, SHAP (SHapley Additive exPlanations) values were used to open up the black box model, and the primary driver was extracted for each pixel showing degradation.

The factored state representation and concurrency semantics of Petri nets are closely related to those of classical planning models, yet automated planning and Petri net analysis have developed independently, with minimal and mainly unconvincing attempts at crossfertilisation. This thesis exploits the relationship between the formal reachability problem, and the automated planning problem, via Petri net unfolding, which is an attractive reachability analysis method for highly concurrent systems as it facilitates reasoning about independent sub-problems. The first contribution of this thesis is the theory of directed unfolding: controlling the unfolding process with informative strategies, for the purpose of optimality and increased efficiency. The second contribution is the application of directed unfolding to automated planning. Inspired by well-known planning heuristics, this thesis shows how problem specific information can be employed to guide unfolding, in response to the formal problem of developing efficient, directed reachability analysis methods for concurrent systems. Complimenting this theoretical work, this thesis presents a new forward search method for partial order planning which can be exponentially more efficient than state space search. Our suite of planners based on directed unfolding can perform optimal and suboptimal classical planning subject to arbitrary action costs, optimal temporal planning with respect to arbitrary action durations, and address probabilistic planning via replanning for the most likely path. Empirical results reveal directed unfolding is competitive with current state of the art automated planning systems, and can solve Petri net reachability problems beyond the reach of the original “blind” unfolding technique. / Thesis (Ph.D.) -- University of Adelaide, School of Electrical and Electronic Engineering, 2008

Dès qu’on manipule des ordres partiels (des hiérarchies), il est naturel de se demander comment les représenter dans un système informatique. Parmi les solutions proposées dans la littérature, on retrouve le codage par vecteur de bits. Dans cette thèse, nous nous intéressons au problème de calcul d’un codage des ordres par vecteur de bits de taille minimale, aussi connu par le problème de calcul de la 2-dimension des ordres, qui est NP-complet. Nous proposons des solutions du problème de nature heuristique, pour le cas général et pour des classes d’ordres particulières.Cette thèse présente également des résultats sur des conjectures autour de la 2-dimension des arbres. Notamment celle de Habib et al. à propos de la 2-approximabilité de la 2-dimension des arbres. Nous proposons quelques pistes de preuve de cette conjecture puis une reformulation, permettant d’apporter un nouveau regard sur le problème en question et d’espérer trouver des codages des ordres par vecteur de bits efficaces et de taille inférieure à leur 2-dimension. Nous apportons une réponse négative à deux autres conjectures. / The main question asked when manipulating partial orders (hierarchies), is how to represent them in computer. Among solutions proposed in literature, there is the bit-vector encoding. In this thesis, we consider the problem of computing a bit-vector encoding of orders with minimal size, which is also known as the problem of computing the2-dimension of orders that is NP-complete. We propose heuristics solutions of the problem for the general case and for some particular order classes. In addition, this thesis presents some results about conjectures on the 2-dimension of trees. Especially, the conjecture of Habib et al. about the 2-approximability of the 2-dimension of trees. We propose some ideas of a proof of this conjecture then give a reformulation of it that brings new perspectives on the problem that are finding efficient bits-vector encodings of orders of size less than their 2-dimension. We disprove two other conjectures.

The thesis focuses on two open problems on finite partially ordered sets: the structure of order polytopes and the approximation of the number of linear extensions of a poset by mean of graph entropy. The polytopes considered here are the linear ordering polytope, the semiorder polytope, the interval order polytope, the partial order polytope and also a generalisation of the linear ordering polytope: the linear extension polytope of a fixed poset P. Various results on the structure of theses polytopes are proved in the first part of the thesis. In the second part of the thesis, we improve the existing bounds linking the entropy of the incomparability graph of the poset P and its number of linear extension. / Le but de la thèse est d'étudier deux problèmes ouverts sur les ensembles ordonnés finis: la structure des polytopes d'ordre et l'approximation du nombre d'extensions linéaires d'un ordre partiel au moyen de la notion d'entropie de graphe. Les polytopes considérés sont le polytope des ordres totaux, le polytope des semiordres, le polytope des ordres d'intervalles, le polytope des ordres partiels, ainsi qu'une généralisation du polytope des ordres totaux: le polytope des extensions linéaires d'un ensemble ordonné fixé P. Des résultats sur la structure de ces polytopes sont présentés dans la première partie de la thèse. Dans la deuxième partie de la thèse, nous améliorons les bornes existantes liant l'entropie du graphe d'incomparabilité d'un ordre partiel et son nombre d'extensions linéaires. / Doctorat en Sciences / info:eu-repo/semantics/nonPublished

Partial order planning is an important approach that solves planning problems without completely specifying the orderings between the actions in the plan. This property provides greater flexibility in executing plans; hence making the partial order planners a preferred choice over other planning methodologies. However, in order to find partially ordered plans, partial order planners perform a search in plan space rather than in space of world states and an uninformed search in plan space leads to poor efficiency. In this thesis, I discuss applying a reinforcement learning method, called First-visit Monte Carlo method, to partial order planning in order to design agents which do not need any training data or heuristics but are still able to make informed decisions in plan space based on experience. Communicating effectively with the agent is crucial in reinforcement learning. I address how this task was accomplished in plan space and the results from an evaluation of a blocks world test bed.

In dieser Arbeit geht es um die schrittweise Verfeinerung verteilter Algorithmen. Dabei wird ein einfacher Algorithmus, der einige gewünschte Eigenschaften hat, Schritt für Schritt zu einem komplexen Algorithmus verfeinert, der konkrete Implementationsanforderungen erfüllt, so daß in jedem Schritt die gewünschten Eigenschaften erhalten bleiben. Wir stellen einen neuen eigenschaftserhaltenden Verfeinerungsbegriff vor, der auf der kausalen Ordnung der Aktionen eines Algorithmus basiert. Diesen Begriff definieren wir als Transitionsverfeinerung für elementare Petrinetze und diskutieren Beweiskriterien. Danach definieren und diskutieren wir die simultane Verfeinerung mehrerer Transitionen. Zur Modellierung komplexer verteilter Algorithmen sind elementare Petrinetze oft nicht adäquat. Wir benutzen deshalb algebraische Petrinetze. Wir definieren Transitionsverfeinerung für algebraische Petrinetze und stellen einen Zusammenhang zur simultanen Verfeinerung von Transitionen in elementaren Petrinetzen her. Transitionsverfeinerung ist besonders für Verfeinerungsschritte geeignet, in denen synchrone Kommunikation zwischen Agenten durch asynchronen Nachrichtenaustausch ersetzt wird. Wir zeigen dies am Beispiel eines komplexen verteilten Algorithmus, zur Berechnung des minimalen spannenden Baumes in einem gewichteten Graphen. Wir zeigen die Korrektheit dieses Algorithmus in mehreren Schritten, von denen einige Schritte Transitionsverfeinerungen sind. In anderen Schritten sind klassische Verfeinerungsbegriffe ausreichend. Wir übertragen deshalb auch einen klassischen Verfeinerungsbegriff in unser formales Modell. / The topic of this PhD thesis is the stepwise refinement of distributed algorithms. Stepwise refinement starts with a simple algorithm with certain desired properties. This algorithm is refined step by step such that the desired properties are preserved in each refinement step. The result is a complex distributed algorithm which satisfies concrete implementation requirements and which still has the desired properties. We propose a new property preserving notion of refinement which is based on the causal ordering of actions of an algorithm. We call this notion transition refinement and we define it first for elementary Petri nets. Furthermore, we discuss proof criteria. Then, we define and discuss the simultaneous refinement of several transitions. For modelling complex distributed algorithms, we use algebraic Petri nets instead of elementary Petri nets. We define transition refinement for algebraic Petri nets, and we show its relationship to simultaneous transition refinement in elementary Petri nets. Transition refinement is particularly suitable for refinement steps in which synchronous communication between agents is replaced by asynchronous message passing. We show this by means of a complex distributed algorithm for determining the minimal spanning tree of a weighted graph. We prove the correctness of this algorithm in several steps. Some of these steps are transition refinements. For other steps, well-known notions of refinement are sufficient. Therefore, we also carry over a well-known notion of refinement into our formal model.

La conception d'algorithmes pour les systèmes concurrents et répartis est subtile et difficile. Ces systèmes sont enclins à des blocages et à des conditions de course et sont par conséquent difficiles à reproduire La vérification formelle est une technique essentielle pour modéliser le système et ses propriétés et s'assurer de sa correction au moyen du model checking. Des langages formels tels TLA+ permettent de décrire des algorithmes compliqués de manière assez concise, mais les concepteurs d'algorithmes trouvent souvent difficile de modéliser un algorithme par un ensemble de formules. Dans ce mémoire nous présentons le langage PlusCal-2 qui vise à allier la simplicité de pseudo-code à la capacité d'être vérifié formellement. PlusCal-2 améliore le langage algorithmique PlusCal conçu par Lamport en levant certaines restrictions de ce langage et en y ajoutant de nouvelles constructions. Notre langage est destiné à la description d'algorithmes à un niveau élevé d'abstraction. Sa syntaxe ressemble à du pseudo-code mais il est tout à fait expressif et doté d'une sémantique formelle. Pour calculer la dépendance conditionnelle pour les algorithmes en PlusCal-2 nous exploitons des informations sur la localité des actions et nous générons des prédicats d'indépendance. Nous proposons également une adaptation d'un algorithme de réduction par ordre partiel dynamique pour une variante du model checker TLC. Enfin, nous proposons une variante d'un algorithme de réduction par ordre partiel statique s'appuyant sur une relation de dépendance constante, et son implantation au sein de TLC. Nous présentons nos résultats expérimentaux et une preuve de correction / Designing sound algorithms for concurrent and distributed systems is subtle and challenging. These systems are prone to deadlocks and race conditions, and are therefore hard to reproduce. Formal verification is a key technique to model the system and its properties and then perform verification by means of model checking. Formal languages like TLA+ have the ability to describe complicated algorithms quite concisely, but algorithm designers often find it difficult to model an algorithm in the form of formulas. In this thesis, we present PlusCal-2 that aims at being similar to pseudo-code while being formally verifiable. PlusCal-2 improves upon Lamport?s PlusCal algorithm language by lifting some of its restrictions and adding new constructs. Our language is intended for describing algorithms at a high level of abstraction. Finite instances of algorithms described in PlusCal-2 can be verified through the TLC model checker. The second contribution presented in this thesis is a study of partial-order reduction methods using conditional and constant dependency relation. To compute conditional dependency for PlusCal-2 algorithms, we exploit their locality information and present them in the form of independence predicates. We also propose an adaptation of a dynamic partial-order reduction algorithm for a variant of the tlc model checker. As an alternative to partial order reduction based on conditional dependency, we also describe a variant of a static partial-order reduction algorithm for the tlc model checker that relies on constant dependency relation. We also present our results for the experiments along with the proof of correctness

This thesis is dedicated to the development of statistical and computational methods for the analysis of DNA sequences and gene expression time series.<br /><br />First we study a parsimonious Markov model called Mixture Transition Distribution (MTD) model which is a mixture of Markovian transitions. The overly high number of constraints on the parameters of this model hampers the formulation of an analytical expression of the Maximum Likelihood Estimate (MLE). We propose to approach the MLE thanks to an EM algorithm. After comparing the performance of this algorithm to results from the litterature, we use it to evaluate the relevance of MTD modeling for bacteria DNA coding sequences in comparison with standard Markovian modeling.<br /><br />Then we propose two different approaches for genetic regulation network recovering. We model those genetic networks with Dynamic Bayesian Networks (DBNs) whose edges describe the dependency relationships between time-delayed genes expression. The aim is to estimate the topology of this graph despite the overly low number of repeated measurements compared with the number of observed genes. <br /><br />To face this problem of dimension, we first assume that the dependency relationships are homogeneous, that is the graph topology is constant across time. Then we propose to approximate this graph by considering partial order dependencies. The concept of partial order dependence graphs, already introduced for static and non directed graphs, is adapted and characterized for DBNs using the theory of graphical models. From these results, we develop a deterministic procedure for DBNs inference. <br /><br />Finally, we relax the homogeneity assumption by considering the succession of several homogeneous phases. We consider a multiple changepoint<br />regression model. Each changepoint indicates a change in the regression model parameters, which corresponds to the way an expression level depends on the others. Using reversible jump MCMC methods, we develop a stochastic algorithm which allows to simultaneously infer the changepoints location and the structure of the network within the phases delimited by the changepoints. <br /><br />Validation of those two approaches is carried out on both simulated and real data analysis.