Autómatas estocásticos para sistemas concurrentes y tolerantes a fallas
Tesis (Doctor en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2018.
Main Author: | |
---|---|
Other Authors: | |
Format: | doctoralThesis |
Language: | spa |
Published: |
2023
|
Subjects: | |
Online Access: | http://hdl.handle.net/11086/549542 |
_version_ | 1801213524719960064 |
---|---|
author | Monti, Raúl Enrique |
author2 | D'Argenio, Pedro Rubén |
author_facet | D'Argenio, Pedro Rubén Monti, Raúl Enrique |
author_sort | Monti, Raúl Enrique |
collection | Repositorio Digital Universitario |
description | Tesis (Doctor en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2018. |
format | doctoralThesis |
id | rdu-unc.549542 |
institution | Universidad Nacional de Cordoba |
language | spa |
publishDate | 2023 |
record_format | dspace |
spelling | rdu-unc.5495422023-12-05T11:54:13Z Autómatas estocásticos para sistemas concurrentes y tolerantes a fallas Monti, Raúl Enrique D'Argenio, Pedro Rubén Hermanns, Holger Automata Concurrencia Determinismo Simulación Confluencia Probabilidades continuas Formal languages and automata theory Automata over infinite objects Quantitative automata Models of computation Concurrency Timed and hybrid models Logic Verification by model checking Tesis (Doctor en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2018. Fil: Monti, Raúl Enrique. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. En esta tesis introducimos una nueva clase de autómata llamada Input/Output Stochastic Automata (IOSA). Los IOSA son composicionales, y los IOSA cerrados (sin acciones de entrada) son completamente deterministas y por lo tanto aptos para simulación. Esto los hace atractivos para analizar sistemas probabilistas complejos, que son imprácticos de analizar por Model Checking. Una segunda versión de IOSA introduce al modelo acciones urgentes, con el fin de mejorar la composicionalidad del modelo. Esta extensión introduce no-determinismo también el los modelos cerrados. Logramos distinguir no-determinismo espurio producido por acciones confluentes. Sumado a esto, proveemos condiciones suficientes para asegurar que una red de IOSAs que interactúan es determinista sin la necesidad de analizar el modelo compuesto. Finalmente, usamos IOSA con acciones urgentes para definir una semántica formal para Repairable Fault Trees (RFT), una técnica muy efectiva para el análisis de modelos industriales. Probamos que la semántica es determinista, y analizamos un caso de estudio usando el simulador de eventos raros FIG. In this thesis we introduce a new class of automata called Input/Output Stochastic Automata (IOSA). IOSAs are compositional, and closed IOSAs (no input actions) are fully deterministic and therefore suitable for simulation. This makes them attractive for analyzing complex probabilistic systems, which are impractical to analyze by Model Checking. A second version of IOSA introduces urgent actions to the model, in order to improve the compositionality of the model. This extension introduces non-determinism also in closed models. We managed to distinguish spurious non-determinism produced by confluent actions. Added to this, we provide sufficient conditions to ensure that a network of interacting IOSAs is deterministic without the need to analyze the composite model. Finally, we use IOSA with urgent actions to define a formal semantics for Repairable Fault Trees (RFTs), a very effective technique for industrial model analysis. We prove that the semantics are deterministic, and we analyze a case study using the rare event simulator FIG. Fil: Monti, Raúl Enrique. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. 2023-10-19T12:57:05Z 2023-10-19T12:57:05Z 2018-12 doctoralThesis http://hdl.handle.net/11086/549542 spa Atribución 4.0 Internacional http://creativecommons.org/licenses/by/4.0/ |
spellingShingle | Automata Concurrencia Determinismo Simulación Confluencia Probabilidades continuas Formal languages and automata theory Automata over infinite objects Quantitative automata Models of computation Concurrency Timed and hybrid models Logic Verification by model checking Monti, Raúl Enrique Autómatas estocásticos para sistemas concurrentes y tolerantes a fallas |
title | Autómatas estocásticos para sistemas concurrentes y tolerantes a fallas |
title_full | Autómatas estocásticos para sistemas concurrentes y tolerantes a fallas |
title_fullStr | Autómatas estocásticos para sistemas concurrentes y tolerantes a fallas |
title_full_unstemmed | Autómatas estocásticos para sistemas concurrentes y tolerantes a fallas |
title_short | Autómatas estocásticos para sistemas concurrentes y tolerantes a fallas |
title_sort | automatas estocasticos para sistemas concurrentes y tolerantes a fallas |
topic | Automata Concurrencia Determinismo Simulación Confluencia Probabilidades continuas Formal languages and automata theory Automata over infinite objects Quantitative automata Models of computation Concurrency Timed and hybrid models Logic Verification by model checking |
url | http://hdl.handle.net/11086/549542 |
work_keys_str_mv | AT montiraulenrique automatasestocasticosparasistemasconcurrentesytolerantesafallas |