1,721,030 research outputs found
Semánticas de pruebas para álgebras de procesos probabilísticos
Full text linkTesis de la Universidad Complutense de Madrid, Facultad de Ciencias Matemáticas, leída el 25-06-1996En esta tesis presentamos un algebra de procesos que ha sido extendida con información probabilística. Definimos una semántica operacional para nuestro lenguaje, y a continuación definimos una semántica de pruebas parametrizadas por una cierta familia de pruebas. La caracterización vendrá dada por la probabilidad con la que los procesos pasan las pruebas del conjunto dado. Una vez definido el marco general, consideraremos dos conjuntos de pruebas los cuales estarán asociados a una interpretación de los modelos reactivos y generativo respectivamente. Para la interpretación del modelo reactivo daremos una caracterización alternativa de la semántica pruebas, la cual esta basada en trazas probabilísticas. Dado que el operador de elección externa no es congruente, definimos una semántica denotacional para el lenguaje en el que no se considera la elección externa. Esta semántica denotacional es completamente abstracta con respecto a la semántica de pruebas. Para la interpretación generativa, definimos una caracterización alternativa basada en conjuntos de aceptación probabilísticos y una semántica denotacional basada en árboles de aceptación probabilísticos. Además, para este modelo definimos una semántica axiomatica. Demostramos que todas estas semánticas son equivalentes a la semántica de pruebas para el modelo generativo. A continuación damos una serie de ejemplos en los cuales mostramos la utilidad de nuestro lenguaje a la hora de especificar sistemas concurrentes que dependen de información probabilística. Finalizamos extendiendo nuestro lenguaje con un operador de composición paralela y discutiendo los problemas que presenta incluir un operador de restricción.Sección Deptal. de Sistemas Informáticos y ComputaciónFac. de Ciencias MatemáticasTRUEpu
Jugando con el tiempo : semántica de pruebas para algebras de procesos temporizadas
No full textTesis de la Universidad Complutense de Madrid, Facultad de Ciencias Matemáticas, leída el 25-06-1996en el presente trabajo hemos estudiado la semántica de pruebas para alebras de procesos temporizadas. En primer lugar hemos estudiado un álgebra de procesos temporizada básica, se trata de un lenguaje recursivo, secuencial no determinista. Puesto que las semánticas de pruebas son poco manejables, se hace necesario dar una caracterización alternativa de la misma; nosotros hemos dado una caracterizacion que depende unicamente de la semántica operacional de álgebra. A continuación hemos dotado al álgebra de una semántica denotacional, que ha resultado ser completamente abstracta con respecto a la semántica de pruebas. Seguidamente hemos estudiado una semántica axiomática, puesto que conseguimos probar que esta ultima es correcta y completa con respecto a la semántica detonaciones tenemos inmediatamente que tambien será correcta y completa con respecto a la semántica de pruebas. Puesto que todo lo anterior lo habíamos hecho con un álgebra bastante simple, es necesario introducir operadores mas complejos. En concreto hemos estudiado una serie de operadores que aparecen en la mayoria de las alebras de procesos temporizadas: . El operador de paralelo. El operador de ocultamiento, y. El operador de prefijo mediante acción visible con intervalo de tiempo. Por ultimo hemos estudiado un operador de elección tipo ccs, que tiene los problemas típicos con respecto a la congruenciaFac. de Ciencias MatemáticasTRUEpu
Revisiting logical semantics for processes and their distances
Full text linkTesis inédita de la Universidad Complutense de Madrid, Facultad de Informática, Departamento de Sistemas Informáticos y Computación, leída el 2-02-2016Esta tesis se enmarca en el amplio campo de la teoría de la concurrencia. Más específicamente, nos centramos en el estudio de las relaciones de similitud entre procesos concurrentes. Comenzamos estudiando la bisimulación, considerada la más importante de estas relaciones, y vemos después cómo podemos extender nuestros resultados al resto de las semánticas de procesos estudiadas durante las últimas décadas. En particular, nuestra contribución a la comunidad científica, se centra en dos puntos principales: – El desarrollo de una caracterización lógica uniforme de las semánticas de procesos: proponemos un esquema lógico común (enmarcado en la conocida lógica modal de Hennessy-Milner) e incluimos las diferentes semánticas en este esquema, enfatizando las diferencias y similitudes entre ellas, que se presentan del modo más claro posible. – La presentación de una nueva noción de distancia, tanto entre procesos finitos como infinitos: la misma se diferencia de las anteriormente propuestas en su carácter global, que acumula las diferencias que aportan los distintos cómputos, en lugar de quedarnos con la máxima de ellas...This thesis can be included in the broad field of concurrency theory. More specifically, we focus on the study of the similarities between concurrent processes. We start from bisimulation, the main of these relations, and then we see how we can extend the obtained results to the rest of the semantics developed along the last years. In particular, our main contributions can be roughly described by the following two items: – The development of a unified logical characterization of process semantics: we propose a common logical scheme (within the framework of the well known Hennessy-Milner Logic) and we set the different semantics in this scheme by emphasizing, in the clearest possible way, the (dis)similarities between them. – We present a new notion of distance for both finite and infinite processes. This novel notion differs from the previously available ones in its global character: instead of taking the maximum disagreement between the two compared processes, it adds all the differences provided by their whole sets of computations...Depto. de Sistemas Informáticos y ComputaciónFac. de InformáticaTRUEunpu
Decibilidad de problemas sobre redes de Petri temporizadas
No full textTesis de la Universidad Complutense de Madrid, Facultad de Ciencias Matemáticas, S.D.Informática y Automática, leída el 07-05-1993La tesis investiga cuestiones de decibilidad sobre distintos variantes de redes de Petri temporizados. Se detiene diversas extensiones de las propiedades clásicas de redes de Petri, a los modelos temporizados, se consideran, asimismo distintas hipótesis sobre el tipo de modelo temporal: discreto, racional, real etc.. El trabajo se encuadra en una línea de investigación de acrualidad y los resutados obtenidos son interesantes, numerosos y originalesFac. de Ciencias MatemáticasTRUEpu
Caracterizaciones lógicas uniformes de las semánticas de procesos
Full text linkMáster en Investigación en Informática, Facultad de Informática, Departamento de Sistemas Informáticos y computación, curso 2009-2010El trabajo más importante de catalogación y clasificación de las semánticas de procesos fue llevado a cabo por R. J. van Glabbeek. En su artículo titulado "Linear time-branching time spectrum", recopiló las principales semánticas, estableciendo una clasificación basada en el poder de distinción de las mismas. Las caracterizaciones que aparecen en dicho artículo se realizan mediante fórmulas lógicas y axiomatizaciones fundamentalmente. Sin embargo,si bien el trabajo tiene un cierto carácter enciclopédico,se echa en falta notablemente la uniformidad a la hora de desarrollar las caracterizaciones de las distintas semánticas. La búsqueda de caracterizaciones uniformes fue uno de los temas centrales de la Tesis Doctoral de C. Gregorio, en la que, partiéndose de la diferencia entre las semánticas de simulación, y las semánticas lineales se encontraron los mecanismos que permiten unificar tanto las caracterizaciones observacionales como las axiomáticas. El objetivo central de este trabajo ha consistido en completar la labor de unificacación anterior, extendiéndola al campo de las semánticas lógicas, donde de nuevo, hemos encontrado caracterizaciones similares a las de van Glabbeek, pero desarrolladas en un marco uniforme del que distan las originalmente obtenidas.
[ABSTRACT]
The most important work to classify process semantics was developed by R. J. van Glabbeek, in his paper "Linear time-branching time spectrum", where he collects the most important process semantics, classifying them with respect to their discriminating power. His semantics are dened both by means of an adequate logic and a complete axiomatization. However the most important objection that we could make to his work was the lack of uniformity. The search of uniform characterizations of all the process semantics was one of the central topics of C. Gregorios PhD Thesis where he develops both uniform presentation of the observational semantics and of their axiomatizations. Our main objective here is to complete this unification work by providing a uniform logical characterization of all the semantics in the spectrum. Starting from the logic semantics provided by van Glabbeek we have obtained simple new logics that give us additional knowledge about the structure of the extended ltbt-spectrum.Depto. de Sistemas Informáticos y ComputaciónFac. de InformáticaFALSEunpu
CSP Probabilístico (PCSP) : un modelo probabilístico de procesos concurrentes
Full text linkTesis de la Universidad Complutense de Madrid, Facultad de Ciencias Matemáticas, S.D. de Informática y automatica, leída el 12-11-1993El trabajo consiste en un enriquecimiento con probabilidades del modelo algebraíco CSP (Comumnications Sequential Processes), [Hoare 85]. Se asocian probabilidades a los operadores de elección extena e interna. Se espera con ello mejorar la capacidad de razonar sobre las propiedades de un sistema concurrente. Se precisa el modelo resultante de esta idea y se dota al lenguaje de cuatro semánticas con enfoques respectivamente operacional, de pruebas, denotaciones y algebraico. Se demuestra que las cuatro semánticas son equivalentesFac. de Ciencias MatemáticasTRUEpu
Towards verifying Petri Nets: a model cheking approach
Full text linkMáster en Investigación en Informática, Facultad de Informática, Departamento de Sistemas Informáticos y computación, curso 2009-2010Las redes de Petri son un importante formalismo para la especificación de sistemas concurrentes y distribuídos. Tal y como se hace con otros formalismos, como los autómatas finitos, nos gustaría poder verificar formal y automáticamente ciertas propiedades sobre los sistemas representados mediante redes de Petri. Este problema
se denomina "model checking" (o comprobación de modelos). En este trabajo hemos hecho una recopilación de los principales resultados sobre model checking para redes de Petri y dos de sus principales extensiones monótonas que son ortogonales: las redes reset y las ν-PNs. Comenzamos con una pequeña introducción a las redes de Petri, sus extensiones y los principales resultados de decidibilidad
sobre estas, que sirven para demostrar cuestiones sobre model checking. Una de las principales tareas realizadas en este trabajo ha sido identicar resultados sobre model checking para otros formalismos y adaptarlos a las extensiones de redes de Petri anteriormente citadas. A pesar de la naturaleza eminentemente bibliográfica del trabajo, presentamos también algunos resultados originales. En particular, se da una demostración de la indecidibilidad del recubrimiento repetido para ν-PNs y de aquí se deduce la indecidibilidad del problema de model-checking para cierta lógica temporal para ν-Petri nets. Finalmente, al encontrarnos con que todas las lógicas temporales consideradas son indecidibles para las redes reset y las ν-
PNs, discutimos cómo enfrentarnos al problema del model checking en el caso indecidible, mediante dos técnicas diferentes: el unfolding y el cómputo del cover.
[ABSTRACT]
Petri nets are an important formalism to specify concurrent and distributed systems. When Petri nets are used to model systems, we would like to be able to verify certain properties about the modelled systems automatically, as is done when other formalisms, as nite automata, are applied. This problem is called the "model checking" problem. In this work, we present a compilation of the main model checking results for plain Petri nets and two orthogonal monotonic extensions: reset Petri nets and ν-Petri nets. We rst introduce Petri nets and its extensions, and summarize the main decidability results for them, which are
useful in proving decidability issues about model checking. An important part of the work has been looking for model checking results about other formalisms (in particular lossy VASS with inhibitor arcs) which are applicable to reset nets and ν-Petri nets. Despite the fact that this work is eminently bibliographic, some new results are proved here. In particular, a proof for the undecidability of the repeated coverability problem for ν-Petri nets is given, and we use this result to prove the undecidability of model checking certain temporal logic for ν-Petri
nets. Finally, as all the considered temporal logics for reset nets and ν-Petri nets are undecidable, we discuss how to approach the model checking problem in the undecidable case with two different techniques: unfolding and cover computation.Depto. de Sistemas Informáticos y ComputaciónFac. de InformáticaFALSEunpu
Algorithms for minimal coverability set of Petri Nets
No full textTrabajo de Fin de Máster en Métodos Formales en Ingeniería Informática, Facultad de Informática UCM, Departamento de Sistemas Informáticos y Computación, Curso 2022/2023.Desde que Carl Adam Petri definió las Redes de Petri en los años 60, estas han sido una herramienta muy utilizada para modelar y analizar sistemas concurrentes, sirviendo como una representación gráfica que describe la dinámica de sistemas complejos, lo que las convierte en un recurso esencial en las Ciencias de la Computación. Uno de los problemas centrales en el análisis de redes de Petri es la determinación de su comportamiento y su capacidad de alcanzar diferentes estados. El árbol de cobertura, es una estructura de datos crucial en este contexto, ya que representa de manera eficiente una aproximación compacta útil del conjunto de estados a los que puede llegar una red de Petri durante su ejecución. Sin embargo, calcular el árbol de mínima cobertura de una red de Petri, que proporciona una visión más concisa y simplificada de su comportamiento, es una tarea computacionalmente desafiante. En este trabajo exploraremos los algoritmos de Finkel, CovProc, un algoritmo que computa el conjunto de mínima cobertura utilizando el algoritmo de Tarjan (StackProc), Poda-Monótona y MinCov, desarrollados con el propósito de calcular el conjunto de mínima cobertura de una Red de Petri. Cada uno de estos enfoques ha sido diseñado para abordar este problema desde una perspectiva diferente, buscando optimizar la eficiencia y la precisión del resultado. Estos cuatro algoritmos se examinarán en detalle presentando sus fundamentos teóricos y analizando su eficacia y eficiencia. Así, tendremos una visión completa de los algoritmos que se han desarrollado para calcular el conjunto de mínima cobertura de las redes de Petri.Since Carl Adam Petri defined Petri Nets in the 1960s, they have been a highly useful tool for modeling and analyzing concurrent systems, serving as a graphical representation that describes the dynamics of complex systems, making them an essential asset in computer science research. One of the central challenges in the analysis of Petri nets is determining their behavior and their ability to reach different states. The coverability tree is a crucial data structure in this context as it efficiently represents a compact approximation of the set of states a Petri net can reach during its execution. However, calculating the minimal coverability tree of a Petri net, which provides a more concise and simplified view of its behavior, is a computationally challenging task. In this work, we will explore the algorithms of Finkel, CovProc, a minimal coverability set algorithm that uses Tarjan’s algorithm (StackProc), Monotonic-Prunning and MinCov developed for the purpose of calculating the minimal coverability set of a Petri Net. Each of these approaches has been designed to address this problem from a different perspective, aiming to optimize efficiency and result accuracy. These five algorithms will be examined in detail, presenting their theoretical foundations and analyzing their effectiveness and efficiency. Thus, we will have a comprehensive view of the algorithms that have been developed to calculate the minimal coverability set of Petri nets.Depto. de Sistemas Informáticos y ComputaciónFac. de InformáticaTRUEunpu
Técnicas Coalgebraicas y Categóricas para el estudio de las semánticas de procesos
Full text linkTesis inédita de la Universidad Complutense de Madrid, Facultad de Ciencias Matemáticas, Departamento de Sistemas Informáticos y Programación, leída el 16-03-2012De un modo general, esta tesis puede englobarse dentro del estudio de los sistemas de procesos y, muy especialmente, del estudio de las relaciones entre esos procesos mediante
bisimulación y simulación (abreviadamente (bi)simulación). Además, los resultados que aquí aparecen están sustentados en gran parte por el marco general de la teoría de
categorías y, más concretamente, en el de las coálgebras en el que Jesse Hughes y Bart Jacobs propusieron una definición general de simulación entre coálgebras. La noción de simulación entre coálgebras se apoya en los conceptos de orden funtorial y alzamiento de relaciones; la bisimulación entre coálgebras es un caso particular de simulación (en la que el orden funtorial es la igualdad).
La (bi)simulación coalgebraica permite disponer de un único concepto general cuyas instancias definen las nociones concretas para sistemas de transiciones (LTS), estructuras
de Kripke, etc. No obstante no todo orden funtorial define una relación de similitud correcta pues, en concreto, es necesario que se cumpla la condición de estabilidad para
asegurar que la composición de simulaciones es también una simulación, y así garantizar que la similitud sea una relación transitiva. Podemos considerar dos partes esenciales en esta tesis: en la primera explotamos la
potencia de la definición coalgebraica de simulación para obtener resultados generales, mientras que en la segunda nos centramos en el estudio de dos nuevas nociones de simulación que hemos propuesto, pero en esta ocasión desde un punto de vista más clásico al estilo de los resultados de van Glabbeek. En primer lugar, estudiamos bajo qué condiciones las instancias de dichas nociones
categóricas generales de (bi)simulación permiten traspasar propiedades entre las estructuras relacionadas, es decir, en qué condiciones se puede generalizar al mundo coalgebraico los resultados clásicos de reflexión y preservación de propiedades lógicas mediante bisimulaciones,
y la preservación mediante simulaciones. Nuestra conclusión es que, si bien para el caso de las bisimulaciones se obtiene la deseada generalización, para el caso de la
simulación es necesario restringir los órdenes que participan en la definición de simulación propuesta de Hughes y Jacobs, obteniéndose en este caso resultados parciales. También estudiamos cómo las transformaciones naturales entre funtores permiten unificar nociones de (bi)simulación entre distintos tipos de estructuras, obteniendo resultados de representación de las coálgebras entre los distintos funtores relacionados por la transformación natural. En particular, unificamos los sistemas probabilísticos y los sistemas de transiciones en el modelo de los sistemas de multitransiciones. Para finalizar la primera parte de la tesis, profundizamos en el estudio de la no ción de simulación coalgebraica y de la condición necesaria de estabilidad, para llegar a entender cómo se pueden definir nociones de simulación dentro del marco coalgebraico que definan relaciones de similitud con buenas propiedades. En concreto, ilustramos nuestros resultados teóricos definiendo dos nuevas nociones de simulación sobre sistemas de transiciones etiquetados: la simulación covariante-contravariante (cc-simulación) y la
simulación conforme. La segunda parte de la tesis está dedicada al estudio de las dos nociones de simulación
que hemos nombrado. Para las dos nociones de simulación construimos su caracterización lógica y axiomática. Además, para el caso de la simulación covariante-contravariante,
estudiamos también su estrecha relación con los refinamientos modales sobre sistemas de transiciones modales (MTS) construyendo transformaciones de los LTS módulo ccsimulación y los MTS módulo refinamiento modal, y viceversa. Asimismo, construimos las fórmulas características de los LTS módulo cc-simulación y cómo estas representan procesos, es decir, la representación gráfica de las fórmulas.Sección Deptal. de Sistemas Informáticos y ComputaciónFac. de Ciencias MatemáticasTRUEunpu
Turing al servicio de sus Majestades: su rey y sus matemáticas
No full textDe entre las múltiples actividades que Alan Turing desarrolló en su lamentablemente muy corta vida, me centraré sobre todo en sus famosas actividades "Rompiendo el Código de Enigma", en las instalaciones secretas del Gobierno inglés radicadas en Bletchley Park. Dejando de lado las cuestiones relacionadas con las Máquinas de Turing, el Test de Turing y el desarrollo en sus albores de la Programación, complementaré mi charla con otros aspectos en los que aparecen contenidos matemáticos más clásicos, aunque aplicados también de un modo altamente revolucionario, hablando un poco sobre Inteligencia Artificial, Vida Artificial, Morfogénesis y Algoritmos Genéticos
- …
