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: | |
---|---|
Formato: | Tesis de Grado |
Lenguaje: | Español |
Publicado: |
Sept
|
Materias: | |
Acceso en línea: | https://hdl.handle.net/20.500.12110/seminario_nCOM000441_Brassesco |
Aporte de: |
id |
todo:seminario_nCOM000441_Brassesco |
---|---|
record_format |
dspace |
spelling |
todo:seminario_nCOM000441_Brassesco2023-10-03T16:48:30Z Síntesis concurrente de controladores para juegos definidos con objetivos de Generalized Reactivity (1) Concurrent synthesis for controllers designed with generalized reactivity (1) Brassesco, María Virginia CONCURRENCIA DISEÑO SINTETIZADO LTS CONTROLADORES REACTIVIDAD GENERALIZADA PEQUEÑA MEDIDA DE PROGRESO CONCURRENT DESIGN SYNTHESIS CONTROLLERS GENERALIZED REACTIVITY SMALL PROGRESS MEASURES 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. Septiembre de 2017 Tesis de Grado PDF Español info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar https://hdl.handle.net/20.500.12110/seminario_nCOM000441_Brassesco |
institution |
Universidad de Buenos Aires |
institution_str |
I-28 |
repository_str |
R-134 |
collection |
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) |
language |
Español |
orig_language_str_mv |
Español |
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. |
format |
Tesis de Grado |
author |
Brassesco, María Virginia |
author_facet |
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) |
publishDate |
Sept |
url |
https://hdl.handle.net/20.500.12110/seminario_nCOM000441_Brassesco |
work_keys_str_mv |
AT brassescomariavirginia sintesisconcurrentedecontroladoresparajuegosdefinidosconobjetivosdegeneralizedreactivity1 AT brassescomariavirginia concurrentsynthesisforcontrollersdesignedwithgeneralizedreactivity1 |
_version_ |
1807319815202799616 |