Esta tese discute o papel da Análise Forense de Imagens como reguladora de mídia digital na sociedade. Isto inclui um estudo com mais de 400 indivíduos para determinar suas capacidades de detectar edições em imagens. Os resultados desse experimento indicam que humanos são facilmente enganados por imagens digitais, tendo dificuldades em diferenciar entre imagens pristinas e editadas. A tese então analisa a efetividade do arsenal de análise forense de imagens contra o estado-da-arte de composição de imagens. Através da análise de padrões fundamentais de imagens, as técnicas forenses são capazes de detectar a presença da maioria das operações de composição testadas. A tese então apresenta uma abordagem alternativa para análise forense de imagens, baseada na geração automática de planos. Ao tratar o processo de inspeção de uma imagem como um plano composto de múltiplos passos, propusemos uma arquitetura que é capaz de indicar os passos necessários para analisar uma imagem. Os planos são baseados em uma modelagem formal do conhecimento e técnicas forenses, de modo que possam ser traduzidos em passos a serem executados. A tese então demonstra que os limites de tal abordagem dependem da dificuldade de validar tal solução. Isso é uma consequência da natureza dos problemas de análise forense de imagens: essencialmente, são problemas de confiança distribuída entre indivíduos com acesso limitado à informação. Essa configuração é analisada de diferentes perspectivas em busca dos limites práticos para a análise forense de imagens digitais. Os resultados dessa análise sugerem que a área falha em produzir soluções acessíveis para a sociedade não por limitações técnicas, mas pela falta de um engajamento multi-disciplinar. A tese então discute como paradoxos filosóficos surgem naturalmente em cenários de análise forense de imagens. A análise forense de imagens digitais lida, essencialmente, com comunicação humana e, como tal, está sujeita a todas suas complexidades. Finalmente, é argumentado que o caminho para construir soluções úteis para a sociedade requer um esforço coletivo de diferentes disciplinas do conhecimento. É responsabilidade da comunidade forense desenvolver uma teoria epistemológica comum e acessível para este projeto coletivo. / This thesis discusses the role of Digital Image Forensics as a regulator of digital media in society. This includes a perceptual study with over 400 subjects to assess their ability to notice editing in images. The results of such experiment indicate that humans are easily fooled by digital images, not being able to tell apart edited and pristine images. The thesis then analyzes the effectiveness of the available arsenal of digital image forensics technology to detect image editing performed by state-of-the-art image-compositing techniques. By analyzing fundamental image patterns, forensics techniques can effectively detect the occurrence of most types of image compositing operations. In response to these two studies, the thesis presents an alternative approach to digital image forensics, based on automated plan generation. By treating the image inspection process as a plan comprised of different steps, it proposes an architecture that is able to guide an analyst choosing the next best step for inspecting an image. The generated plans are flexible, adapting on the fly to the observed results. The plans are based on a formal modelling of current forensics knowledge and techniques, so that they can be translated in steps to be executed. The thesis then shows that the limits of such an approach lie in the difficulty to validate results, which is a consequence of the setup of forensics problems: they are problems of distributed trust among parties with limited information. This scenario is analyzed from different perspectives in search for the practical limits of Digital Image Forensics as a whole. The results of such an analysis suggest that the field is lacking in providing practical and accessible solutions to society due to limited engagement in multidisciplinary research rather than due to limited technical proficiency. The thesis then discusses how paradoxes from philosophy, mathematics, and epistemology arise naturally in both real forensics scenarios, and in the theoretical foundations of the field. Digital Image Forensics ultimately deals with human communication and, as such, it is subject to all its complexities. Finally, it is argued that the path for providing useful solutions for society requires a collective engagement from different disciplines. It is the responsibility of the forensics community to develop a common, accessible epistemological framework for this collective enterprise.

