Abstrakt. Med tanke på en Kripke struktur M och CTL formel, där M inte uppfyller  och, problemet med Model Repair är att få en ny modell M sådan att M uppfyller  och. Dessutom bör ändringarna till M för att härleda M vara minimala med avseende på alla sådana M. Som vid modellkontroll kan tillståndsexplosion göra det praktiskt taget omöjligt att utföra modellreparationer på modeller med oändliga eller till och med stora tillståndsutrymmen. I detta dokument presenterar vi en ram för modellreparationer som använder abstraktion förfining för att ta itu med statsexplosion. Vårt ramverk syftar till att reparera Kripke Structure modeller baserade på en Kripke Modal Transition System abstraktion och en 3-värderad semantik för CTL. Vi introducerar en abstrakt modellreparationsalgoritm för vilken vi bevisar sundhet och halvfullkomlighet, och vi studerar dess komplexitetsklass. Dessutom presenteras en prototypimplementering för att illustrera den praktiska nyttan av abstrakt-modell-reparation på en Automatic Door Opener-systemmodell och en modell av Andrew File System 1-protokollet.
Chatzieftheriou m.fl. Detta beslut träder i kraft dagen efter det att det har offentliggjorts i Europeiska unionens officiella tidning. REF presenterar en metod för att reparera abstrakta strukturer med hjälp av Kripke modal övergångssystem och 3-värderade semantik för CTL.
Abstract Model Repair
{'venue': 'Logical Methods in Computer Science, Volume 11, Issue 3 (September 17, 2015) lmcs:1587', 'journal': None, 'mag_field_of_study': ['Computer Science']}