Autonomous systems must be able to detect and promptly react to faults. Fault Detection and Identification components (FDI) are in charge of detecting the occurrence of faults. The FDI depends on the concrete design of the system, needs to take into account how faults might interact, and can only have a partial view of the run-time state through sensors. For these reasons, the development of the FDI and certification of its correctness and quality are difficult tasks. This difficulty is compounded by the fact that current approaches for verification of the FDI rely on manual inspection and testing. Motivated by industrial case-studies from the European Space Agency, this thesis proposes a formal foundation for FDI design that covers specification, validation, verification, and synthesis. The Alarm Specification Language (ASLk) is introduced in order to formally capture a set of interesting and desirable properties of the FDI components. ASLk is equipped with a semantics based on Temporal Epistemic Logic, thus enabling reasoning about partially observable systems. Automated reasoning techniques can then be applied to perform validation, verification, and synthesis of the FDI. This formal process guarantees that the generated FDI satisfies the designer expectations. The problems deriving from this process were out of reach for existing model-checking techniques. Therefore, we develop novel and efficient techniques for model-checking temporal epistemic logic over infinite state systems.

Any form of model-based reasoning is limited by the adherence of the model to the actual reality. Scheduling is the problem of finding a suitable timing to execute a given set of activities accommodating complex temporal constraints. Planning is the problem of finding a strategy for an agent to achieve a desired goal given a formal model of the system and the environment it is immersed in. When time and temporal constraints are considered, the problem takes the name of temporal planning. A common assumption in existing techniques for planning and scheduling is controllability of activities: the agent is assumed to be able to control the timing of starting and ending of each activity. In several practical applications, however, the actual timing of actions is not under direct control of the plan executor. In this thesis, we focus on this temporal uncertainty issue in scheduling and in temporal planning: we propose to natively express temporal uncertainty in the model used for reasoning. We first analyze the state-of-the-art on the subject, presenting a rationalization of existing works. Second, we show how Satisfiability Modulo Theory (SMT) solvers can be exploited to quickly solve different kinds of query in the realm of scheduling under uncertainty. Finally, we address the problem of temporal planning in domains featuring real-time constraints and actions having duration that is not under the control of the planning agent.

In this work we provided a contribution in the specific context of verbal humor generation, focused on computational creation of humorous texts. The goal consisted of the design and implementation of a tool for the automatic generation of short humorous expressions. We focused on humorous puns generated through the variation of familiar expressions, performed via lexical substitution. Phonetic and semantic features are employed to select the appropriate substitution. We have chosen a corpus-based approach, in line with a tendency prevailing in the computational linguistics field. A number of textual corpora and dictionaries were employed. We have developed some of these resources (WordNet-Affect and Affective-Weight) in an early stage of the research. The system can be used as a testbed for the empirical investigation of various aspects of verbal humor. More specifically, it can be used to study the correlation between linguistic parameters of humorous expressions and appraisal dimensions that are part of the cognitive process of humor understanding. In the last phase of the work, we developed two exploratory applications: a prototype was developed as a first component of a system in which task-oriented assistance and humorous feedback can be integrated to achieve frustration reduction. The other application developed is a tool for the collaborative creation of puns. In this system, the pun generator is integrated with a graphical user interface based on a dynamic graph, helping the exploration of different creative solutions.

Formal methods are becoming increasingly important for debugging and verifying hardware and software systems, whose current complexity makes the traditional approaches based on testing increasingly-less adequate. One of the most promising research directions in formal verification is based on the exploitation of Satisfiability Modulo Theories (SMT) solvers. In this thesis, we present MathSAT, a modern, efficient SMT solver that provides several important functionalities, and can be used as a workhorse engine in formal verification. We develop novel algorithms for two functionalities which are very important in verification -- the extraction of unsatisfiable cores and the generation of Craig interpolants in SMT -- that significantly advance the state of the art, taking full advantage of modern SMT techniques. Moreover, in order to demonstrate the usefulness and potential of SMT in verification, we develop a novel technique for software model checking, that fully exploits the power and functionalities of the SMT engine, showing that this leads to significant improvements in performance.

