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...
Autor principal: | |
---|---|
Otros Autores: | |
Formato: | Tesis de grado publishedVersion |
Publicado: |
Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
2017
|
Materias: | |
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 |