Please use this identifier to cite or link to this item:
Title: Calculating τ-confluence compositionally
Authors: Pace, Gordon J.
Lang, Frederic
Mateescu, Radu
Keywords: Computer programs -- Verification
Compositionality (Linguistics)
Computer algorithms
Multicasting (Computer networks)
Issue Date: 2003
Publisher: Springer Berlin Heidelberg
Citation: Lang, F., Mateescu, R., & Pace, G. J. (2003). Calculating τ-confluence compositionally. 15th International Conference on Computer Aided Verification (CAV 2003), Boulder. 446-459.
Abstract: τ-confluence is a reduction technique used in enumerative model-checking of labeled transition systems to avoid the state explosion problem. In this paper, we propose a new on-the-fly algorithm to calculate partial τ-confluence, and propose new techniques to do so on large systems in a compositional manner. Using information inherent in the way a large system is composed of smaller systems, we show how we can deduce partial τ-confluence in a computationally cheap manner. Finally, these techniques are applied to a number of case studies, including the rel/REL atomic multicast protocol.
Appears in Collections:Scholarly Works - FacICTCS

Files in This Item:
File Description SizeFormat 
Calculating_τ_confluence_compositionally_2003.pdf245.83 kBAdobe PDFView/Open

Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.