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
Formato: Tesis de Grado
Lenguaje:Español
Publicado: Sept
Materias:
LTS
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