Temporary closures of octopus fishing areas constitute a promising co-management measure that aims to improve local governance, food security and incomes in coastal small-scale fishing communities. Although positive social and economic outcomes of temporary closures are increasingly reported, the underlying social-ecological and ecological interactions, and their impact on closure benefits are rarely studied. This lack of systemic understanding may lead to undesired outcomes. Here, I extend an existing agent-based model of temporary closures to explore the influence of individual octopus movements on ecological outcomes and fishers’ benefits in Zanzibar. First, I conceptualized the octopus closure system by analyzing empirical qualitative data and literature. Next, I iteratively developed and tested an individual-based model extension. This extension simulates between-den movements across a hypothetical seascape and formalizes intrinsic attributes of Octopus cyanea such as movement patterns and maturity stages. I analyzed the effects of varying closure size of fishing grounds temporarily closed to illustrate potential implications for outcomes of octopus closures. Simulation results show that individual octopus movements triggered by fishing activities have noticeable impacts on octopus sizes, their spatial and temporal distribution, and fishers’ catches, particularly when considering different social groups that depend on the fishery. Scenarios with closures in place show higher mean octopus weight in closed areas in contrast to open-access areas. Mean catches for women foot-fishers are lower compared to freedivers’ catches and even slightly lower when allowing octopuses to move in response to disturbance in all scenarios. Catch rates and distribution of mature octopuses are highly sensitive to closure size revealing a social-ecological trade-off when implementing larger closures. This study demonstrates an approach to integrating individual octopus movements and interactions between fishers and octopuses in a fishery management context, and suggests that reactive movement of octopus contributes to unequal distribution of the closure benefits between different social groups. / Octopus and People In Novel Transdisciplinary Simulations (OctoPINTS project)

