ACM/IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Eighth Annual IEEE Symposium on

Logic in Computer Science (LICS 1993)

Paper: Verifying programs with unreliable channels (at LICS 1993)

Authors: Parosh A. Abdulla Bengt Jonsson


The verification of a particular class of infinite-state systems, namely, systems consisting of finite-state processes that communicate via unbounded lossy FIFO channels, is considered. This class is able to model, e.g., link protocols such as the Alternating Bit Protocol and HDLC. For this class of systems, it is shown that several interesting verification problems are decidable by giving algorithms for verifying: the reachability problem (whether a finite set of global states is reachable from some other global state of the system); the safety property over traces, formulated as regular sets of allowed finite traces; and eventuality properties (whether all computations of a system eventually reach a given set of states). The algorithms are used to verify some idealized sliding-window protocols with reasonable time and space resources


    author = 	 {Parosh A. Abdulla and Bengt Jonsson},
    title = 	 {Verifying programs with unreliable channels},
    booktitle =  {Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science (LICS 1993)},
    year =	 {1993},
    month =	 {June}, 
    pages =      {160--170},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}

Last modified: 2021-04-0120:36
Sam Staton