Vi anser att verifieringen av en viss klass av infinita tillståndssystem, nämligen system som består av finita tillståndsprocesser som kommunicerar via obundna förlorade FIFO-kanaler. Denna klass kan modellera t.ex. länk protokoll såsom Alternating Bit Protocol och HDLC. För denna klass av system, visar vi att flera intressanta verifieringsproblem är deciderbara genom att ge algoritmer för att verifiera (1) tillgänglighetsproblem: är en ändlig uppsättning globala tillstånd som kan nås från någon annan global tillstånd i systemet, ( 2 ) säkerhet korrekt över spår formulerade som regelbundna uppsättningar tillåtna finita spår, och (3) eventualitet egenskaper: gör alla beräkningar av ett system så småningom nå en given uppsättning stater. Vi har använt algoritmerna för att verifiera några idealiserade skjutfönster protokoll med rimlig tid och utrymme resurser. Våra resultat bör ställas i kontrast till det välkända faktum att dessa problem är obeslutbara för system med obegränsade perfekta FIFO-kanaler.
För obundna förlorade FIFO kanaler, tillgänglighet, säkerhet av systemspår, och eventualitet egenskaper är decideable REF.
Verifying programs with unreliable channels
{'venue': '[1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science', 'journal': '[1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science', 'mag_field_of_study': ['Computer Science']}