Esta tese discute o papel da Análise Forense de Imagens como reguladora de mídia digital na sociedade. Isto inclui um estudo com mais de 400 indivíduos para determinar suas capacidades de detectar edições em imagens. Os resultados desse experimento indicam que humanos são facilmente enganados por imagens digitais, tendo dificuldades em diferenciar entre imagens pristinas e editadas. A tese então analisa a efetividade do arsenal de análise forense de imagens contra o estado-da-arte de composição de imagens. Através da análise de padrões fundamentais de imagens, as técnicas forenses são capazes de detectar a presença da maioria das operações de composição testadas. A tese então apresenta uma abordagem alternativa para análise forense de imagens, baseada na geração automática de planos. Ao tratar o processo de inspeção de uma imagem como um plano composto de múltiplos passos, propusemos uma arquitetura que é capaz de indicar os passos necessários para analisar uma imagem. Os planos são baseados em uma modelagem formal do conhecimento e técnicas forenses, de modo que possam ser traduzidos em passos a serem executados. A tese então demonstra que os limites de tal abordagem dependem da dificuldade de validar tal solução. Isso é uma consequência da natureza dos problemas de análise forense de imagens: essencialmente, são problemas de confiança distribuída entre indivíduos com acesso limitado à informação. Essa configuração é analisada de diferentes perspectivas em busca dos limites práticos para a análise forense de imagens digitais. Os resultados dessa análise sugerem que a área falha em produzir soluções acessíveis para a sociedade não por limitações técnicas, mas pela falta de um engajamento multi-disciplinar. A tese então discute como paradoxos filosóficos surgem naturalmente em cenários de análise forense de imagens. A análise forense de imagens digitais lida, essencialmente, com comunicação humana e, como tal, está sujeita a todas suas complexidades. Finalmente, é argumentado que o caminho para construir soluções úteis para a sociedade requer um esforço coletivo de diferentes disciplinas do conhecimento. É responsabilidade da comunidade forense desenvolver uma teoria epistemológica comum e acessível para este projeto coletivo. / This thesis discusses the role of Digital Image Forensics as a regulator of digital media in society. This includes a perceptual study with over 400 subjects to assess their ability to notice editing in images. The results of such experiment indicate that humans are easily fooled by digital images, not being able to tell apart edited and pristine images. The thesis then analyzes the effectiveness of the available arsenal of digital image forensics technology to detect image editing performed by state-of-the-art image-compositing techniques. By analyzing fundamental image patterns, forensics techniques can effectively detect the occurrence of most types of image compositing operations. In response to these two studies, the thesis presents an alternative approach to digital image forensics, based on automated plan generation. By treating the image inspection process as a plan comprised of different steps, it proposes an architecture that is able to guide an analyst choosing the next best step for inspecting an image. The generated plans are flexible, adapting on the fly to the observed results. The plans are based on a formal modelling of current forensics knowledge and techniques, so that they can be translated in steps to be executed. The thesis then shows that the limits of such an approach lie in the difficulty to validate results, which is a consequence of the setup of forensics problems: they are problems of distributed trust among parties with limited information. This scenario is analyzed from different perspectives in search for the practical limits of Digital Image Forensics as a whole. The results of such an analysis suggest that the field is lacking in providing practical and accessible solutions to society due to limited engagement in multidisciplinary research rather than due to limited technical proficiency. The thesis then discusses how paradoxes from philosophy, mathematics, and epistemology arise naturally in both real forensics scenarios, and in the theoretical foundations of the field. Digital Image Forensics ultimately deals with human communication and, as such, it is subject to all its complexities. Finally, it is argued that the path for providing useful solutions for society requires a collective engagement from different disciplines. It is the responsibility of the forensics community to develop a common, accessible epistemological framework for this collective enterprise.

abstract: Humans and robots need to work together as a team to accomplish certain shared goals due to the limitations of current robot capabilities. Human assistance is required to accomplish the tasks as human capabilities are often better suited for certain tasks and they complement robot capabilities in many situations. Given the necessity of human-robot teams, it has been long assumed that for the robotic agent to be an effective team member, it must be equipped with automated planning technologies that helps in achieving the goals that have been delegated to it by their human teammates as well as in deducing its own goal to proactively support its human counterpart by inferring their goals. However there has not been any systematic evaluation on the accuracy of this claim. In my thesis, I perform human factors analysis on effectiveness of such automated planning technologies for remote human-robot teaming. In the first part of my study, I perform an investigation on effectiveness of automated planning in remote human-robot teaming scenarios. In the second part of my study, I perform an investigation on effectiveness of a proactive robot assistant in remote human-robot teaming scenarios. Both investigations are conducted in a simulated urban search and rescue (USAR) scenario where the human-robot teams are deployed during early phases of an emergency response to explore all areas of the disaster scene. I evaluate through both the studies, how effective is automated planning technology in helping the human-robot teams move closer to human-human teams. I utilize both objective measures (like accuracy and time spent on primary and secondary tasks, Robot Attention Demand, etc.) and a set of subjective Likert-scale questions (on situation awareness, immediacy etc.) to investigate the trade-offs between different types of remote human-robot teams. The results from both the studies seem to suggest that intelligent robots with automated planning capability and proactive support ability is welcomed in general. / Dissertation/Thesis / Masters Thesis Computer Science 2015

