L'un des principaux problèmes que les applications Webs doivent gérer aujourd'hui est l'évolutivité des données. Dans cette thèse, nous considérons ce problème et plus précisément l'évolution des documents actifs. Les documents actifs sont documents XML pouvant évolués grâce à l'activation d'appel de services Web. Ce formalisme a déjà été utilisé dans le cadre de la gestion d'information distribuée. Les principales contributions de cette thèse sont l'étude théorique de différentes notions pour l'implémentation de deux systèmes gérant des applications manipulant des flux de données et des applications de type workflow. Dans un premier temps, nous étudions des notions reliées à la maintenance de vues sur des documents actifs. Ces notions sont utilisées dans l'implémentation d'un processeur de flux de données appelé Axlog widget manipulant des flux à travers un document actif. La deuxième contribution porte sur l'expressivité de différents formalismes pour contraindre le séquencement des activations d'un document actif. Cette étude a été motivée par l'implémentation d'un système gérant des workflows focalisés sur les données utilisant les documents actifs, appelé Axart. / One of the major issues faced by Web applications is the management of evolving of data. In this thesis, we consider this problem and in particular the evolution of active documents. Active documents is a formalism describing the evolution of XML documents by activating Web services calls included in the document. It has already been used in the context of the management of distributed data \cite{axml}. The main contributions of this thesis are theoretical studies motivated by two systems for managing respectively stream applications and workflow applications. In a first contribution, we study the problem of view maintenance over active documents. The results served as the basis for an implementation of stream processors based on active documents called Axlog widgets. In a second one, we see active documents as the core of data centric workflows and consider various ways of expressing constraints on the evolution of documents. The implementation, called Axart, validated the approach of a data centric workflow system based on active documents. The hidden Web (also known as deep or invisible Web), that is, the partof the Web not directly accessible through hyperlinks, but through HTMLforms or Web services, is of great value, but difficult to exploit. Wediscuss a process for the fully automatic discovery, syntacticand semantic analysis, and querying of hidden-Web services. We proposefirst a general architecture that relies on a semi-structured warehouseof imprecise (probabilistic) content. We provide a detailed complexityanalysis of the underlying probabilistic tree model. We describe how wecan use a combination of heuristics and probing to understand thestructure of an HTML form. We present an original use of a supervisedmachine-learning method, namely conditional random fields,in an unsupervised manner, on an automatic, imperfect, andimprecise, annotation based on domain knowledge, in order to extractrelevant information from HTML result pages. So as to obtainsemantic relations between inputs and outputs of a hidden-Web service, weinvestigate the complexity of deriving a schema mapping between databaseinstances, solely relying on the presence of constants in the twoinstances. We finally describe a model for the semantic representationand intensional indexing of hidden-Web sources, and discuss how toprocess a user's high-level query using such descriptions.

We can associate an incidence graph with any CNF formula. It's a bipartite graph, in which he first part corresponds to variables and the second one to clauses. We can define matched formulas and biclique satisfiable formulas, based on this incidence graph. Both of these classes share an interesting property: Given a formula F which is matched or biclique satisfiable, F remains satisfiable even after we switch polarity of any occurrence of any literal. Class of formulas with this property is called var-satisfiable. In this thesis, we consider a parameterized algorithm introduced by Stefan Szeider for deciding satisfiability of formulas with small deficiency. Here deficiency of a formula is defined as a difference between the number of clauses and the number of variables in the formula. We explain why this algorithm cannot be simply generalized for the case of biclique satisfiable formulas. Since the problem of determining whether a formula is biclique satisfiable is NP-complete, we introduce a heuristic, which tries to find some biclique cover in time O(n2 e), where n denotes the number of variables and e denotes the length of the input formula. We performed experiments testing this heuristic on random formulas. The results of these experiments suggest, that there is a phase transition in the behaviour of the heuristic....

Many bugs are reported during the software maintenance phase, and in order for asoftware product to have a longer life, it must effectively handle and resolve thesebugs. As a result, when cost and time are considered, a prioritized list of bugs isrequired for all products. Due to some factors, such as user expertise, the numberof bugs, the priority methodology, and how critical the software is, developing a prioritization technique that includes user inputs and preset bug constraints to producea final prioritization list of software bugs is challenging. Our approach to solvingthe prioritization problem involves combining an SMT solver with user interactionto provide the best possible solution. Our findings suggest that this strategy outperforms both random and non-interactive bug prioritization methods.

Prioritization of software requirements is an important part of the requirements engineering process within the industry of software development. There are many different methods for achieving the most optimal order of software requirements, a list that shows in what order the requirements should be implemented. This degree project utilizes the SMT-based solver Z3 for an interactive prioritization algorithm. Previous studies have shown good results with another SMT-based solver called Yices. With the newer Z3 from Microsoft, the results have been improved further, and the tool is based on Python, and the framework for Z3 is called Z3PY. Experiments have been conducted on a set of different software requirements derived from a project in the healthcare industry and show that the Z3 solution is, in general, improving the requirements prioritization compared to other mentioned solutions in the study that has been tested on the same set of requirements. Results show that the Z3 solution outperformed the other SMT-based solution Yices by 2-4% regarding disagreement and by 3% regarding average distance. The results are significantly improved based on an ANOVA test with a p-value <= 0.05.

