Model Repair Revamped - On the Automated Synthesis of Markov Chains -

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F19%3APU134974" target="_blank" >RIV/00216305:26230/19:PU134974 - isvavai.cz</a>

Výsledek na webu

<a href="https://www.researchgate.net/publication/335984637_Model_Repair_Revamped_-_On_the_Automated_Synthesis_of_Markov_Chains_-" target="_blank" >https://www.researchgate.net/publication/335984637_Model_Repair_Revamped_-_On_the_Automated_Synthesis_of_Markov_Chains_-</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-31514-6_7" target="_blank" >10.1007/978-3-030-31514-6_7</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Model Repair Revamped - On the Automated Synthesis of Markov Chains -

Popis výsledku v původním jazyce

This paper outlines two approaches-based on counterexample-guided abstraction refinement (CEGAR) and counterexample-guided inductive synthesis (CEGIS), respectively-to the automated synthesis of finite-state probabilistic models and programs. Our CEGAR approach iteratively partitions the design space starting from an abstraction of this space and refines this by a light-weight analysis of verification results. The CEGIS technique exploits critical subsystems as counterexamples to prune all programs behaving incorrectly on that input. We show the applicability of these synthesis techniques to sketching of probabilistic programs, controller synthesis of POMDPs, and software product lines.

Název v anglickém jazyce

Model Repair Revamped - On the Automated Synthesis of Markov Chains -

Popis výsledku anglicky

This paper outlines two approaches-based on counterexample-guided abstraction refinement (CEGAR) and counterexample-guided inductive synthesis (CEGIS), respectively-to the automated synthesis of finite-state probabilistic models and programs. Our CEGAR approach iteratively partitions the design space starting from an abstraction of this space and refines this by a light-weight analysis of verification results. The CEGIS technique exploits critical subsystems as counterexamples to prune all programs behaving incorrectly on that input. We show the applicability of these synthesis techniques to sketching of probabilistic programs, controller synthesis of POMDPs, and software product lines.

Druh

C - Kapitola v odborné knize

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2019

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název knihy nebo sborníku

From Reactive Systems to Cyber-Physical Systems

ISBN

978-3-030-31513-9

Počet stran výsledku

19

Strana od-do

107-125

Počet stran knihy

301

Název nakladatele

Springer International Publishing

Místo vydání

Cham

Kód UT WoS kapitoly

—