τ-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. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Pace, G. J., Lang, F., & Mateescu, R. (2003). Calculating τ-confluence compositionally. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2725, 446–459. https://doi.org/10.1007/978-3-540-45069-6_41
Mendeley helps you to discover research relevant for your work.