Síntesis concurrente de controladores para juegos definidos con objetivos de Generalized Reactivity(1)

Se describe un algoritmo concurrente para resolver juegos de tipo: Generalized Reactivity (1), con aplicación a síntesis de controladores. El algoritmo esta basado en Jurdzinski’s Small Progress Measures. Utiliza estructuras de acceso concurrente para optimizar las lecturas y cuenta con bloqueos de...

Descripción completa

Detalles Bibliográficos
Autor principal: Brassesco, María Virginia
Otros Autores: D’Ippolito, Nicolás Roque
Formato: Tesis de grado publishedVersion
Publicado: Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2017
Materias:
LTS
Acceso en línea:https://hdl.handle.net/20.500.12110/seminario_nCOM000441_Brassesco
http://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000441_Brassesco_oai
Aporte de:
id I28-R145-seminario_nCOM000441_Brassesco_oai
record_format dspace
spelling I28-R145-seminario_nCOM000441_Brassesco_oai2023-08-29 D’Ippolito, Nicolás Roque Brassesco, María Virginia 2017-09-26 Se describe un algoritmo concurrente para resolver juegos de tipo: Generalized Reactivity (1), con aplicación a síntesis de controladores. El algoritmo esta basado en Jurdzinski’s Small Progress Measures. Utiliza estructuras de acceso concurrente para optimizar las lecturas y cuenta con bloqueos de escritura. El siguiente trabajo muestra la implementación del algoritmo de estabilización de punto fijo de forma concurrente, para cálculo de ranking. La implementación se realizó y verificó sobre la herramienta MTSA [DL15]. Se analizaron implementaciones conocidas basadas en Small Progress Measures [HPK11] [vdPW08a]. Se adaptó la implementación para poder calcular ranking utilizando los teoremas conocidos de equivalencias entre juegos de paridad y GR1 [GWT02]. Se reportan comparaciones sobre los resultados obtenidos. This work describes a concurrent algorithm to solve Generalized Reactivity (1) games with its application to controller synthesis. The algorithm is based on Jurdzinski’s Small Progress Measures (SPM). It uses concurrent structures to optimize reads and some write locks. The following work shows the implementation of the fixed point recucurrent algorithm to compute the ranking in a concurrent way. The implementation was done and verified on MTSA tool [DFCU08b]. Different known implementations based on SPM where analized [vdPW08a]. The implementation was adapted to calculate the ranking using known theorems based on GR1 and parity games equivalencies [GWT02]. A result comparisson was also reported. Fil: Brassesco, María Virginia. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. application/pdf https://hdl.handle.net/20.500.12110/seminario_nCOM000441_Brassesco Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar CONCURRENCIA DISEÑO SINTETIZADO LTS CONTROLADORES REACTIVIDAD GENERALIZADA PEQUEÑA MEDIDA DE PROGRESO CONCURRENT DESIGN SYNTHESIS CONTROLLERS GENERALIZED REACTIVITY SMALL PROGRESS MEASURES Síntesis concurrente de controladores para juegos definidos con objetivos de Generalized Reactivity(1) Concurrent synthesis for controllers designed with generalized reactivity (1) info:eu-repo/semantics/bachelorThesis info:ar-repo/semantics/tesis de grado info:eu-repo/semantics/publishedVersion http://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000441_Brassesco_oai
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-145
collection Repositorio Digital de la Universidad de Buenos Aires (UBA)
topic CONCURRENCIA
DISEÑO SINTETIZADO
LTS
CONTROLADORES
REACTIVIDAD GENERALIZADA
PEQUEÑA MEDIDA DE PROGRESO
CONCURRENT
DESIGN SYNTHESIS
CONTROLLERS
GENERALIZED REACTIVITY
SMALL PROGRESS MEASURES
spellingShingle CONCURRENCIA
DISEÑO SINTETIZADO
LTS
CONTROLADORES
REACTIVIDAD GENERALIZADA
PEQUEÑA MEDIDA DE PROGRESO
CONCURRENT
DESIGN SYNTHESIS
CONTROLLERS
GENERALIZED REACTIVITY
SMALL PROGRESS MEASURES
Brassesco, María Virginia
Síntesis concurrente de controladores para juegos definidos con objetivos de Generalized Reactivity(1)
topic_facet CONCURRENCIA
DISEÑO SINTETIZADO
LTS
CONTROLADORES
REACTIVIDAD GENERALIZADA
PEQUEÑA MEDIDA DE PROGRESO
CONCURRENT
DESIGN SYNTHESIS
CONTROLLERS
GENERALIZED REACTIVITY
SMALL PROGRESS MEASURES
description Se describe un algoritmo concurrente para resolver juegos de tipo: Generalized Reactivity (1), con aplicación a síntesis de controladores. El algoritmo esta basado en Jurdzinski’s Small Progress Measures. Utiliza estructuras de acceso concurrente para optimizar las lecturas y cuenta con bloqueos de escritura. El siguiente trabajo muestra la implementación del algoritmo de estabilización de punto fijo de forma concurrente, para cálculo de ranking. La implementación se realizó y verificó sobre la herramienta MTSA [DL15]. Se analizaron implementaciones conocidas basadas en Small Progress Measures [HPK11] [vdPW08a]. Se adaptó la implementación para poder calcular ranking utilizando los teoremas conocidos de equivalencias entre juegos de paridad y GR1 [GWT02]. Se reportan comparaciones sobre los resultados obtenidos.
author2 D’Ippolito, Nicolás Roque
author_facet D’Ippolito, Nicolás Roque
Brassesco, María Virginia
format Tesis de grado
Tesis de grado
publishedVersion
author Brassesco, María Virginia
author_sort Brassesco, María Virginia
title Síntesis concurrente de controladores para juegos definidos con objetivos de Generalized Reactivity(1)
title_short Síntesis concurrente de controladores para juegos definidos con objetivos de Generalized Reactivity(1)
title_full Síntesis concurrente de controladores para juegos definidos con objetivos de Generalized Reactivity(1)
title_fullStr Síntesis concurrente de controladores para juegos definidos con objetivos de Generalized Reactivity(1)
title_full_unstemmed Síntesis concurrente de controladores para juegos definidos con objetivos de Generalized Reactivity(1)
title_sort síntesis concurrente de controladores para juegos definidos con objetivos de generalized reactivity(1)
publisher Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
publishDate 2017
url https://hdl.handle.net/20.500.12110/seminario_nCOM000441_Brassesco
http://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000441_Brassesco_oai
work_keys_str_mv AT brassescomariavirginia sintesisconcurrentedecontroladoresparajuegosdefinidosconobjetivosdegeneralizedreactivity1
AT brassescomariavirginia concurrentsynthesisforcontrollersdesignedwithgeneralizedreactivity1
_version_ 1782033784922701824