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.

No description available.

[pt] Ao menos desde 1916, a quitação é um instituto típico do Direito Privado brasileiro. Mas é certo que, muito antes disso, a quitação já era um instrumento socialmente típico e de absoluta relevância, com presença marcante no tráfico negocial. Apesar da sua importância prática, o instituto da quitação carece de trabalhos monográficos específicos a seu respeito. E custa caro aos tribunais brasileiros a inexistência de um estudo dedicado à sistematização do instituto e ao estabelecimento de parâmetros interpretativos para as situações em que o alcance da eficácia da quitação é objeto de controvérsia. Somente na Segunda Seção do Superior Tribunal de Justiça – órgão fracionário de elevada hierarquia dentro da Corte nacional que tem exatamente a função de uniformizar a jurisprudência – há entendimentos conflitantes sobre a interpretação da quitação que geram insegurança e incerteza ao jurisdicionado quanto aos critérios a serem analisados pelo intérprete para autorizar ou não a investida judicial para ver complementada uma obrigação já anteriormente quitada. Nesse cenário, com o objetivo de, em alguma medida, preencher tal lacuna doutrinária, este trabalho analisará o instituto da quitação de forma sistematizada à luz da legislação brasileira, abordará o seu perfil funcional, examinará precedentes do Superior Tribunal de Justiça que revelam séria divergência e buscará oferecer parâmetros interpretativos para os impasses a respeito do alcance da quitação. / [en] At least since 1916, the discharge is a typical institute of Brazilian Private Law. However, it is certain that, long before that, discharge was already a relevant and socially typical instrument, continuously present in business traffic. Despite its practical importance, the discharge institute lacks specific monographic works about it. And it is costly to the Brazilian courts that there is no study dedicated to systematizing the institute and establishing interpretative parameters for situations in which the scope of the effectiveness of the discharge is a controversial topic. For example, in the Second Section of the Brazilian Superior Court of Justice – a hierarchically high part within the national Court that has the exact function of standardizing the jurisprudence – there are conflicting understandings on the interpretation of the discharge that create insecurity and uncertainty for the person subject to its jurisdiction related to the criteria to be analyzed by the interpreter in order to authorize or not the judicial onslaught to see a previously settled obligation complemented. In this scenario, with the objective of, to some extent, filling this doctrinal gap, this work will analyze the institute of discharge in a systematized way in light of the Brazilian law system, address its functional profile, examine precedents of the Superior Court of Justice representing serious divergence and seek to offer interpretative parameters for certain impasses regarding the scope of the discharge.

Whereas early researchers in computability theory described effective computability in terms of such models as Turing machines, Markov algorithms, and register machines, a recent trend has been to use simple programming languages as computability models. A parallel development to this programming approach to computability theory is the current interest in systematic and scientific development and proof of programs. This paper investigates the feasibility of using formal proofs of programs in computability theory. After describing a framework for formal verification of programs written in a simple theoretical programming language, we discuss the proofs of several typical programs used in computability theory.

Data conversion for evolving events in an Event Sourcing System is a complex issue and needs to be maintainable. There are suggested ways handling data conversion today which combine different methods into a framework. However, there is a lack of exploration of different and alternative methods to handle the complicated matter.This thesis explores data conversion with fine-grained events. The purpose is to explore methods and broaden knowledge for handling data conversion while using attribute driven events called fine-grained events. The goal was to build a proof-of-concept that preserves the attributes reliability and availability and can handle data conversion of these specific events.The results found by using fine-grained events are a decrease in terms of system complexity and a proof-of-concept that maintains the desired attributes. / Datakonvertering för utvecklande händelser i ett Event Sourcing System är en komplex fråga som kräver att systemet är enkelt underhållning. Det finns förslag på sätt att hantera datakonvertering idag, vilket kombinerar olika metoder i ett ramverk. Det finns emellertid en brist på undersökning av olika och alternativa metoder för att hantera den komplexa orsaken.Denna avhandling undersöker datakonvertering med finkorniga händelser. Syftet är att utforska metoder och utvidga kunskap för hantering av datakonvertering genom att använda attributdrivna händelser som kallas finkorniga händelser. Målet var att bygga ett proof-of-concept som bevarar egenskaperpålitlighet och tillgängligt och som dessa specifika händelser.även hanterar datakonvertering förResultaten som hittas genom att använda finkorniga händelser är en minskning av systemkomplexiteten och ett bevis på koncept som upprätthåller de önskade egenskaperna.

