Tesis Doctorals - Departament - Matemàtiques i Informàtica

URI permanent per a aquesta col·leccióhttps://hdl.handle.net/2445/99760

Estadístiques

Examinar

Mostrant 1 - 20 de 60

Deep Learning Approaches for Human Activity Understanding
(Universitat de Barcelona, 2025-06-12) Zhang, Zejian; Escalera Guerrero, Sergio; Palmero Cantariño, Cristina; Universitat de Barcelona. Departament de Matemàtiques i Informàtica
[eng] Understanding human activities is crucial for developing practical applications that benefit society. Temporal action localization (TAL) in untrimmed videos is one of the most challenging tasks in this field. While significant progress has been made over the years, the methods developed are still far from being suitable for real-world use, and TAL remains an ongoing challenge. This thesis aims to address this challenge task through three contributions. First, we propose a dual hierarchical model capable of extracting and fusing both local, fine-grained boundary details and broader, high-level semantic contexts for TAL. In this method, the second hierarchical design enables the model to uncover actions of varying durations, leveraging the features learned from the first hierarchy. Our findings show that fusing temporal contexts at different scales is essential for precise TAL. In this approach, the model utilizes the self-attention mechanism in Transformer encoders. However, due to the quadratic complexity of self-attention, methods relying on it may struggle to handle real-world-length videos. Next, we present a comprehensive experimental comparison to determine which temporal feature encoder should be selected under different conditions. We analyzed 12 models, equipped with pure Transformer encoders, pure Mamba Blocks, and combinations of both into a unified encoder for TAL. The experimental results suggest that the choice of encoder depends heavily on the specific dataset. Nevertheless, the pure Mamba Block emerges as the preferred option for unknown datasets due to its performance and lower complexity. Finally, we introduce UDIVA-HHOI, a novel large-scale audio-visual dyadic human-human-object interaction dataset. This dataset provides rich, extremely short-duration and concurrent actions, featuring both low-level physical actions and high-level goal-oriented actions and the objects involved in these actions—elements not typically represented in commonly used TAL benchmarks. UDIVA-HHOI opens up new possibilities for addressing the detection of complex interactive actions in real-world scenarios. Our preliminary study confirms its potential, and our analysis also offers recommendations for selecting an appropriate feature encoder for future research on this new benchmark, with the Mamba Block being the preferred choice.
Bridging Natural Language and Hierarchical Multivariate Data Visualisation to Support Data Analysis
(Universitat de Barcelona, 2025-04-23) Kavaz, Ecem; Rodríguez Santiago, Inmaculada; Puig Puig, Anna; Universitat de Barcelona. Departament de Matemàtiques i Informàtica
[eng] Tracking and analysing the vast amounts of data generated from social networks and digital platforms presents important challenges, not only due to the overwhelming volume but also the complex relationships embedded within the data. This thesis addresses these challenges through data visualisation techniques, focusing on hierarchical and multivariate data, where visual clutter and effective use of space are key concerns. Furthermore, the rise of Visual Natural Language Interfaces (V-NLIs), also referred to in this thesis as VisChatbots, offers new opportunities to facilitate the interaction with data visualisations via natural language. This thesis contributes to the fields of Hierarchical Multivariate Data Visualisation and Visualisation-oriented Natural Language Interfaces. Specifically, we introduce a novel categorization algorithm to classify hierarchical data, from which we propose the most suitable visual designs for their visualisation. Additionally, we propose a new incremental design methodology for Vis-Chatbots, called VisChat. This structured approach guides the development of chatbots integrated into visualisation platforms, establishing smooth communication among stakeholders—end users, designers, and developers—and introducing new design artefacts, such as the VisAgent persona, visualisation conversation patterns, and conversational transcripts that help guide and validate the design of the VisChatbot. Following the VisChat methodology, we have integrated a VisChatbot into a platform for visualising hierarchical and multivariate data. To validate our proposal, we present a case study on the analysis of hate speech in online news articles, where the suitability of the proposed visualisations was evaluated, as well as the capability of the visualisation chatbot to enable users to easily explore and understand, through Natural Language interactions, both the structural relationships and the feature-based relationships within the data. In conclusion, this thesis not only advances data visualisation techniques for multivariate hierarchical data but also establishes a framework for integrating natural language interfaces intov isual analysis platforms, thereby promoting a more efficient and effective analysis of data.
Large and iterated finite group actions on aspherical manifolds
(Universitat de Barcelona, 2025-07-11) Daura Serrano, Jordi; Mundet i Riera, Ignasi; Universitat de Barcelona. Departament de Matemàtiques i Informàtica
[eng] Finite transformation group theory investigates the finite symmetries of topological objects, such as manifolds or CW-complexes. In this thesis, we focus on actions on closed topological manifolds and adopt the following approach: instead of directly studying the action properties of a finite group G to a manifold M, we focus on the properties of action restricted to certain subgroups H of bounded index. Several problems align with this philosophy, such as determining whether the group of homeomorphisms of a manifold is Jordan, calculating the discrete degree of symmetry of a manifold, determining whether a manifold is quasi-asymmetric, and studying the number and size of isotropy subgroups for finite group actions on manifolds. In the first part of the thesis, we provide solutions to these problems for two general classes of manifolds, namely: (1) Closed, connected and aspherical manifolds, whose fundamental group has a group of external Minkowski automorphisms (a group G is Minkowski if there exists a constant C such that every finite subgroup H of G has order at most C). (2) Closed, connected and orientable manifolds that admit a non-zero degree application to a nilmanifold. We show that the group of external automorphisms of a lattice of a connected Lie group is Minkowski, which allows us to apply our results to locally homogeneous aspherical closed manifolds. In addition, we provide the earliest known examples of manifolds M and M' with isomorphic cohomology rings such that Homeo(M) is Jordan but Homeo(M') is not. We establish two stiffness results for the discrete degree of symmetry: if M is a closed, connected, aspherical manifold and the external automorphism group of the fundamental group of M is Minkowski, or if M admits a non-zero degree application to a nilmanifold and its fundamental group is virtually solvable, then M is homeomorphic to a torus if its discrete degree of symmetry is equal to the dimension of M. In the second part, we refine the concept of group actions to explore in greater depth the topological and cohomology rigidity of closed and connected manifolds. This framework allows us to analyze in more detail the structure of closed aspherical manifolds and those that admit a non-zero degree application to a nilmanifold. We define new invariants, such as the iterated length of a manifold, which is closely related to its self-coatings, and introduce a refined version of the discrete degree of symmetry, called the discrete degree of iterate symmetry. We show that if M is a closed, oriented manifold that admits a non-zero degree application to a nilmanifold of nilpotency class 2, and both manifolds have the same discrete degree of iterated symmetry, then the rational cohomology of M is isomorphic to that of the nilmanifold. Furthermore, if the fundamental group of M is virtually solvable, then M is homeomorphic to the nilmanifold. We also prove that if M is a locally homogeneous closed aspherical manifold with a discrete degree of iterated symmetry equal to its dimension, then M is homeomorphic to a nilmanifold of nilpotency class 2.
Periodic boundary points for transcendental Fatou components
(Universitat de Barcelona, 2025-09-18) Jové Campabadal, Anna; Fagella Rabionet, Núria; Universitat de Barcelona. Departament de Matemàtiques i Informàtica
[eng] This thesis is framed in the field of Complex Dynamics, which studies discrete dynamical systems generated by the iteration of holomorphic functions. More precisely, given a transcendent, integer or meromorphic function, we consider the discrete dynamical system generated by it. Then the complex plane is divided into two totally invariant sets: the Fatou set, where the dynamics are stable; and Julia's ensemble, its complement, where the dynamics are chaotic. The Fatou set is open and generally has infinite related components, called Fatou components, and they are periodic, pre-periodic, or wandering. One of the basic results in Complex Dynamics (demonstrated by Fatou and Julia for rational functions) is that the Julia set is the closure of the repulsing periodic points of the function. This result was generalized by Baker by integer functions, and by Baker, Kotus, and Lü by transcendent meromorphic functions. We note that, given an invariant Fatou component, then its boundary is an invariant closed subset of the Julia set. So, the next question arises naturally: given a meromorphic function, and it is a periodic Fatou component, are the periodic points dense at their boundary? Note that, although the periodic points are dense in the Julia set, a priori they could accumulate at the boundary from its complement, without being at the boundary For example, if the Fatou component is a rotation domain with a locally connected boundary, then there is no periodic point. However, F. Przytycki and A. Zdunik showed that, by rational functions, rotation domains (i.e. Siegel's disks and Herman's rings) are the only exceptions for which the periodic points are not dense at the boundary. In particular, they gave a positive answer to the previous question for attraction or parabolic basins of rational functions. The work of F. Przytycki and A. Zdunik already shows us that the answer to such an elementary question is far from simple. Indeed, an exhaustive study of the boundaries of such Fatou components (which may not be locally connected) is necessary, combining tools of dynamics, measurement theory and conformal analysis. In the particular case of simply connected attraction basins, the proof is based on the properties of the function at the boundary from the point of view of the theory of measurement and Lyapunov's exponents, as well as precise estimates of the distortion of the Riemann application and the finite Blaschke products in the unit circle, and Pesin's theory conforms. For components of Fatou not limited to transcendent functions, the situation is even more delicate, due to the presence of the essential singularity, and most of the above techniques cannot be applied. Moreover, since the boundary of the Fatou component is not compact, it is not compact, nor is the existence of periodic points on the boundary evident. In view of the above questions, and the existing previous work to understand the boundaries of transcendent Fatou components, the following conjecture naturally arises, which is a large open problem in transcendent dynamics. Let it be a meromorphic function, and let it be a simply connected periodic Fatou component, such that it is not univalent. Then, there is a periodic point on the border of such a component of Fatou. In addition, if it is an attractor or parabolic basin, or a doubly parabolic Baker domain, then the periodic points are dense at the boundary. This thesis should be understood as significant progress in proving the above conjecture. Indeed, we demonstrate the existence and density of periodic points at the boundary of Fatou components under very weak hypotheses in the postsingular set, together with additional results in relation to boundary dynamics, escape points and accessibility. During the thesis, new techniques have been demonstrated, such as estimates in the distortion of internal functions and Pesin's theory for transcendent functions.
Flow map parameterization methods for invariant tori in Hamiltonian systems
(Universitat de Barcelona, 2025-06-05) Fernández-Mora, Álvaro; Haro, Àlex; Mondelo González, José María; Universitat de Barcelona. Departament de Matemàtiques i Informàtica
[eng] Given a dynamic system, it is important to identify the invariant objects that organize long-term behavior, as well as their dynamic connections. Both in theory and in applications. The objective of this thesis is to advance in the development of Kolmogorov-Arnold-Moser (KAM) type techniques within the framework of the parameterization method and its application to problems of celestial mechanics. We have developed KAM iterative schemes for the calculation of partially hyperbolic invariant torus and their invariant bundles in quasiperiodic Hamiltonian systems. We look for invariant bulls and bundles under adequate time-1 maps, which allow us to reduce the dimension of the bull to be calculated by one. The computational cost of manipulating functions grows exponentially with the number of variables in the parameterization. Therefore, reduction by flow maps is computationally advantageous, although it requires numerical integration. However, this integration can be easily parallelized. If the parameterization is approximated with N Fourier coefficients, the iterative step requires O(N) of storage and O(N log N) operations, in contrast to standard Newtonian methods, which need O(N^2) of storage and O(N^3) operations. This gain in efficiency comes from the geometric properties of phase space (i.e., symplectic geometry), systems (symplectic accuracy), torus (isotropy, Lagrangianity), as well as dynamical properties (reducibility). In particular, the reducibility of the linearized dynamics around the torus to a triangular matrix by blocks is known as automatic reducibility and is an important property both in theory and in applications. The algorithms have been implemented and applied to the Three-Body Elliptic Restricted Problem (ERTBP) to compute an extensive set of non-resonant three-dimensional invariant torus along with their invariant bundles. From these results, we have obtained an a posteriori theorem for partially hyperbolic invariant bulls and their rank 1 invariant bundles in quasiperiodic Hamiltonian systems. The approach followed allows the theorem to be applied to autonomous, periodic and quasiperiodic Hamiltonian systems, and constitutes the demonstration of the convergence of methods based on flow maps. In addition, we simultaneously obtain both stable and unstable bundles, providing a clear geometric view of the tangent space to the torus. The proof is based on geometric properties of a symplectic nature, which hold approximately when the parameterizations approximately satisfy their equations of invariance. We have obtained geometric lemmas that control error in the KAM iterative process. The new error in the invariance equations is controlled with explicit constants, which requires a careful treatment of the loss of analyticity at each iterative step. The demonstration concludes by obtaining convergence conditions for the KAM iterative process. The a posteriori theorem obtained allows computer-aided proofs to be carried out. Partially hyperbolic bulls have associated stable and unstable varieties, whiskers, where dynamics converge exponentially fast in the future and in the past, respectively. The stable and unstable bundles with the linear approximations of these varieties. We have also developed KAM schemes to compute high-order Fourier-Taylor expansions of whiskers in autonomous and quasiperiodic Hamiltonian systems. Unlike order-to-order methods, which first calculate the torus and its bundles before calculating the whiskers on an order-by-order basis, the approach followed simultaneously computes both the torus and the whiskers using the same KAM iterative method. This unified framework improves the efficiency of whisker calculation by doubling the number of correct terms in expansion in each iteration. The algorithms have been applied to the calculation of high-order expansions of partially hyperbolic non-resonant invariant torus in the circular and three-body elliptical constrained problems.
Boosting the Artificial Intelligence solutions training phase by means of process simulation methods
(Universitat de Barcelona, 2025-05-13) Abió Rojo, Albert; Pujol Vila, Oriol; Bonada Bo, Francesc; Universitat de Barcelona. Departament de Matemàtiques i Informàtica
[eng] Despite the emergence of Industry 4.0 and the rise of a data-driven manufacturing paradigm, the acquisition of valuable data in a cost-efficient and sustainable manner for manufacturing processes remains a challenge for many companies. Conducting non-productive tests on the production line in an industrial plant result in a waste of raw materials, energy, human resources, and time. Furthermore, executing high fidelity manufacturing simulations entails a significant temporal and computational burden. Consequently, these drawbacks hinder the creation of knowledge in manufacturing processes and the development of technologies that aim to enhance and influence in the process performance, such as optimization or AI-based tools. This is especially critical for tools that benefit from the availability of large volumes of data and real-time responses, like Digital Twins and Reinforcement Learning agents. Therefore, it is necessary to provide methods that facilitate data generation in industrial environments. This dissertation is devoted to present a set of general methods to companies and manufacturers to boost the data generation phase in the industrial context. Concretely, we focus on a fast and efficient way to model manufacturing processes through the development of Machine Learning-based Surrogate Models. We propose different general theoretical frameworks implementing or combining machine learning techniques for surrogate modeling applicable in distinct manufacturing process. The thesis demonstrates that the proposed methods enable significant cost and time reductions in different practical manufacturing applications while maintaining high accuracy in modeling and predicting process variables. We investigate the importance of the data chosen to construct the Surrogate Models and the transfer of the knowledge in the Surrogate Models from simulation to real plants by means of Trans fer Learning. Overall, this supposes an improvement of the presented surrogate modeling methods and it facilitates the deployment of Surrogate Models in real-world industrial plants. The developed models during the thesis are a valuable asset in other studies, acting as a virtual environment to train Reinforcement Learning agents in hot stamping or supporting a Digital Twin of the high pressure die casting process. The thesis helps to advance towards the innovation of data-driven manufacturing by providing practical and efficient solutions in the direction of a better understanding of the manufacturing processes, leading to an enhancement in their performance and sustainability.
Approximate option pricing for jump-diffusion stochastic volatility models
(Universitat de Barcelona, 2025-01-21) Makumbe, Zororo Stanelake; Vives i Santa Eulàlia, Josep, 1963-; El-Khatib, Youssef; Universitat de Barcelona. Departament de Matemàtiques i Informàtica
[eng] The following is a summary of the above-mentioned thesis. The thesis covers alternative stochastic models, risk management, and option price decomposition. 1.1 Alternative Stochastic Models Several alternative asset pricing models are explored, each designed to capture market dynamics better. The models we consider include: 1. The Hybrid Stochastic Local Volatility (SLV) model entitled the Heston-CEV model with jumps (HCEVJ). This model combines the strengths of the Constant Elasticity of Variance (CEV) and Heston models, making volatility dependent on time, asset price, and an underlying stochastic process. 2. The 2-factor stochastic volatility model with jumps (2FSVJ) with multiple factors to drive the volatility process, offering richer dynamics. 3. Lastly, we consider the infinite activity Heston-Lévy model to account for large changes in asset prices due to jumps, thus capturing large market movements. The HCEVJ model is a general model with the CEV, Heston, Heston-CEV, Bates, and Heston-CEV with jumps as special cases. We calibrate each of these models to the EURO STOXX 50 European option quotes of 30 September 2014 using a brute-force grid search algorithm to facilitate comparisons. Monte Carlo methods are employed to model the asset price movements and verify model properties. The analysis shows that the HCEVJ model deepens the volatility smile by introducing an additional parameter that controls the intensity of the volatility smile. Moreover, the HCEVJ model exhibits the leverage effect, volatility clustering and price jumps, offering a more comprehensive representation of asset price dynamics. The properties of the 2FSVJ and Heston-Lévy models are not tested, however. 1.2 Malliavin Calculus, Hedging, and Option Greeks A key element of options pricing is hedging and option sensitivities. In this thesis, we use Malliavin Calculus to obtain faster estimates of the first-order Greeks of the option prices for the HCEVJ model. Additionally, we use the Clark-Ocone formula to find an explicit formula to hedge a portfolio. 1.3 Pricing Methods The third and main objective is to explore option pricing methods. The thesis reviews existing approaches, such as Monte Carlo simulations, Fourier integral methods, and decomposition techniques, and compares them. Decomposition methods outperform Monte Carlo simulations and Fourier integral methods, particularly under simple jump structures. In the 2FSVJ case, a first-order and a second-order decomposition formula are derived under a general jump structure. We choose log-normal and double-exponential jumps and carry out numerical experiments. The double-exponential jump case shows poorer accuracy and speed performance. Furthermore, the decomposition pricing model was more accurate under short-maturity and out-of-the-money conditions. In the Heston-Lévy case, we build on existing research on decomposition formulas by considering infinite activity jumps in asset returns. The study addresses the pricing of options in models where the return process includes both stochastic volatility and jumps of infinite activity but finite variation. The key contribution of this work is two exact decomposition formulas for option pricing under this model. The first decomposition formula expands the pricing model using a series of expectations involving the underlying asset and volatility terms and correction terms for the jumps in the asset price. However, this approach remains computationally challenging, as obtaining a tractable version of the formula is an open problem. The second Decomposition Formula uses methods from Lévy process estimation to simplify the infinite activity problem by approximating it as a finite activity jump process. Error bounds are provided for this approximation, and numerical estimates are compared to benchmark prices. The method, while accurate, relies on Monte Carlo simulations making it computationally slow.
End-to-End AI Solutions for Capsule Endoscopy: Enhancing Efficiency and Accuracy in Gastrointestinal Diagnostics
(Universitat de Barcelona, 2025-01-22) Gilabert Roca, Pere; Seguí Mesquida, Santi; Universitat de Barcelona. Departament de Matemàtiques i Informàtica
[eng] Artificial Intelligence (AI) models are fundamentally transforming the way clinicians carry out their daily tasks. By streamlining various processes, AI offers a more robust and consistent method for reviewing medical procedures. This thesis is dedicated to the development of AI applications for Capsule Endoscopy (CE), a small device that patients swallow, which is equipped with both a light and a camera to traverse the digestive system, capturing detailed images of internal organs. Once these images are captured, physicians are tasked with meticulously reviewing an extensive number of frames to identify potential pathologies, a process that is both time-consuming and tedious. In this thesis, we aim to enhance the entire review pipeline from end to end, providing support to physicians at multiple stages of the process. These stages include data collection, data labeling, assessing the usability of the videos (particularly in determining whether intestinal residues may hinder the process), identifying the entry and exit points of the small and large intestines, and most crucially, detecting polyps as early indicators of Colorectal Cancer (CRC). By employing advanced techniques such as Active Learning (AL) for data labeling and Vision Transformer (ViT) for polyp detection, we significantly improve upon existing systems in the literature, achieving state-of-the-art results. Additionally, the integration of AI into CE holds the promise of not only improving diagnostic accuracy but also reducing the workload for clinicians, allowing them to focus on more complex cases. This technological advancement has the potential to revolutionize gastrointestinal diagnostics, leading to earlier detection of diseases and, ultimately, better patient outcomes. Furthermore, this thesis led to the initiation of two clinical studies. The first was a controlled study that evaluated the performance of the polyp detection application. The second is a larger study involving over 600 patients, testing an enhanced version of the application, which is currently under development.
Characterization and Mitigation of Algorithmic Bias in Recommender Systems
(Universitat de Barcelona, 2024-12-17) Gómez Yepes, Elizabeth; Salamó Llorente, Maria; Universitat de Barcelona. Departament de Matemàtiques i Informàtica
[eng] Recommender Systems are critical in helping users navigate large amounts of information by providing personalized suggestions. However, these systems can exhibit biases, especially when data imbalances exist, leading to unfair recommendations that favor more popular or majority items over those from minority groups. This thesis explores the identification, characterization, and mitigation of algorithmic bias within Recommender Systems. This research focuses on addressing biases that arise from data imbalances and how these biases can lead to unfair treatment of certain groups, particularly in terms of visibility and exposure in recommendations. The primary goal of the thesis is to mitigate algorithmic bias in Recommender Systems to produce fairer and more equitable recommendation lists, through techniques of post-processing bias mitigation (e.g., re-ranking recommendation results to ensure fairness). This includes identifying and categorizing biases in datasets, designing strategies to mitigate these biases, and developing techniques to optimize recommendation algorithms to reduce bias. The main contributions of this thesis are five, divided into two thematic parts. The first thematic part focuses on Provider Fairness and the second thematic part on Fairness from Multiple Perspectives. Regarding the first thematic part, two contributions have been made. In the first, a Binary Approach was adopted, by categorizing geographic bias or imbalance associated with the country of production of the items and identifying two groups of providers (majority versus rest), and based on the distribution observed in the original training set, the recommendations are adjusted to align with these groups, with the aim of mitigating disparity bias. In the second contribution, we explain the process of categorization and bias mitigation using a Multi-Class Approach. We explore how recommendation algorithms can exacerbate biases by promoting items from certain regions, which could disadvantage underrepresented geographic groups. Concerning the second thematic part, three contributions have been made. The first contribution introduces CONFIGRE, a novel methodology designed to ensure fairness in Recommender Systems by balancing visibility between coarse- and fine-grained demographic groups. In second contribution we present MOReGln, a new approach for managing multiple objectives in Recommender Systems. This method specifically addresses the challenge of achieving both global balance and individual fairness in recommendations. Finally, in an additional contribution, we develop a new dataset (AMBAR, in the music domain) that includes sensitive attributes at various levels of granularity. Furthermore, we extend two real-world datasets (MovieLenslM and Book-Crossing) with geographic information to study the link between geographic imbalance and disparate impact. This thesis advances on the identification, characterization, mitigation and evaluation of biases in collaborative Recommender Systems. It addresses existing gaps in the analysis of geographical biases in different group settings: from binary groups, multi-class groups to different levels of granularity of groups. The outlined contributions establish a basis for further advancements and effective mitigation of biases without significantly compromising accuracy. Our findings, developed software, and resources presented in this dissertation are available to the community to facilitate further research and knowledge transfer.
Relational methods in algebraic logic
(Universitat de Barcelona, 2025-01-21) Fornasiere, Damiano; Gispert Brasó, Joan; Moraschini, Tommaso; Universitat de Barcelona. Departament de Matemàtiques i Informàtica
[eng] This thesis is concerned with three instances of relational methods in algebraic logic. First, determining which partially ordered sets are isomorphic to the spectrum of a Heyting algebra. This is an open question related to the classical problem of representing partially ordered sets as spectra of bounded distributive lattices or, equivalently, commutative rings with unit. We prove that a root system (the order dual of a forest) is isomorphic to the spectrum of a Heyting algebra if and only if it satisfies a simple order theoretic condition, known as "having enough gaps", and each of its nonempty chains has an infimum. This strengthens Lewis' characterisation of the root systems which are spectra of commutative rings with unit. While a similar characterisation for arbitrary forests currently seems out of reach, we show that a well-ordered forest is isomorphic to the spectrum of a Heyting algebra if and only if it has enough gaps and each of its nonempty chains has a supremum. Second, Sahlqvist theorem provides sufficient syntactic conditions for a normal modal logic to be complete with respect to an elementary class of Kripke frames. We extend Sahlqvist theory to the fragments of the intuitionistic propositional calculus that include the conjunction connective. This allows us to introduce a Sahlqvist theory of intuitionistic character amenable to arbitrary protoalgebraic deductive systems. As an application, we obtain a Sahlqvist theorem for the fragments of the intuitionistic propositional calculus that include the implication connective and for the extensions of the intuitionistic linear logic. Third, Blok's celebrated dichotomy theorem proves that each normal modal logic shares its Kripke frames with exactly one or continuurn-many logics. It is an outstanding open problem to characterise the number of logics having the same posets of an axiomatic extension of the intuitionistic propositional calculus. We solve this question in the case of implicative logics, the axiomatic extensions of the implicative fragment of the propositional intuitionistic logic. In this case, a trichotomy holds: every irnplicative logics shares its posets exactly with 1, N0, or 2(No) many logics.
Congested Optimal Transport in the Heisenberg Group
(Universitat de Barcelona, 2024-07-03) Circelli, Michele; Clop, Albert; Citi, Giovanna; Universitat de Barcelona. Departament de Matemàtiques i Informàtica
In this thesis we adapted the problem of continuous congested optimal transport to the Heisenberg group, equipped with a sub-Riemannian metric: we restricted the set of admissible paths to the horizontal curves. We obtained the existence of equilibrium configurations, known as Wardrop Equilibria, through the minimization of a convex functional, over a suitable set of measures on the horizontal curves. Moreover, such equilibria induce trans port plans that solve a Monge-Kantorovic problem associated with a cost, depending on the congestion itself, which we rigorously defined. We also proved the equivalence between this problem and a minimization problem defined over the set of p-summable horizontal vector fields with prescribed divergence. We showed that this new problem admits a dual formulation as a classical minimization problem of Calculus of Variations. In addition, even the Monge-Kantorovich problem associated with the sub-Riemannian distance turns out to be equivalent to a minimization problem over measures on horizontal curves. Passing through the notion of horizontal transport density, we proved that the Monge-Kantorovich problem can also be formulated as a minimization problem with a divergence-type constraint. Its dual formulation is the well-known Kantorovich duality theorem. In the end, we treated the continuous congested optimal transport problem with orthotropic cost function: we proved the Lipschitz regularity for solutions to a pseudo q-Laplacian-type equation arising from it.
Carotid Artery Ultrasound Image-Based Cardiovascular Risk Prediction using Deep Learning
(Universitat de Barcelona, 2024-05-03) Vila Muñoz, Maria del Mar; Igual Muñoz, Laura; Grau, Maria; Universitat de Barcelona. Departament de Matemàtiques i Informàtica
[eng] Cardiovascular Diseases (CVDs), the leading cause of death in developed countries, often involve atherosclerosis, which is a chronic inflammatory thickening of the inner artery layer. Monitoring atherosclerotic plaque detection and its characteristics is crucial for assessing future cardiovascular events. Carotid Artery (CA) Ultrasound (US) images are utilized for subclinical atherosclerosis detection by measuring carotid Intima Media Thickness (IMT) and identifying atherosclerotic plaques. This thesis introduces Deep Learning (DL) methods to segment CA US images and characterize atherosclerotic plaque, aiming to improve cardiovascular risk prediction. First, we address the segmentation of the Carotid Intima-Media (CIM) region, where the IMT is estimated. In this work, we introduce a fully automated method based on Convolutional Neural Networks that accurately localizes the carotid IMT region in longitudinal B-mode CA US images. In particular, we present a novel single-step approach using DenseNets for semantic segmentation, resulting in enhanced subclinical atherosclerosis detection through efficient carotid IMT estimation and atherosclerotic plaque detection. This thesis introduces two clinical applications of carotid IMT estimation and atherosclerotic plaque detection. The first study evaluates cardiovascular event risk in autoimmune disease patients, focusing on chronic inflammation's impact on subclinical atherosclerosis. In the second study, we examine the coexistence of subclinical atherosclerosis in the lower limb (Ankle-Brachial Index) and carotid arteries. The findings of both studies highlights the systemic nature of atherosclerosis, suggesting a correlation between biomarkers in different areas and the likelihood of subclinical disease. Finally, we explore new ways of improving cardiovascular risk prediction using DL techniques to extract information from CA US. In cardiovascular epidemiology, risk prediction functions assess the likelihood of a cardiovascular event based on individual clinical variables, using survival models. Despite their accurate stratification into low, moderate, and high-risk groups, a significant number of cardiovascular events still occur in the medium-risk category. This study introduces a novel approach for CA characterization, integrating individual artery condition data into traditional survival models. The work presents an innovative survival model that incorporates CA US image features derived from Deep Neural Networks, enabling effective cardiovascular risk prediction and the reclassification of individuals from the moderate to the high-risk category within the survival model.
Geometric realizations using regular subdivisions: Construction of many polytopes, sweep polytopes, s-permutahedra
(Universitat de Barcelona, 2024-06-07) Philippe, Eva; Padrol Sureda, Arnau; Santos, Francisco, 1968-; Universitat de Barcelona. Departament de Matemàtiques i Informàtica
[eng] This thesis concerns three problems of geometric realizations of combinatorial structures via polytopes and polyhedral subdivisions. A polytope is the convex hull of a finite set of points in a Euclidean space Rd. It is endowed with a combinatorial structure coming from its faces. A subdivision is a collection of polytopes whose faces intersect properly and such that their union is convex. It is regular if it can be obtained by taking the lower faces of a lifting of its vertices in one dimension higher. We first present a new geometric construction of many combinatorially different polytopes of fixed dimension and number of vertices. This construction relies on showing that certain polytopes admit many regular triangulations. It allows us to improve the best known lower bound on the number of combinatorial types of polytopes. We then study the projections of permutahedra, that we call sweep polytopes because they model the possible orderings of a fixed point configuration by hyperplanes that sweep the space in a constant direction. We also introduce and study a combinatorial abstraction of these structures: the sweep oriented matroids, that generalize Goodman and Pollack’s theory of allowable sequences to dimensions higher than 2. Finally, we provide geometric realizations of the s-weak order, a combinatorial structure that generalizes the weak order on permutations, parameterized by a vector s ∈ (Z>0)n. In particular, we answer Ceballos and Pons’s conjecture that the s-weak order can be realized as the edge-graph of a polytopal complex that is moreover a subdivision of a permutahedron.
Gaze Estimation with Spatiotemporal and Multimodal Deep Learning
(Universitat de Barcelona, 2024-01-22) Palmero Cantariño, Cristina; Escalera Guerrero, Sergio; Universitat de Barcelona. Departament de Matemàtiques i Informàtica
[eng] lt is often said that the eyes are the window to the soul. The eyes and their behavior have sparked interest for centuries, and have been widely studied due to their link with multiple developmental, neurological, behavioral, cognitive, and clinical factors. Furthermore, the ability to accurately detect the fine of sight has enabled many possibilities for consumer applications, such as human-computer interaction and gaze-contingent displays. Eye-tracking technology has evolved to the point where noninvasive, sufficiently accurate, and cost-effective camera-based approaches are becoming increasingly available, driven by the progressive miniaturization of electronics and breakthroughs in computer vision and deep learning: However, achieving universal applicability in eye tracking remains a challenge, primarily due to the influence of individual factors, varying environmental conditions, and the impact of sensor viewpoint or head pose shifts. Recent remate and portable eye-tracking·devices often sacrifice robustness and accuracy when used in uncontrolled scenarios. In addition, they grapple with the need for rapid eye signa! capture, a crucial requirement for specific applications. The promising potential of eye tracking motivates us to further enhance existing methods, striving for greater reliability, accuracy, and speed. In turn, as eye tracking becomes more ubiquitous, it encourages us to explore innovative applications that leverage its expanding capabilities. This thesis approaches eye tracking from a computer vision and deep learning perspective, with the goal of: 1) increasing the accuracy and sampling rate of current gaze estimation approaches across different scenarios and devices; and 2} promoting the use of gaze input in emerging applications. For the first goal, we investigate the contribution of spatiotemporal and multimodal/multisensor cues for gaze estimation, both for remote cameras (e.g., desktop setting) and infrared, near-eye devices (e.g.,·head-mounted displays), across different sources of variability. To do so, we rely on the combination of convolutional-recurrent deep neural networks and feature-based and hybrid multimodal fusion. In. particular, we address multimodality from two different angles. First, by combining appearance and shape cues (i.e., 3D facial landmarks) extracted from RGB face images to increase accuracy. And second, by combining the signa·! obtained by two different sensors (camera and photosensors) operating at the same or different sampling rates, to increase the accuracy and the effective sampling rate of the estimated gaze signa!. We then move on to the second goal, for which we explore the use of gaze-related features along with other modalities, such as speech and facial expressions, for emotion expression recognition in a conversational human-machine interaction scenario. More concretely, we focus on the interaction between a simulated virtual coach and older adults, delving into the nuances of affective computing in this context.
Application of Radiomics-based Machine Learning models on complex cardíac diseases
(Universitat de Barcelona, 2024-07-18) Izquierdo, Cristián; Lekadir, Karim, 1977-; Gkontra, Polyxeni; Universitat de Barcelona. Departament de Matemàtiques i Informàtica
[eng] This doctoral thesis investigates the combination of radiomics and machine learning (ML) within the field of cardiology, emphasizing early detection and prognosis of complex cardiovascular diseases (CVDs). Radiomics converts standard medical images into detailed, high-dimensional data sets that expose subtle cardiac pathologies invisible to the naked eye. A specialized pipeline was developed to extract radiomic features and apply ML for effective classification and analysis. Each chapter modifies and optimizes this pipeline for different scenarios, culminating in a survival analysis ML pipeline in the final chapter. The thesis starts with a fundamental overview of cardiovascular diseases, radiomics, and ML, laying the groundwork for their use in cardiac imaging. The second chapter illustrates how cardiovascular magnetic resonance (CMR) radiomics and ML can differentiate left ventricular non-compaction cardiomyopathy (LVNC) from other types such as hypertrophic and dilated cardiomyopathies. In this chapter, we illustrated that radiomics is crucial in this differentiation process, showing that an automated ML-Radiomics pipeline can achieve state- of-the-art benchmarks from the clinical variables used in current medical practice, but without need for clinicians manual delineations. The subsequent chapter explores the benefits of integrating CMR radiomics with electrocardiogram (ECG) data to enhance atrial fibrillation (AF) detection. In this study of the UK Biobank participants we demonstrated that an ECG-based model had lower accuracy to detect AF in female subjects compared to males. The inclusion of CMR radiomics combined with ECG increased the model performance in women. The main universal implication is that a combined approach of ECG and atrial imaging might lead to better assessment of female participants suspected of AF. The fourth chapter evaluates the capacity of CMR radiomics and ML to forecast significant cardiovascular events like AF, heart failure (HF), myocardial infarction (MI), and stroke, using data from the UK Biobank. Incorporating radiomic features with vascular risk factors (VRFs) and CMR indices significantly enhances the performance of these predictive models. Radiomics features provided additional information over VRFs, although the improvement was only marginal compared to conventional CMR metrics. The improvement was most prominent in AF and HF prediction, which highlight that the performance of radiomics models is dependent on the disease aetiology and mechanism. The final chapter focuses on the use of radiomics and ML for identifying genetic cardiomyopathy in patients with excessive trabeculation. In a multicenter cohort study of individuals diagnosed with excessive trabeculation of the left ventricle radiomics analysis of standard, non-enhanced cine CMR images provided added value beyond left ventricular ejection fraction in the identification of a genetic or familial substrate and of adverse prognosis. Textural radiomics features were instrumental to recognize a genetic or familial substrate, while shape features dominated the identification of adverse prognosis. This thesis underscores the potential of radiomics and ML to advance cardiac diagnostic and prognostic capabilities, providing a more precise, personalized approach to managing CVDs.
Regularity theory for obstacle problems and boundary Harnack inequalities
(Universitat de Barcelona, 2024-06-21) Torres Latorre, Clara; Ros, Xavier; Universitat de Barcelona. Departament de Matemàtiques i Informàtica
[eng] This thesis is dedicated to the study of elliptic and parabolic Partial Differential Equations, both local and nonlocal. More specifically, this work concerns the regularity properties of some obstacle problems. Obstacle problems are prototypical examples of free boundary problems, that is, PDE problems where the unknowns are not only a function, but also a subdivision of the domain into different regions, and the PDE satisfied in each region is different. Free boundary problems are a very active field of research. On the one hand, free boundaries are a good model for interfaces in real-world settings, with applications in Physics, Biology, Finance and Engineering. On the other hand, they have been a source of interesting mathematical challenges, motivating the fine analysis of solutions to elliptic and parabolic equations. This Thesis is divided into two Parts. Part I is devoted to the study of several different obstacle problems. In Chapter 1, we study the obstacle problem for parabolic nonlocal operators, in the supercritical regime s < 1/2. We establish the optimal C^{1,1} regularity of solutions, which is surprisingly better than in the elliptic problem, and we also show that the free boundary is globally C^{1,α}. Our main difficulties are the lack of monotonicity formulas, and the supercritical scaling of the equation, that is, the fact that the highest order of differentiation corresponds to the time derivative. Chapter 2 is devoted to the generic regularity properties of the free boundary in the thin obstacle problem. Since there are many pathological examples of solutions to free boundary problems, often the goal is instead of proving regularity for all solutions, proving regularity for most solutions in an appropriate sense. In our work, we show that, for one-parameter monotonous families of solutions, for almost every solution, the free boundary is smooth outside of a set of codimension 2 + α (in the free boundary). In particular, this means that in R^3 and R^4, the free boundary is generically smooth. We conclude Part I with Chapter 3, where we use a nonlocal analogue of the Bernstein technique to establish semiconvexity estimates for a wide class of nonlinear nonlocal elliptic and parabolic equations, including obstacle problems. As a consequence, we extend the known regularity theory for nonlocal obstacle problems in the full space to problems in bounded domains. In Part II, we extend the boundary Harnack inequality to (local) elliptic and parabolic equations with a right-hand side. The boundary Harnack is a classical result that states that if u and v are positive harmonic functions that vanish on part of the boundary of a regular enough domain, then u/v is bounded and Hölder continuous up to the boundary. Boundary Harnack inequalities are used in the proof of the smoothness of free boundaries in several obstacle problems, in the key step of seeing that if a free boundary is flat Lipschitz, then it is C^{1,α}. The goal of our work was to extend the regularity theory of obstacle problems to the fully nonlinear setting. To do so, we developed boundary Harnack inequalities for equations in non-divergence form with a right-hand side. Chapter 4 concerns elliptic equations and Chapter 5 is about parabolic equations. The techniques used are different. In the elliptic setting, it is enough to use barriers, scaling arguments and a standard iteration to deduce the Hölder regularity of the quotient. However, in the parabolic world, the proofs are much more involved and they are based on a delicate contradiction-compactness argument.
Automatic Cardiac Segmentation of Complex Morphologies, Modalities and Tissues
(Universitat de Barcelona, 2024-01-18) Martín Isla, Carlos; Escalera Guerrero, Sergio; Universitat de Barcelona. Departament de Matemàtiques i Informàtica
[eng] Cardiovascular diseases (CVDs) continue to take a significant toll on global health, highlighting the need for more accurate and efficient diagnostic tools. This thesis, titled "Automatic Cardiac Segmentation of Complex Morphologies, Modalities, and Tissues Using Deep Learning," delves into complex medical imaging and artificial intelligence (AI) technologies necessary to perform advanced and cutting-edge cardiovascular diagnostics. The groundwork of this work is laid by emphasizing the critical importance of early, precise, and personalized CVD assessment by means of machine learning (ML) and deep learning (DL), in order to evolve from qualitative visual assessments and basic quantitative measures into advanced, quantitative, data- driven insights. The importance of accurate delineation of cardiac structures for a correct assessment of their status and function is crucial to move forward in that direction. The first chapter delves into the right ventricle segmentation within magnetic resonance imaging (MRI) images, highlighting the challenges posed by complex shapes and ill-defined borders. It introduces the M&Ms-2 challenge, a substantial dataset encompassing diverse pathologies, multiple views, and various scanners. The chapter discusses the success of nnU-Net and underscores the value of multi-view approaches, indicating the need for comprehensive cardiac segmentation algorithms. In the second chapter, the focus shifts to late gadolinium enhancement MRI (LGE-MRI) segmentation, crucial for quantifying scar tissue in cardiac patients. The proposed solution leverages generative adversarial networks to create synthetic images, enhancing segmentation accuracy in the presence of scar tissue. Results reveal the potential of multi-sequence model training with synthetic images and data augmentation to outperform traditional methods. The third chapter addresses the segmentation of pathological tissue, specifically scar tissue and edema, within multi-modal cardiac MRI images. The chapter introduces a two-staged approach, involving a stacked BCDU-net for accurate myocardium segmentation and multi-modal pathological region segmentation. Anatomically constrained synthetic data augmentation enriches the model's performances. This thesis represents a pioneering effort to enhance cardiac deep learning-driven segmentation. By tackling the complexities of morphologies, MRI modalities and pathological tissues, this research contributes valuable insights, algorithms, and datasets to such task.
Mastering the Triad of Data, Models and Tasks in Deep Learning for Image Understanding
(Universitat de Barcelona, 2024-06-27) Nagarajan, Bhalaji; Radeva, Petia; Aguilar, Eduardo; Universitat de Barcelona. Departament de Matemàtiques i Informàtica
[eng] Deep learning's rapid growth brings vast application potential across diverse domains. Achieving optimal performance hinges on a critical interplay between three key elements: powerful model architectures, vast amounts of data, and a deep understanding of the target domain. Each element presents unique challenges. This thesis tackles these challenges to unlock the full potential of models, exploring solutions for data, models, and task understanding. The first part of this thesis tackles the fundamental challenges associated with data used in deep learning. Acquiring large-scale data is a significant challenge, often limited by factors like annotation costs and label errors. Data within a dataset frequently exhibits significant diversity. We address these challenges with a multifaceted approach. We investigate the development of noise-robust sample-selection-based deep learning models to handle the presence of label errors. To leverage the large volumes of unlabeled data available, we explore contrastive self- supervised learning strategies. To address the heterogeneity within datasets, we propose a sample importance strategy to prioritize samples that present learning challenges. These solutions address the various data-related challenges that hinder deep learning models. The second part of the thesis covers the critical role of understanding model behaviour. We use uncertainty quantification metrics to gain valuable insights into the capabilities of the models in making predictions. By understanding these metrics, we identify areas where the model’s predictions might be less reliable. We extend our exploration by applying these uncertainty metrics across various tasks to improve the decision-making process of the models. The final part of this thesis explores the importance of task understanding. We utilize the challenging domain of food recognition as a case study. Food recognition presents unique challenges due to the visual complexity of food images. We address the domain-specific challenges of fine- grained and multi-label classification by strategically designing and modifying deep learning models to improve their performances. Our research during this thesis yielded significant advancements in several key areas of model development. We achieved state-of-the-art results on several benchmarks across various tasks, demonstrating the effectiveness of our proposed solutions. This highlights the potential of our work to contribute to the broader field of deep learning.
Advancing 3D Point Cloud Understanding in Real-World Applications
(Universitat de Barcelona, 2024-06-03) Zoumpekas, Athanasios; Puig Puig, Anna; Salamó Llorente, Maria; Universitat de Barcelona. Departament de Matemàtiques i Informàtica
[eng] In recent years, rapid advancements in 3D sensing technologies, such as LiDAR, have revolutionized various fields, spanning robotics, augmented reality, earth vision, and industrial manufacturing. Point clouds, acquired through 3D sensing technologies, capture the geometric structure of objects and environments in a three-dimensional coordinate system. However, the lack of structure and order in point clouds, as well as the significantly redundant and inconsistent sample densities, makes it challenging to analyze. In addition, point clouds captured in real-world setups contain millions of points accompanied by noise either from the measurement tool itself or by moving objects in the scene, leading to further computational challenges. Moreover, point clouds are frequently obtained dynamically, generating temporal 3D point clouds, where the alignment between frames is often essential for spatial consistency and accurate analysis. Consequently, learning intelligent models on either static or temporal 3D point clouds presents important challenges and necessitates advanced computational techniques to address issues of accuracy, efficiency, and robustness depending on the application needs. This thesis presents research efforts toward advancing 3D point cloud understanding, providing theoretical and practical insights to enhance decision-making and application in fields where spatial and geometric understanding is important. The main contributions of this thesis are seven, divided into three thematic parts, Model Evaluation and Interactive Visualization in 3D Point Cloud Segmentation, 3D Understanding Applications in Geoscience and 3D Understanding Applications in Industrial Manufacturing. Concerning the first thematic part, four contributions have been made. The first contribution includes a benchmarking of point cloud segmentation models that instead of focusing solely on accuracy-related performance metrics, further incorporates time and memory efficiency evaluation. Then, our second contribution encompasses a comprehensive analysis of state-of-the-art deep learning architectures for 3D point cloud segmentation. Through rigorous evaluation approaches, novel performance metrics are proposed to facilitate effective model comparison, considering ac- curacy, time and memory efficiency, and robustness. In addition, we create a correspondence between model design properties and experimental properties, further elucidating model selection. Our third contribution includes a proposed early-stopping technique for enhancing the trade-off between efficiency and accuracy in training neural networks on point cloud segmentation. Our fourth contribution to model evaluation and selection is visual insights into the results of point cloud segmentation models during and after the learning process. A new dashboard visualization tool, named CLOSED, has been proposed facilitating the rigorous comparison of different neural networks in 3D point cloud segmentation. Concerning the second part on applications in the intersection of Geoscience, Machine Learning, and Computer Vision, two contributions have been made towards automating rockfall detection utilizing real-world captured temporal 3D point clouds. The first one focuses on enhancing rock- fall detection and addresses critical challenges such as class imbalance in the detection of rockfall candidate areas. Initially, various machine learning algorithms are studied alongside resampling techniques on real-world 3D scans in order to develop an intelligent framework for rockfall detection. This framework, further extended to incorporate geological properties, demonstrates high accuracy and robustness in detecting areas susceptible to rockfall. The second contribution leverages advancements in point-based neural networks and spatiotemporal information from the captured 3D scans to improve the accuracy and efficiency of rockfall candidate area detection. The proposed method showcases effectiveness in identifying rockfall candidate areas directly from real-world 3D scans. Finally, concerning the third part on applications in the intersection of Industrial Manufacturing, Deep Learning, and Computer Vision, one contribution has been made. Our contribution lies in adapting 3D point cloud understanding models to accurately identify various machining tools based on sampled surfaces, enabling insights for optimizing industrial machining processes and reverse engineering workpieces. Specifically, we propose a novel process and develop guidelines for the task of machining tool identification using temporal 3D point clouds, sampled from the tool engagement surface from a workpiece in progress. This thesis advances 3D point cloud understanding in real-world applications. It addresses existing gaps in the research field, poses new research questions, and explores novel research directions. We present deep learning and classical machine learning techniques on 3D point clouds and real-world applications in geoscience and industrial manufacturing. The outlined contributions establish a basis for further advancements and effective utilization of models on 3D point clouds across diverse disciplines. Our findings, developed software, and resources presented in this dissertation are available to the community to facilitate further research and knowledge transfer.
Suitable logics: provability, temporal laws, and formalization
(Universitat de Barcelona, 2024-01-12) Borges, Ana de Almeida Gabriel Vieira; Joosten, Joost J.; Universitat de Barcelona. Departament de Matemàtiques i Informàtica
[eng] This thesis explores various aspects of logic, encompassing provability logic, logical analysis of law, and formalization of both mathematics and software. We are particularly interested in the aspect of suitability, both in the sense of finding expressible and tractable fragments of certain logical systems, and in the sense of finding appropriate formal systems for describing certain legal texts. In the domain of provability logic, we introduce two novel calculi: the Worm Calculus (WC) and the Quantified Reflection Calculus with one modality (QRC1). Both WC and QRC1 are inspired by the Reflection Calculus (RC), introduced by Dashkov in 2012. All three logics are strictly positive provability logics, with WC and RC being propositional and polymodal, while QRC1 features a quantified language with a single modality. Worms are words in a numerical alphabet that have many possible readings, particularly as iterated consistency statements. Although the language of worms is very simple, it is remarkably expressive, and known to fully describe the closed fragment of RC. The Worm Calculus is a calculus in the language of worms that illustrates this power: RC is shown to be conservative over WC. Vardanyan showed in 1986 that the quantified provability logic of Peano Arithmetic (QPL(PA)) is Π0-complete, and in particular not recursively axiomatizable. We investigate the strictly positive fragment of QPL(PA), showing that QRC1 is a decidable axiomatization of that fragment. In the process, we prove soundness and completeness of QRC1 with respect to Kripke semantics and two flavors of arithmetical semantics. We also see that QRC1 is the strictly positive fragment of QK4 and of QGL, and of any logic in between those. In the realm of law and inspired by a collaboration with industry, we focus on two European transport regulations, examining certain articles with curious mathematical properties. Then we identify fragments of Monadic Second-order Logic capable of expressing specific segments of one of these regulations, and show how other fragments are less suitable. This effort illustrates some issues with the way the current regulations specify algorithms, and it hints at the role of model checking as a useful legal tool. Lastly, we delve into the formal verification of both mathematics and software using Coq, presenting two case studies. The first case study involves the formalization of modal logical results on QRC1. We describe the overall formalization strategy, focusing on the difficulties and adaptations of both definitions and proofs helpful for the formalization. Due to this process, we were able to identify a small number of improvements to the original proofs. The formalization of software is somewhat different from the formalization of mathematics, although they share many particularities. We use a general framework for software formalization that starts by writing a basic specification for each function, which is then iteratively refined with better algorithms, data structures, and error handling, culminating in extraction to OCaml. Our case study is the formalization of UTC calendars, particularly functions to translate between human-readable times and timestamps, as well as functions to perform time arithmetic. This is a first step towards the formalization of laws that depend on time keeping, of which there are many, including the ones studied here.

El Dipòsit Digital ha actualitzat el programari. Contacteu amb dipositdigital@ub.edu per informar de qualsevol incidència.

Examinar

Enviaments recents