Every human being is familiar to the experience of reminiscence: recalling and revisiting our past memories. We reminisce to create our identities. We reminisce to maintain our relationships. We reminisce to review our lives. And we also reminisce together. This dissertation develops around the topic of how IT stimulates reminiscence, motivated by its proven benefits in peopleâ s well-being and its prevalence across all stages of life. The focus is set on older adults, with the overall goal of fostering intergenerational social interactions (that is, interactions between older adults and younger generations). This thesis is motivated by the current interest on active ageing as an emergent way of life, with better and more opportunities for health, participation and security. As the world ageing population continues to increase and the average life expectancy of people increasing every year, there is a growing need for understanding the ageing phenomena, and particularly, for designing human centered information technologies (IT) that enhance opportunities of social participation as people age. Within this scenario, this dissertation addresses the following research questions using a participatory approach to research and design: (i) what is the role of IT in enabling a more happy and active ageing?; (ii) in doing so, how can IT stimulate intergenerational social interactions?, and (iii) can IT-supported social reminiscence facilitate these interactions and make of them an enjoyable experience?. To answer these questions, we leverage upon a participatory action research approach to gain an understanding of the topic, moving later to the participatory design of IT for social reminiscence and finally, evaluating how IT supports the practice of social reminiscence in a face-to-face intergenerational context. The contributions of this dissertation can be summarized as follows: - Knowledge: an understanding of what role IT can play in supporting, stimulating and accompanying active ageing and social interactions through the practice of reminiscence. - Model: a conceptual model of the different stages of IT-supported social reminiscence sessions, and an extended model of the design spaces for intergenerational engagement. - System: an exemplary socio-technical system that fits the aforementioned roles, including a knowledge base and algorithms to support contextual stimulation of reminiscence, using multimedia resources that are publicly available on the web. - Evaluation: quantitative and qualitative results obtained from observing the use of our system in a real intergenerational context.

Formal methods are becoming increasingly important for debugging and verifying hardware and software systems, whose current complexity makes the traditional approaches based on testing increasingly-less adequate. One of the most promising research directions in formal verification is based on the exploitation of Satisfiability Modulo Theories (SMT) solvers. In this thesis, we present MathSAT, a modern, efficient SMT solver that provides several important functionalities, and can be used as a workhorse engine in formal verification. We develop novel algorithms for two functionalities which are very important in verification -- the extraction of unsatisfiable cores and the generation of Craig interpolants in SMT -- that significantly advance the state of the art, taking full advantage of modern SMT techniques. Moreover, in order to demonstrate the usefulness and potential of SMT in verification, we develop a novel technique for software model checking, that fully exploits the power and functionalities of the SMT engine, showing that this leads to significant improvements in performance.

This thesis introduces SKOs (Scientific Knowledge Object) a specification for capturing the knowledge and artifacts that are produced by the scientific research processes. Aiming to address the current existing limitations of scientific production this specification is focused on reducing the work overhead of scientific creation, being composable and reusable, allow continuous evolution and facilitate collaboration and discovery among researchers. To do so it introduces four layers that capture different aspects of the scientific knowledge: content, meaning, ordering and visualization.