Internet of Things (IoT) is a phenomenon that involves providing things or objects with sensors and internet connection. The field of IoT is growing rapidly and there are strong incentives for companies to follow the trend to develop and create an IoT. However, the proportion of IoT initiatives considered to be successful has been shown to be low. This study therefore investigates how a project methodology can support a concept development and secure the business value for IoT initiatives. The project methodology developed in this study is named eXtreme PoC Development (XPD). XPD is based on existing project methodologies from literature and interviews from consulting companies within the field in the Stockholm region. It was evaluated by a case study where fault detection in street lighting was investigated and implemented. The evaluation of the methodology highlighted the importance of defining problems and solutions that are anchored in the business value, calculating a potential of an IoT initiative that determines the continuation of a project, involving stakeholders at an early stage and developing a PoC to validate and evaluate a concept with stakeholders. / Internet of Things (IoT) är ett fenomen som innebär att förse saker eller objekt med sensorer och internetförbindelse. Området för IoT är starkt växande och det finns starka incitament hos företag att följa trenden att utveckla och skapa en IoT. Andelen IoT-initiativ som anses vara framgångsrika har däremot visats sig vara låg. Denna studie undersöker hur en projektmetodik kan stödja en konceptutveckling och säkra affärsnyttan för IoT-initiativ. Projektmetodiken som tagits fram i denna studie benämns eXtreme PoC Development (XPD). XPD baseras på befintliga projektmetodiker från litteratur och intervjuer från konsultbolag i Stockholmsregionen. Den utvärderades genom en fallstudie där feldetektering i ljuspunkter i utomhusmiljö undersöktes och implementerades. Utvärderingen av metodiken belyste vikten av att definiera problem och lösningar som är förankrade i affärsnyttan, att beräkna en potential av ett IoT-initiativ som bestämmer ett projekts fortsättning, att involvera intressenter i ett tidigt stadie och att utveckla en PoC för att validera och utvärdera ett koncept med intressenterna.

Denna studie undersöker huruvida avsiktligt implementerad friktion inom interaktionsdesign kan minska antal användarfel vid insatsprocessen för blockkedjor med Proof-of-Stake teknik. Friktion som avsiktligt implementerats har tidigare visats kunna leda till färre användarfel. Det spekuleras i att blockkedjor kan komma att användas i större utsträckning i framtiden. Eftersom fel i insatsprocessen för en blockkedja med Proof-of-Stake teknik kan leda till att pengar går förlorade valdes det området för att undersökas närmare om friktion kan leda till färre användarfel. Studien avgränsas till en typ av avsiktlig friktion som kallas design for pauses som syftar till att få användaren att tillfälligt stanna upp med sin interaktion. I studien skapades två versioner av en prototyp på en insatsprocess till blockkedjan Ethereum som testades på två olika testgrupper. Ena versionen av prototypen innehöll avsiktligt implementerad friktion och i den andra versionen adderades ingen friktion avsiktligt. Deltagarna i testet ombads utföra insatsprocessen i prototypen där deras interaktioner granskades och statistik fördes på antal användarfel. Användarfelen delades upp i två kategorier: slarvfel och misstag. Resultaten från testerna visar på att avsiktlig friktion av typen design for pauses minskar antal användarfel av typen misstag. Ytterligare forskning krävs för att besvara om design for pauses kan bidra till att minska antal användarfel av typen slarvfel. / This study evaluates whether intentionally implemented friction within interaction design can reduce the amount of user errors in the staking process within blockhains with Proof-of-Stake technology. Intentionally implemented friction has previously been proved to reduce user errors. It is speculated that blockchains may be used to a greater extent in the future. Since user errors in the staking process of a blockchain with Proof-of-Stake technology can result in money being lost, that field was selected to investigate if friction can result in fewer user errors. This study is limited to a type of deliberate friction called design for pauses which aims to temporarily pause the users interaction. In the study, two versions of a prototype were created to simulate the staking process for the Ethereum blockchain and were tested on two different test groups. One version of the prototype had intentionally added friction while in the other version no friction was added intentionally. Participants in the test were asked to perform the staking process in the prototype. Their interactions were analyzed and statistics were kept on the number of user errors. The user errors were divided into two categories: slips and mistakes. The results of the tests shows that deliberate friction of type design for pauses leads to reduced number of user errors of type mistakes. Further research is needed in order to answer whether design for pauses may reduce the number of user errors of type slips.

