Compilación de model checking probabilístico en la planificación probabilística

Anteriormente se ha observado que la verificación de propiedades de seguridad en marcos deterministas de model checking se puede compilar en la planificación clásica. Existe una conexión similar entre el análisis de probabilidad objetivo en cualquier lado, pero esa conexión no se ha explorado. Llenamos esa brecha con una traducción de Jani, un lenguaje de entrada para verificadores de modelos(model checkers) cuantitativos que incluye el conjunto de herramientas Modest y PRISM, en PPDDL. Nuestros experimentos motivan una mayor fertilización cruzada entre ambas áreas de investigación, específicamente el intercambio de algoritmos. Nuestro estudio también inicia la creación de nuevos puntos de referencia para el análisis de probabilidad de objetivos.

Este post es una traducción de Compiling Probabilistic Model Checking into Probabilistic Planning

• Título original: Compiling Probabilistic Model Checking into Probabilistic Planning
• Autores: Michaela Klauck , Marcel Steinmetz, Jorg Hoffmann y Holger Hermanns
• Año: 2018