No description available.

Slices are digraphs that can be composed together to form larger digraphs.In this thesis we introduce the foundations of a theory whose aim is to provide ways of defining and manipulating infinite families of combinatorial objects such as graphs, partial orders, logical equations etc. We give special attentionto objects that can be represented as sequences of slices. We have successfully applied our theory to obtain novel results in three fields: concurrency theory,combinatorics and logic. Some notable results are: Concurrency Theory: We prove that inclusion and emptiness of intersection of the causalbehavior of bounded Petri nets are decidable. These problems had been open for almost two decades. We introduce an algorithm to transitively reduce infinite familiesof DAGs. This algorithm allows us to operate with partial order languages defined via distinct formalisms, such as, Mazurkiewicztrace languages and message sequence chart languages. Combinatorics: For each constant z ∈ N, we define the notion of z-topological or-der for digraphs, and use it as a point of connection between the monadic second order logic of graphs and directed width measures, such as directed path-width and cycle-rank. Through this connection we establish the polynomial time solvability of a large numberof natural counting problems on digraphs admitting z-topological orderings. Logic: We introduce an ordered version of equational logic. We show thatthe validity problem for this logic is fixed parameter tractable withrespect to the depth of the proof DAG, and solvable in polynomial time with respect to several notions of width of the equations being proved. In this way we establish the polynomial time provability of equations that can be out of reach of techniques based on completion and heuristic search. / <p>QC 20131120</p>

El Desarrollo de Software Dirigido por Modelos es una rama de la Ingeniería del Software en la que los artefactos software se representan como modelos para incrementar la productividad, calidady eficiencia económica en el proceso de desarrollo de software, donde un modelo proporciona una representación abstracta del código final de una aplicación. En este campo, la iniciativa Model-Driven Architecture (MDA), patrocinada por la OMG, está constituida por una familia de estándares industriales, entre los que se destacan: Meta-Object Facility (MOF), Unified Modeling Language (UML), Object Constraint Language (OCL), XML Metadata Interchange (XMI), y Query/Views/Transformations (QVT). Estos estándares proporcionan unas directrices comunes para herramientas basadas en modelos y para procesos de desarrollo de software dirigidos por modelos. Su objetivo consiste en mejorar la interoperabilidad entre marcos de trabajo ejecutables, en automatizar el proceso desarrollo de software de software y en proporcionar técnicas que eviten errores durante ese proceso. El estándar MOF describe un marco de trabajo genérico que permite definir la sintaxis abstracta de lenguajes de modelado. Este estándar persigue la definición de los conceptos básicos que son utilizados en procesos de desarrollo de software dirigidos por modelos: que es un modelo, que es un metamodelo, qué es reflexión en un marco de trabajo basado en MOF, etc. Sin embargo, la mayoría de estos conceptos carecen de una semántica formal en la versión actual del estándar MOF. Además, OCL se utiliza como un lenguage de definición de restricciones que permite añadir semántica a un metamodelo MOF. Desafortunadamente, la relación entre un metamodelo y sus restricciones OCL también carece de una semántica formal. Este hecho es debido, en parte, a que los metamodelos solo pueden ser definidos como dato en un marco de trabajo basado en MOF. El estándar MOF también proporciona las llamadas facilidades de reflexión de MOF (MOF Reflecti / Boronat Moll, A. (2007). A formal framework for model management [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/1964