The thesis investigates how a blockchain can be used to build a decentralised public key infrastructure for the web, by proposing a custom federation blockchain relying on honest majority. Our main contribution is the design of a Proof of Stake protocol based on a stake tree, which builds upon an idea called follow-the-satoshi used in previous papers. Digital identities are stored in an authenticated self-balancing tree maintained by blockchain nodes. Our back-of-the-envelope calculations, based on the size of the domain name system, show that the block size must be set to at least 5.2 MB, while each blockchain node with a one-month transaction history would need to store about 243 GB. Thin clients would have to synchronise about 13.6 MB of block headers per year, and download an additional 3.7 KB of proof data for every leaf certificate which is to be checked. / Uppsatsen undersöker hur en blockkedja kan användas för att bygga en decentraliserad publik nyckel-infrastruktur för webben. Vi ger ett designförslag på en blockkedja som drivs av en pålitlig grupp av noder, där en majoritet antas vara ärliga. Vårt huvudsakliga bidrag är utformningen av ett Proof of Stake-protokoll baserat på ett staketräd, vilket bygger på en idé som kallas follow-the-satoshi omnämnd i tidigare publikationer. Digitala identiteter sparas i ett autentiserat, självbalanserande träd som underhålls av noder anslutna till blockkedjenätverket. Våra preliminära beräkningar baserade på storleken av DNS-systemet visar att blockstorleken måste sättas till åtminstone 5.2 MB, medan varje nod med en månads transaktionshistorik måste spara ungefär 243 GB. Webbläsare och andra resurssnåla klienter måste synkronisera 13.6 MB data per år, och ladda ner ytterligare 3.7 KB för varje användarcertifikat som skall valideras.

This thesis presents a PoC for a Machine Learning based Integrated Business Forecasting tool in Integrated Business Planning (mature S&OP) environment for long-term and mid-term transportation volume forecasting for outbound supply flows as a case study.   To achieve this goal, the thesis provides a literature review which ensures the research gap presented by the research questions and scope. Later, the thesis introduces Sales and Operations Planning process, Machine Learning methods used in the study and the case study scope and the corresponding data minning scope. Following a mixed research strategy, a cause effect diagonis is presented and relevant business factors influencing the transportation volumes per lane are identified based on As-Is business process understanding achieved from interviews and internal and external documentations; which is further used to develop a conditional LSTM based machine learning time series forecasting model for transportation volume forecasting for five transportation lanes as PoC. Furthermore, a benchmark evaluation of the developed ML time series forecasting model with two other forecasting models (XGBoost and Extra Trees) is performed for accuracy and robustness performance metrics for long-term transportation volume forecast and also the performance of the developed ML forecasting model for the mid-term forecast is reported.  From the benchmark evaluation the proposed conditional LSTM model is proven to be a better balanced models in terms of maintaining acceptable level of forecasting accuracy and robustness. The Extra Trees model is the most accurate model with least robustness in forecasting across the five transportation lanes due to it’s inability to learn conditionally for each of the five transportation lanes.

Shareholder Registers provide vital information about ownership structures in corporations and are of interest for a diverse set of stakeholders such as the Swedish Companies Registration Office (and its international equivalences), stockholders, the SEC to name a few. Eventhough the information is public and the interest is high, transparency is limited. Blockchain technology offers a unique set of benefits that can help enhance transparency and security in shareholder registers. Therefore, this thesis aims to investigate how shareholder registers can benefit from blockchain technology by implementing a proof-of-concept and conducting a market analysis. The proof of concept consists of a small-scale implementation of a blockchain network with essential functionality meant to simulate a shareholder register. The market analysis was conducted through interviews with executives from several companies. There is good reason to believe blockchain technology has a future in shareholder registers. The decentralied nature of blockchain implies that it can be leveraged to provide security and transparency benefits that contemporary alternatives cannot. The Proof of concept proves that it can be done conceptually and the market analysis shows that there is demand for it that has not been filled by other alternatives. / Aktieböcker lagrar viktig information som berör aktiebolags ägarstrukturer och är av intresse för flertalet intressenter som Bolagsverket, aktieägare och Finansinspektionen för att nämna ett fåtal. Trots att aktieboken är en allmän handling och att intresset för den är så stort präglas aktieböcker av låg transparens. Blockkedjeteknik erbjuder en uppsättning unika egenskaper som kan bidra med ökad transparens och säkerhet för aktieägare. Detta kandidatarbete ämnar därför att undersöka hur blockkedjeteknik kan bidra till att göra aktieböcker bättre i detta avseende genom att genomföra ett koncepttest samt en marknadsanalys. Koncepttestet består av en småskalig implementation av ett blockkedjenätverk med grundläggande funktionalitet menat att simulera en aktiebok. Marknadsanalysen består av intervjuer genomförda med chefer från flera olika aktiebolag. Det finns goda skäl att tro på att blockkedjeteknik har en framtid inom aktieböcker. Blockkedjeteknikens decentraliserade natur medför möjligheter att förbättra säkerhet och transparens hos dagens aktieböcker. Arbetets koncepttest visar att det kan göras rent konceptuellt medan marknadsanalysen visar att det finns en efterfrågan som inte fyllts av andra alternativ.