Access to geographic information has radically changed in the past decade. Previously, it was a specific task, for which complex desktop Geographic Information Systems (GISs) were built, and geographic data was maintained locally, managed by a restricted number of technicians. With the significant impact of the world-wide-web, an increasing number of different geographic services became available from heterogeneous sources. To support interoperability among different providers and users, GIS agencies have started to adopt Spatial Data Infrastructure (SDI) models. Usually, each SDI service provider publishes and gathers geographic information based on its background knowledge. Hence, discovering, chaining, and using services require a semantic interoperability level between different providers. This problem is typically referred as the need for 'semantic interoperability among autonomous and heterogeneous systems' and it is a challenge for current SDIs, due to their distributed architecture. This thesis provides a framework to approach the semantic heterogeneity problem in the field of geo-services - services that deal with the generation and management of geographical information - among distributed SDIs. The framework is based on: (i) a peer-to-peer (P2P) view of the semantics of web service coordination, implemented by using the OpenKnowledge system and (ii) the use of a specific semantic matching solution called Structure Preserving Semantic Matching (SPSM). SPSM is a basic module of OpenKnowledge as it enables web service discovery and integration by using semantic matching between invocations of web services and web service descriptions. We applied the OpenKnowledge system on a realistic emergency response scenario and selected SDI services. We modeled an emergency response scenario, i.e., a potential flooding event in the area of Trento. The scenario is based on the past experience and actual emergency plans as collected from interviews with personnel of the involved institutions and from related documents. Within this emergency response scenario a detailed implementation of selected SDI services is presented, namely the gazetteer, map and download services. The SPSM solution has been assessed on a set of GIS ESRI ArcWeb services. Two kinds of experiments have been conducted: the first experiment includes matching of original web service signatures with synthetically altered ones. In the second experiment a manual classification of the GIS dataset has been compared to the unsupervised one produced by SPSM. The evaluation results demonstrate robustness and good performance of the SPSM approach on a large (ca. 700.000) number of matching tasks. In the first experiment a high overall matching relevance quality (F-measure) was obtained (over 55%). In the second experiment the best F-measure value exceeded 50% for the given GIS operations set. SPSM performance is good, since the average execution time per matching task was 43 ms. This suggests that SPSM could be employed to find similar web service implementations at runtime. The aforementioned results suggest the practical real time application of the SPSM approach to: (i) discovering geo-services from specific geographic information catalogs, (ii) composing specific geo-processing services, (iii) supporting coordination of geo-sensor networks, and (iv) supporting geo-data discovering and integration.

The use of intelligent presentation systems within a museum is a well-established practice. This thesis deals with connecting the museum experience with novel cultural experiences in the outside world, with attention to the individual in recognizing opportunities and delivering tailored presentations. Our goal is to help keep the user connected to the cultural experience and to help develop further knowledge and intellectual pleasure after the museum visit. The specific goal of this research is to explore the potential of technology 1) to define contextual opportunities†, 2) to identify these contextual opportunities, 3) to select relevant material, and 4) to deliver it, given the right context, in the most appropriate way for the specific user. We review the field of personalized cultural heritage experience and technology, and related research areas, needed to serve as a grounded basis for ideas developed in the framework. We examine user preferences by reviewing data from two surveys, we conducted, in order to develop additional (from those in the background) inputs (points) for the theoretical framework model. We then describe our theoretical frameworks, both finding the next place to go, and connecting back to previous experiences. We describe the System Architecture and give three concrete examples of use cases. We report on an initial evaluation of the system (and the underlying theoretical framework) by a visitor study, followed by a discussion of possible implications.

This doctoral thesis presents a comprehensive exploration of ultrawideband technology in addressing diverse challenges within localization systems. Beginning with the development of an innovative, cost-effective, and anonymous contact tracing solution for industrial environments during the COVID-19 pandemic, the research integrates ultra-wideband positioning, Bluetooth low-energy, and inertial measurement units. The subsequent sections delve into relative positioning systems, device-free localization, UWB bistatic radar sensors, and UAV-based tracking, showcasing novel methodologies and hardware implementations with promising outcomes. The work extends to groundbreaking approaches in deploying UWB infrastructure through self-deployable robots and cooperative positioning schemes using a UAV swarm. The contributions highlight versatility, costeffectiveness, and scalability, opening new possibilities for applications in security, logistics, IoT services, and space exploration. In summary, this thesis represents a significant advancement in localization systems, offering practical solutions and paving the way for future research and applications