Geodinámica del margen continental de Galicia: estructura profunda y morfotectónica

La presente Tesis Doctoral lleva por t tulo Geodin amica del margen continental de Galicia: Estructura profunda y morfotect onica. Este estudio se aborda a partir de la integraci on de un gran volumen de nuevos datos geof sicos (gravim etricos, batim etricos y s smica de re exi on multicanal 2D y de ultra-alta resoluci on), procedentes de los proyectos ZEEE, ERGAP y BURATO4242. La nueva informaci on ha aportado constricciones muy relevantes sobre el origen, la estructura profunda y la complejidad siogr a ca del margen, as como sobre la caracterizaci on de la variaci on lateral de la transici on oc eano-continente. El margen continental de Galicia se clasi ca como un margen de rift pobre en magma. Este tipo de m argenes tienen dos rasgos comunes, que son: 1) Los pares de m argenes conjugados son asim etricos, teniendo uno de ellos una zona m as ancha de corteza extremadamente adelgazada, subrayada por un re ector s smico subhorizontal; 2) Entre la corteza continental adelgazada y la corteza oce anica normal, hay una zona de basamento compuesto por manto serpentinizado. La estructura del margen continental gallego es extremadamente compleja, re ejando la superposici on de varias etapas sucesivas de rift, y una etapa compresiva posterior que da como resultado la inversi on parcial del margen. Adem as, la proximidad de un punto triple de dorsal produce un cambio de orientaci on de las estructuras principales. Este margen continental ha sido ampliamente estudiado desde la d ecada de los '70. Sin embargo, la mayor parte de los estudios se han centrado en la parte occidental, existiendo una importante carencia de informaci on en los ancos norte y noroeste. Este hecho, junto con su gran complejidad estructural, ha provocado que no exista un modelo geodin amico previo que integre todos los procesos observados. Algunos aspectos, como son la transici on entre el margen oeste (extensivo) y el margen norte (compresivo), y la forma en que se produce su inversi on tect onica, apenas han sido abordados con anterioridad por la comunidad científica...

Verificación de extensiones de Redes de Petri con precios, tiempo y múltiples instancias

Las redes de Petri son un lenguaje formal muy adecuado para la modelizacíon, ańalisis y verificacíon de sistemas concurrentes con infinitos estados. En particular, son muy apropiadas para estudiar las propiedades de seguridad de dichos sistemas, dadas sus buenas propiedades de decidibilidad. Sin embargo, en muchas ocasiones las redes de Petri carecen de la expresividad necesaria para representar algunas caracteŕısticas fundamentales de los sistemas que se manejan hoy en d́ıa, como el manejo de tiempo real, costes reales, o la presencia de varios procesos con un ńumero no acotado de estados ejecut́andose en paralelo. En la literatura se han definido y estudiado algunas extensiones de las redes de Petri para la representaci ́on de las caracteŕısticas anteriores. Por ejemplo, las “Redes de Petri Temporizadas” [83, 10](TPN) incluyen el manejo de tiempo real y las ν-redes de Petri [78](ν-PN) son capaces de representar un ńumero no acotado de procesos con infinitos estados ejecut́andose concurrentemente. En esta tesis definimos varias extensiones que réunen estas dos caracteŕısticas y estudiamos sus propiedades de decidibilidad. En primer lugar definimos las “ν-Redes de Petri Temporizadas”, que réunen las caracteŕısticas expresivas de las TPN y las ν-PN. Este nuevo modelo es capaz de representar sistemas con un ńumero no acotado de procesos o instancias, donde cada proceso es representado por un nombre diferente, y tiene un ńumero no acotado de relojes reales. En este modelo un reloj de una instancia debe satisfacer ciertas condiciones (pertenecer a un intervalo dado) para formar parte en el disparo de una transicíon. Desafortunadamente, demostramos que la verificacíon de propiedades de seguridad es indecidible para este modelo...