{"id":131625,"date":"1996-01-01T00:00:00","date_gmt":"1996-01-01T00:00:00","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/contribucion-al-analisis-del-espacio-de-estados-de-especificaciones-lotos\/"},"modified":"1996-01-01T00:00:00","modified_gmt":"1996-01-01T00:00:00","slug":"contribucion-al-analisis-del-espacio-de-estados-de-especificaciones-lotos","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/ciencias-tecnologicas\/contribucion-al-analisis-del-espacio-de-estados-de-especificaciones-lotos\/","title":{"rendered":"Contribucion al analisis del espacio de estados de especificaciones lotos."},"content":{"rendered":"<h2>Tesis doctoral de <strong> David Larrabeiti L\u00f3pez <\/strong><\/h2>\n<p>La primera fase en la mayoria de los algoritmos de validacion y verificacion de protocolos de comunicaciones existentes consiste en la generacion del espacio de estados de una especificacion formal del sistema. El principal obstaculo a la aplicacion industrial de esta tecnica es la elevada complejidad de los algoritmos de validacion y el gran tama\u00f1o de los espacios de estados de los sistemas reales.  la tesis aborda este problema en el ambito del lenguaje lotos, con el desarrollo de una forma de representacion y un metodo de exploracion de estados compactos con diversas aplicaciones. El modelo propuesto permite una representacion compacta del paralelismo, aliviando el problema de la explosion de estados derivados de la semantica de entrelazamiento de lotos. El algoritmo que transforma cualquier expresion lotos en una expresion equivalente en el nuevo calculo se denomina expansion entrelazada. La expansion entrelazada genera una representacion del sistema de transiciones donde los comportamientos entrelazantes son aislados, factorizados y conservados sin expandir. Esta representacion supone una reduccion de tama\u00f1o importante frente a la representacion extensiva del sistema de transiciones, en aquellas especificaciones con un alto grado de entrelazamiento. Es por tanto adecuado para especificaciones escritas en estilo orientado a recursos donde el problema de la explosion de estados es mas frecuente e intenso.  el desarrollo contiene la extension del modelo a lotos completo y la comparacion con algunos modelos con semanticas de concurrencia real relacionados, como las redes de petri y las estructuras de eventos. Finalmente se estudia un mecanismo de exploracion de estados que conserva la factorizacion de entrelazamiento y que es compatible con metodos de reduccion basados en conjuntos de eventos persistentes. La implementacion de la expansion entrelazada ha permitido contrastar empiricamente los resultados sobre especificacione<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Contribucion al analisis del espacio de estados de especificaciones lotos.<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Contribucion al analisis del espacio de estados de especificaciones lotos. <\/li>\n<li><strong>Autor:<\/strong>\u00a0 David Larrabeiti L\u00f3pez <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 Polit\u00e9cnica de Madrid<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 01\/01\/1996<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n<h3>Direcci\u00f3n y tribunal<\/h3>\n<ul>\n<li><strong>Director de la tesis<\/strong>\n<ul>\n<li>Juan Quemada Vives<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal: Gonzalo Le\u00f3n Serrano <\/li>\n<li>David De Frutos (vocal)<\/li>\n<li>Martin Llamas Nistal (vocal)<\/li>\n<li>Jorge Mataix Oltra (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de David Larrabeiti L\u00f3pez La primera fase en la mayoria de los algoritmos de validacion y verificacion de [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"site-sidebar-layout":"default","site-content-layout":"","ast-site-content-layout":"","site-content-style":"default","site-sidebar-style":"default","ast-global-header-display":"","ast-banner-title-visibility":"","ast-main-header-display":"","ast-hfb-above-header-display":"","ast-hfb-below-header-display":"","ast-hfb-mobile-header-display":"","site-post-title":"","ast-breadcrumbs-content":"","ast-featured-img":"","footer-sml-layout":"","theme-transparent-header-meta":"","adv-header-id-meta":"","stick-header-meta":"","header-above-stick-meta":"","header-main-stick-meta":"","header-below-stick-meta":"","astra-migrate-meta-layouts":"default","ast-page-background-enabled":"default","ast-page-background-meta":{"desktop":{"background-color":"var(--ast-global-color-4)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"ast-content-background-meta":{"desktop":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"footnotes":""},"categories":[332,18667,16008,2535,2206],"tags":[96011,45848,16198,16544,16199,30775],"class_list":["post-131625","post","type-post","status-publish","format-standard","hentry","category-ciencias-tecnologicas","category-diseno-de-sistemas-de-calculo","category-politecnica-de-madrid","category-tecnologia-de-los-ordenadores","category-tecnologia-energetica","tag-david-de-frutos","tag-david-larrabeiti-lopez","tag-gonzalo-leon-serrano","tag-jorge-mataix-oltra","tag-juan-quemada-vives","tag-martin-llamas-nistal"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/131625","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/comments?post=131625"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/131625\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=131625"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=131625"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=131625"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}