abstract: Automated planning problems classically involve finding a sequence of actions that transform an initial state to some state satisfying a conjunctive set of goals with no temporal constraints. But in many real-world problems, the best plan may involve satisfying only a subset of goals or missing defined goal deadlines. For example, this may be required when goals are logically conflicting, or when there are time or cost constraints such that achieving all goals on time may be too expensive. In this case, goals and deadlines must be declared as soft. I call these partial satisfaction planning (PSP) problems. In this work, I focus on particular types of PSP problems, where goals are given a quantitative value based on whether (or when) they are achieved. The objective is to find a plan with the best quality. A first challenge is in finding adequate goal representations that capture common types of goal achievement rewards and costs. One popular representation is to give a single reward on each goal of a planning problem. I further expand on this approach by allowing users to directly introduce utility dependencies, providing for changes of goal achievement reward directly based on the goals a plan achieves. After, I introduce time-dependent goal costs, where a plan incurs penalty if it will achieve a goal past a specified deadline. To solve PSP problems with goal utility dependencies, I look at using state-of-the-art methodologies currently employed for classical planning problems involving heuristic search. In doing so, one faces the challenge of simultaneously determining the best set of goals and plan to achieve them. This is complicated by utility dependencies defined by a user and cost dependencies within the plan. To address this, I introduce a set of heuristics based on combinations using relaxed plans and integer programming formulations. Further, I explore an approach to improve search through learning techniques by using automatically generated state features to find new states from which to search. Finally, the investigation into handling time-dependent goal costs leads us to an improved search technique derived from observations based on solving discretized approximations of cost functions. / Dissertation/Thesis / Ph.D. Computer Science 2012

This thesis focuses on improving the process of automated planing through symmetry breaking. The aim is to describe symmetries, which are often observed by human programmers, but haven't been properly theoretically formalized. After an analysis of available research, there are new definitions of symmetries proposed in context of classical planning, such as state equivalence, T1 automorphisms and more general automorphisms of constants. Several theorems are proved about new symmetries. As a result, an algorithm for detecting a special symmetry class is proposed, together with a method of exploiting such class during planning. Experimens are made to show the effect of symmetry breaking on the performance of the planner. Powered by TCPDF (www.tcpdf.org)

The demand for collaborative, easy to use robots has increased during the last decades in hope of incorporating the use of robotics in smaller production scales, with easier and faster programming. Artificial intelligence (AI) and Machine learning (ML) are showing promising potential in robotics and this project has attempted to automatically solve a specific assembly task with Behavior trees (BTs). BTs can be used to elegantly divide a problem into different subtasks, while being modular and easy to modify. The main focus is put towards developing a Genetic algorithm (GA), that uses the fundamentals of biological evolution to produce BTs that solves the problem at hand. As a comparison to the GA result, a so-called Automated planner was developed to solve the problem and produce a benchmark BT. With a realistic physics simulation, this project automatically generated BTs that builds a tower of Duplo-like bricks and achieved successful results. The results produced by the GA showed a variety of possible solutions, a portion resembling the automated planner's results but also alternative, perhaps more elegant, solutions. As a conclusion, the approach used in this project shows promising signs and has many possible improvements for future research.

This licentiate thesis considers computer-assisted troubleshooting of complex products such as heavy trucks. The troubleshooting task is to find and repair all faulty components in a malfunctioning system. This is done by performing actions to gather more information regarding which faults there can be or to repair components that are suspected to be faulty. The expected cost of the performed actions should be as low as possible. The work described in this thesis contributes to solving the troubleshooting task in such a way that a good trade-off between computation time and solution quality can be made. A framework for troubleshooting is developed where the system is diagnosed using non-stationary dynamic Bayesian networks and the decisions of which actions to perform are made using a new planning algorithm for Stochastic Shortest Path Problems called Iterative Bounding LAO*. It is shown how the troubleshooting problem can be converted into a Stochastic Shortest Path problem so that it can be efficiently solved using general algorithms such as Iterative Bounding LAO*.  New and improved search heuristics for solving the troubleshooting problem by searching are also presented in this thesis. The methods presented in this thesis are evaluated in a case study of an auxiliary hydraulic braking system of a modern truck. The evaluation shows that the new algorithm Iterative Bounding LAO* creates troubleshooting plans with a lower expected cost faster than existing state-of-the-art algorithms in the literature. The case study shows that the troubleshooting framework can be applied to systems from the heavy vehicles domain.

