Checking Language Inclusion On-the-Fly with the Sweep-line Method

The sweep-line state space method allows states to be deleted from memory during state exploration, thus alleviating state explosion. Properties of the system (such as the absence of deadlocks) can then be verified on-the-fly. This paper presents an extension to the sweepline method that allows on-the-fly checking of language inclusion, which is useful for protocol verification. This has been implemented in a prototype Sweep-line library for Design/CPN. We evaluate the prototype by applying it to the connection management procedures of the Datagram Congestion Control Protocol, a new Internet transport protocol