Abstrakt. Gränsad modellkontroll är en symbolisk felsökningsmetod som undersöker vägar av avgränsad längd för brott mot en given LTL-formel. Det snabba införandet inom industrin beror mycket på framsteg inom SAT-teknik under de senaste 10-15 åren. På senare tid har det gjorts allt större ansträngningar för att tillämpa SAT-baserade metoder på obegränsad modellkontroll. En sådan metod är baserad på att beräkna en fullständighetströskel: en bunden k sådan att, om inget motexempel på längd k eller mindre till en given LTL formel hittas, då formeln i själva verket håller över alla oändliga vägar i modellen. Den viktigaste utmaningen är att fastställa tillräckligt små tröskelvärden för fullständighet. I detta dokument visar vi att om Büchi-automaten i samband med en LTL-formel är klibbig, dvs. kan dekomponeras till kliqueformade starkt anslutna komponenter, så är den tillhörande fullständighetströskeln linjär i den aktuella Kripke-modellens recidivdiameter. Vi konstaterar dessutom att alla oary temporal logik formler ger upphov till kliquey automata, och observera att denna grupp innehåller ett brett spektrum av specifikationer som används i praktiken, avsevärt stärka tidigare resultat, som rapporterar hanterbara tröskelvärden endast för elementära formler av formen F p och G q.
För sådan automata ger REF en fullständighetströskel.
Linear completeness thresholds for bounded model checking
{'venue': 'CAV', 'journal': None, 'mag_field_of_study': ['Computer Science']}