Over the years, the Artificial Intelligence and Integrated Computer Systems (AIICS) Division at Linköping University has developed a high-level architecture for collaborative robotic systems that includes a delegation system capable of defining complex missions to be executed by a team of agents. This architecture has been used as a part of a research arena for developing and improving public safety and security using ground, aerial, surfaceand underwater robotic systems. Recently, the division decided to purchase a Boston Dynamics Spot robot to further progress into the public safety and security research area.The robot has a robotic arm and navigation functionalities such as map building, motion planning, and obstacle avoidance. This thesis investigates how the Boston Dynamics Spot robot can be integrated into the high-level architecture for collaborative robotic systems from the AIICS division. Additionally, how the robot’s functionalities can be extended so that it is capable of determining which actions it should take to achieve high-level behavioursconsidering its capabilities and current state. In this context, higher-level behaviours include picking up and delivering first aid supplies, which can be beneficial in specific emergency situations. The study was divided and done in an iterative approach.The system was tested in various scenarios that represent its intended future use. The result demonstrated the robot’s ability to plan and accomplish the desired high-level behaviours. However, there were instances when achieving the desired behaviours proved challenging due to various limiting factors, including limitations posed by the robot’s internal controller.

Student mobility in the area of Higher Education (HE) is gaining more attention nowadays. It is one of the cornerstones of the Bologna Process being promoted at both national and international levels. However, currently there is no technical system that would support student mobility processes and assist users in authoring educational curricula involving student mobility. In this study, the problem of student mobility programmes generation based on existing modules and programmes is considered. A similar problem is being solved in an Intelligent Tutoring Systems field using Curriculum generation techniques, but the student mobility area has a set of characteristics limiting their application to the considered problem. One of main limiting factors is that mobility programmes should be developed in an environment with heterogeneous regulations. In this environment, various established routines and regulations are used to control different aspects of the educational process. These regulations can be different in different domains and are supported by different authors independently. In this thesis, a novel framework was developed for generation of student mobility programmes in an environment with heterogeneous regulations. Two core technologies that were coherently combined in the framework are hierarchical planning and policy-based management. The policy-based planner was designed as a central engine for the framework. It extends the functionality of existing planning technologies and provides the means to carry out planning in environments with heterogeneous regulations, specified as policies. The policy-based planner enforces the policies during the planning and guarantees that the resultant plan is conformant with all policies applicable to it. The policies can be supported by different authors independently. Using them, policy authors can specify additional constraints on the execution of planning actions and extend the pre-specified task networks. Policies are enforced during the planning in a coordinated manner: situations when a policy can be enforced are defined by its scope, and the outcomes of policy evaluation are processed according to the specially defined procedures. For solving the problem of student mobility programme generation using the policy-based planner, the planning environment describing the student mobility problem area was designed and this problem was formalised as a planning task. Educational processes valid throughout the HE environment were formalised using Hierarchical Task Network planning constructs. Different mobility schemas were encoded as decomposition methods that can be combined to construct complex mobility scenarios satisfying the user requirements. New mobility programmes are developed as detailed educational processes carried out when students study according to these programmes. This provides the means to model their execution in the planning environment and guarantee that all relevant requirements are checked. The postponed policy enforcement mechanism was developed as an extension of the policy-based planner in order to improve the planning performance. In this mechanism, future dead-ends can be detected earlier during the planning using partial policy requests. The partial policy requests and an algorithm for their evaluation were introduced to examine policies for planning actions that should be executed in the future course of planning. The postponed policy enforcement mechanism was applied to the mobility programme generation problem within the descending policy evaluation technique. This technique was designed to optimise the process of programme components selection. Using it, policies for different domains can be evaluated independently in a descending order, gradually limiting the scope for the required component selection. The prototype of student mobility programme generation solution was developed. Two case studies were used to examine the process of student mobility programmes development and to analyse the role of policies in this process. Additionally, four series of experiments were carried out to analyse performance gains of the descending policy evaluation technique in planning environments with different characteristics.

The aim of this thesis is to explore the potential of resolution-based methods for linear temporal reasoning. On the abstract level, this means to develop new algorithms for automated reasoning about properties of systems which evolve in time. More concretely, we will: 1) show how to adapt the superposition framework to proving theorems in propositional Linear Temporal Logic (LTL), 2) use a connection between superposition and the CDCL calculus of modern SAT solvers to come up with an efficient LTL prover, 3) specialize the previous to reachability properties and discover a close connection to Property Directed Reachability (PDR), an algorithm recently developed for model checking of hardware circuits, 4) further improve PDR by providing a new technique for enhancing clause propagation phase of the algorithm, and 5) adapt PDR to automated planning by replacing the SAT solver inside with a planning-specific procedure. We implemented the proposed ideas and provide experimental results which demonstrate their practical potential on representative benchmark sets. Our system LS4 is shown to be the strongest LTL prover currently publicly available. The mentioned enhancement of PDR substantially improves the performance of our implementation of the algorithm for hardware model checking in the multi-property...