This work deals with the PSO technique (Particle Swarm Optimization), which is capable to solve complex problems. This technique can be used for solving complex combinatorial problems (the traveling salesman problem, the tasks of knapsack), design of integrated circuits and antennas, in fields such as biomedicine, robotics, artificial intelligence or finance. Although the PSO algorithm is very efficient, the time required to seek out appropriate solutions for real problems often makes the task intractable. The goal of this work is to accelerate the execution time of this algorithm by the usage of Graphics processors (GPU), which offers higher computing potential while preserving the favorable price and size. The boolean satisfiability problem (SAT) was chosen to verify and benchmark the implementation. As the SAT problem belongs to the class of the NP-complete problems, any reduction of the solution time may broaden the class of tractable problems and bring us new interesting knowledge.

Temporal logics are a very popular family of logical languages, used to specify properties of abstracted systems. In the last few years, many extensions of temporal logics have been proposed, in order to address the need to express more than just abstract properties. In our work we study temporal logics extended by local constraints, which allow to express quantitative properties on data values from an arbitrary relational structure called the concrete domain. An example of concrete domain can be (Z, <, =), where the integers are considered as a relational structure over the binary order relation and the equality relation. Formulas of temporal logics with constraints are evaluated on data-words or data-trees, in which each node or position is labeled by a vector of data from the concrete domain. We call the constraints local because they can only compare values at a fixed distance inside such models. Several positive results regarding the satisfiability of LTL (linear temporal logic) with constraints over the integers have been established in the past years, while the corresponding results for branching time logics were only partial. In this work we prove that satisfiability of CTL* (computation tree logic) with constraints over the integers is decidable and also lift this result to ECTL*, a proper extension of CTL*. We also consider other classes of concrete domains, particularly ones that are \"tree-like\". We consider semi-linear orders, ordinal trees and trees of a fixed height, and prove decidability in this framework as well. At the same time we prove that our method cannot be applied in the case of the infinite binary tree or the infinitely branching infinite tree. We also look into extending the expressiveness of our logic adding non-local constraints, and find that this leads to undecidability of the satisfiability problem, even on very simple domains like (Z, <, =). We then find a way to restrict the power of the non-local constraints to regain decidability.

Matched instances of the quantum satisfiability problem have an interesting property: They always have a product state solution. However, it is not clear how to find such a solution efficiently. Recenttly some progress on this question has been made by considering restricted instances of this problem. In this note we consider a different restriction of the problem which turns out to be solvable by techniques of linear algebra.

Motivées par de nombreuses applications allant du traitement XML à lavérification d'exécution de programmes, de nombreuses logiques sur les arbresde données et les flux de données ont été développées dans la littérature.Celles-ci offrent divers compromis entre expressivité et complexitéalgorithmique ; leur problème de satisfiabilité a souvent une complexité nonélémentaire ou peut même être indécidable.De plus, leur étude à travers des approches de théories des modèles ou dethéorie des automates peuvent être algorithmiquement impraticables ou manquerde modularité.Dans une première partie, nous étudions l'utilisation de systèmes de preuvecomme un moyen modulaire de résoudre le problème de satisfiabilité des données logiques sur des structures linéaires.Pour chaque logique considérée, nous développons un calcul d'hyperséquentscorrect et complet et décrivons une stratégie de recherche de preuve optimaledonnant une procédure de décision NP.En particulier, nous présentons un fragment NP-complet de la logique temporelle sur les ordinaux avec données, la logique complète étant indécidable, qui est exactement aussi expressif que le fragment à deux variables de la logique du premier ordre sur les ordinaux avec données.Dans une deuxième partie, nous menons une étude empirique des principaleslogiques à la XPath décidables proposées dans la littérature.Nous présentons un jeu de tests que nous avons développé à cette fin etexaminons comment ces logiques pourraient être étendues pour capturer davantage de requêtes du monde réel sans affecter la complexité de leur problème de satisfiabilité.Enfin, nous analysons les résultats que nous avons recueillis à partir de notre jeu de tests et identifions les nouvelles fonctionnalités à prendre en charge afin d’accroître la couverture pratique de ces logiques. / Motivated by applications ranging from XML processing to runtime verificationof programs, many logics on data trees and data streams have been developed in the literature.These offer different trade-offs between expressiveness and computationalcomplexity; their satisfiability problem has often non-elementary complexity or is even undecidable.Moreover, their study through model-theoretic or automata-theoretic approaches can be computationally impractical or lacking modularity.In a first part, we investigate the use of proof systems as a modular way tosolve the satisfiability problem of data logics on linear structures.For each logic we consider, we develop a sound and complete hypersequentcalculus and describe an optimal proof search strategy yielding an NPdecision procedure.In particular, we exhibit an NP-complete fragment of the tense logic over data ordinals---the full logic being undecidable---, which is exactly as expressive as the two-variable fragment of the first-order logic on data ordinals.In a second part, we run an empirical study of the main decidable XPath-likelogics proposed in the literature.We present a benchmark we developed to that end, and examine how these logicscould be extended to capture more real-world queries without impacting thecomplexity of their satisfiability problem.Finally, we discuss the results we gathered from our benchmark, and identifywhich new features should be supported in order to increase the practicalcoverage of these logics.

京都大学 / 0048 / 新制・課程博士 / 博士(情報学) / 甲第19335号 / 情博第587号 / 新制||情||102(附属図書館) / 32337 / 京都大学大学院情報学研究科知能情報学専攻 / (主査)教授 山本 章博, 教授 鹿島 久嗣, 教授 五十嵐 淳 / 学位規則第4条第1項該当 / Doctor of Informatics / Kyoto University / DFAM

No description available.