Les travaux présentés dans cette thèse sont lies aux problèmes de vérification de l'atteignabilité et de la terminaison de programmes qui manipulent des données entières non-bornées. On décrit une nouvelle méthode de vérification basée sur une technique d'accélération de boucle, qui calcule, de manière exacte, la clôture transitive d'une relation arithmétique. D'abord, on introduit un algorithme d'accélération de boucle qui peut calculer, en quelques secondes, des clôtures transitives pour des relations de l'ordre d'une centaine de variables. Ensuite, on présente une méthode d'analyse de l'atteignabilité, qui manipule des relations entre les variables entières d'un programme, et applique l'accélération pour le calcul des relations entrée-sortie des procédures, de façon modulaire. Une approche alternative pour l'analyse de l'atteignabilité, présentée également dans cette thèse, intègre l'accélération avec l'abstraction par prédicats, afin de traiter le problème de divergence de cette dernière. Ces deux méthodes ont été évaluées de manière pratique, sur un nombre important d'exemples, qui étaient, jusqu'a présent, hors de la portée des outils d'analyse existants. Dernièrement, on a étudié le problème de la terminaison pour certaines classes de boucles de programme, et on a montré la décidabilité pour les relations étudiées. Pour ces classes de relations arithmétiques, on présente un algorithme qui s'exécute en temps au plus polynomial, et qui calcule l'ensemble d'états qui peuvent générer une exécution infinie. Ensuite on a intégré cet algorithme dans une méthode d'analyse de la terminaison pour des programmes qui manipulent des données entières. / This work presents novel methods for verification of reachability and termination properties of programs that manipulate unbounded integer data. Most of these methods are based on acceleration techniques which compute transitive closures of program loops. We first present an algorithm that accelerates several classes of integer relations and show that the new method performs up to four orders of magnitude better than the previous ones. On the theoretical side, our framework provides a common solution to the acceleration problem by proving that the considered classes of relations are periodic. Subsequently, we introduce a semi-algorithmic reachability analysis technique that tracks relations between variables of integer programs and applies the proposed acceleration algorithm to compute summaries of procedures in a modular way. Next, we present an alternative approach to reachability analysis that integrates predicate abstraction with our acceleration techniques to increase the likelihood of convergence of the algorithm. We evaluate these algorithms and show that they can handle a number of complex integer programs where previous approaches failed. Finally, we study the termination problem for several classes of program loops and show that it is decidable. Moreover, for some of these classes, we design a polynomial time algorithm that computes the exact set of program configurations from which non-terminating runs exist. We further integrate this algorithm into a semi-algorithmic method that analyzes termination of integer programs, and show that the resulting technique can verify termination properties of several non-trivial integer programs. / Tato pr´ace pˇredstavuje nov´e metody pro verifikaci program°u pracuj´ıc´ıch s neomezen´ymiceloˇc´ıslen´ymi promˇenn´ymi, konkr´etnˇe metody pro anal´yzu dosaˇzitelnosti a koneˇcnosti.Vˇetˇsina tˇechto metod je zaloˇzena na akceleraˇcn´ıch technik´ach, kter´e poˇc´ıtaj´ı tranzitivn´ıuz´avˇery cykl°u programu.V pr´aci je nejprve pˇredstaven algoritmus pro akceleraci nˇekolika tˇr´ıd celoˇc´ıseln´ychrelac´ı. Tento algoritmus je aˇz o ˇctyˇri ˇr´ady rychlejˇs´ı neˇz existuj´ıc´ı techniky. Z teoretick´ehohlediska pr´ace dokazuje, ˇze uvaˇzovan´e tˇr´ıdy relac´ı jsou periodick´e a poskytuje tud´ıˇzjednotn´e ˇreˇsen´ı prol´emu akcelerace.Pr´ace d´ale pˇredstavuje semi-algoritmus pro anal´yzu dosaˇzitelnosti celoˇc´ıseln´ych program°u, kter´y sleduje relace mezi promˇenn´ymi programu a aplikuje akceleraˇcn´ı technikyza ´uˇcelem modul´arn´ıho v´ypoˇctu souhrn°u procedur. D´ale je v pr´aci navrˇzen alternativn´ıalgoritmus pro anal´yzu dosaˇzitelnosti, kter´y integruje predik´atovou abstrakci s accelerac´ıs c´ılem zv´yˇsit pravdˇepodobnost konvergence v´ypoˇctu. Proveden´e experimenty ukazuj´ı, ˇzeoba algoritmy lze ´uspˇeˇsnˇe aplikovat k verifikaci program°u, na kter´ych pˇredchoz´ı metodyselh´avaly.Pr´ace se rovnˇeˇz zab´yv´a probl´emem koneˇcnosti bˇehu program°u a dokazuje, ˇze tentoprobl´em je rozhodnuteln´y pro nˇekolik tˇr´ıd celoˇc´ıseln´ych relac´ı. Pro nˇekter´e z tˇechto tˇr´ıdrelac´ı je v pr´aci navrˇzen algoritmus, kter´y v polynomi´aln´ım ˇcase vypoˇc´ıt´a mnoˇzinu vˇsechkonfigurac´ı programu, z nichˇz existuje nekoneˇcn´y bˇeh. Tento algoritmus je integrov´ando metody, kter´a analyzuje koneˇcnost bˇeh°u celoˇc´ıseln´ych program°u. Efektivnost t´etometody je demonstrov´ana na nˇekolika netrivi´aln´ıch celoˇc´ıseln´ych programech.

This investigation identifies how CAD models of typical automotive body assemblies could be defined to allow a continuous optimisation of the number of iterations required for the final design and the number of variants on the basis of Parametric Associative Design (PAD) and how methodologies for the development of surfaces, parts and assemblies of the automotive body can be represented and structured for a multiple re-use in a collaborative environment of concept phase of a Product Evolution (Formation) Process (PEP). The standardisation of optimised processes and methodologies and the enhanced interaction between all parties involved in product development could lead to improve product quality and reduce development time and hence expenses. The fundamental principles of PAD, the particular methodologies used in automotive body design and the principles of methodical development and design in general are investigated. The role which automotive body engineers play throughout the activities of the PEP is also investigated. The distribution of design work in concept teams of automotive body development and important methodologies for the design of prismatic profile areas is critically analysed. To address the role and distribution of work, 25 group work projects were carried out in cooperation with the automotive industry. Large assemblies of the automotive bodies were developed. The requirements for distributed design work have been identified and improved. The results of the investigation point towards a file based, well structured administration of a concept design, with a zone based approach. The investigation was extended to the process chain of sections, which are used for development of surfaces, parts and assemblies. Important methods were developed, optimised and validated with regard to an update safe re-use of 3D zone based CAD models instead of 2D sections. The thesis presents a thorough description of the research undertaken, details the experimental results and provides a comprehensive analysis of them. Finally it proposes a unique methodology to a zone based approach with a clearly defined process chain of sections for an update-safe re-use of design models.