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 the present PhD thesis an optimal problem suite is proposed as benchmark for the test of numerical solvers. The problems are divided in four categories, classic, singular, constrained and hard problems. Apart from the hard problems, where it is not possible to give the analytical solution but only some details, all other problems are supplied with the derivation of the solution. The exact solution allows a precise comparison of the performance of the considered software. All of the proposed problems were taken from published papers or books, but it turned out that an analytic exact solution was only rarely provided, thus a true and reliable comparison among numerical solvers could not be done before. A typical wrong conclusion when a solver obtains a lower value of the target functional with respect to other solvers is to claim it better than the others, but it is not recognized that it has only underestimated the true value. In this thesis, a cutting edge application of optimal control to vehicles is showed: the optimization of the lap time in a race circuit track considering a number of realistic constraints. A new algorithm for path planning is completely described for the construction of a quasi G2 fitting of the GPS data with a clothoid spline in terms of the G1 Hermite interpolation problem. In particular the present algorithm is proved to work better than state of the art algorithms in terms of both efficiency and precision.

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.

The lack of generality is a structural weakness of knowledge representation formalisms. Here by lack of generality we mean the inability of any given representation to describe the infinite richness and diversity of the world and also its potentially infinite descriptions which are enabled by language. This lack of generality is the main cause of many of the difficulties encountered so far, just think of the problems which have arisen in the effort of creating reusable ontologies. In this thesis we propose a solution to the problem of generality which is based on the key idea that knowledge should not be modeled a priori, at design time, but it should continuously generated, adapted and evolved, from generation to usage. The thesis provides four main contributions: (i) a shared terminology for the characterization of concepts and for their computational representation; (ii) a formalization of the distinction between substance concepts and classification concepts; (iii) the integration of these two notions of concept into a general representation language that organizes them into a hierarchy of increasing abstraction of what is perceived, and (iv) a two-layered knowledge representation formalism, where the first layer allows to represent concepts, as the main devices for achieving generality, and where the second layer allows to represent concepts as the result of “adapting†a description to the current knowledge representation needs and requirements.

Covenants are an important part of financial contracts, that are used for resolving the conflicts of interest between borrowers and lenders. In more formal way covenants can be determined as special provisions in loans that give lenders the possibility of putting certain actions in force (normally early repayment) when covenants are violated. For instance, a covenant may restrict the company in taking additional credit, or require a firm to maintain certain financial ratios, such as leverage, coverage, liquidity ratios, etc. Our study develops a theoretical framework that allows to determine the covenant strength index that should be included in a debt contract in a way that minimizes expected losses for a bank subject to the rising restructuring costs. This optimal covenant is found in order to better allocate control rights ex ante and to minimize the costs of renegotiations for both parties. The approach that explores dynamic contingent claim models is applied to the prob- lem. This approach was pioneered by Black and Scholes (1973) and Merton (1974), and extended by Black and Cox (1976). The dynamics of the optimal covenant strength with respect to various model parameters is investigated. Different modifications to the initial model are considered which are important in exploring more realistic model setting. First of all, we introduce the concept of deadweight costs of distress or firesale price. The concept of deadweight losses imply that the debt holder gets some fraction of the asset value on default instead of the fundamental asset value (Das and Kim, 2015). Along with the concept of deadweight costs, the notion of firesale price is used, that represents the price at which the asset can be sold before the contract maturity. We explore how this extension of our baseline dynamic model influence the optimal level of covenant strictness in debt contracts. We further develop a model of an optimal covenant in bank loans with information asymmetry. Asymmetric information as a source of agency problems is very important in studying control rights in financial contracting. The conclusions of the papers on information asymmetry regarding control rights allocation and covenant strictness are often ambiguous. Different papers demonstrate more or less control rights of lenders or greater or lesser strictness of covenants depending on the setting and model parameters. Our model is unique in a sense that it unites different implications of empirical and theoretical models with information asymmetry and reflects both perspectives. We also introduce a framework for accessing the consequences of covenant violation in Monte Carlo simulation. Our simulation model allows us to measure different risk- parameters of a project, such as the probability of covenant violation and the probability of repayment of the loan. The measurements (average number of covenant violations per contract, frequency of covenant violation, frequency of loan repayment) can be used in implementation of different rules for a bank that extends the traditional risk-analysis of a project. Moreover, we implement a recursive technique for determining the level of covenant strength that allows the bank to maintain the performance of a specific risk- parameter. We employ a dynamic approach in the spirit of Borgonovo and Gatti (2013); Chang and Lee (2013); Liang et al. (2014) by simulating project value paths over time.

About three quarters of human emerging infectious diseases are caused by zoonotic pathogens, and many of them are spread by vectors such as mosquitoes. Mathematical models nowadays represent very powerful tools to make investigations and predictions for biological dynamical systems, providing helpful insights that can be extremely valuable for several aims. In this thesis, we will focus on a particular mosquito-borne zoonosis, West Nile virus (WNV), a flavivirus of emerging public health relevance in Europe and North America, and its main European vector, Culex pipiens mosquitoes. As the transmission of mosquito-borne diseases is largely driven by the abundance of the vector, to design appropriate control strategies it is crucial to understand the population dynamics of existing vector populations and evaluate how it depends on biotic and environmental factors. This thesis presents some new mathematical models that provide insights on several aspects of mosquito population dynamics by using different statistical and computational approaches, including for instance Linear Models and Markov chain Monte Carlo technique. Specifically, they aim to study the effect of biotic and abiotic factors on Cx. pipiens dynamics by using adult mosquito trapping data, gathered over several years in Northern Italy, to feed theoretical models. Furthermore, the effects of host competition and vector feeding preferences on the dynamics of a vector-borne infection (such as WNV) are investigated through a more theoretical study.

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.

No description available.

In an optimal visiting problem, we want to control a trajectory that has to pass as close as possible to a collection of target points or regions. We introduce a hybrid control-based approach for the classic problem where the trajectory can switch between a group of discrete states related to the targets of the problem. The model is subsequently adapted to a mean-field game framework, that is when a huge population of agents plays the optimal visiting problem with a controlled dynamics and with costs also depending on the distribution of the population. In particular, we investigate a single continuity equation with possible sinks and sources and the field possibly depending on the mass of the agents. The same problem is also studied on a network framework. More precisely, we study a mean-field game model by proving the existence of a suitable definition of an approximated mean-field equilibrium and then we address the passage to the limit.