Result: Distributed state space minimization

Title:
Distributed state space minimization
Authors:
BLOM, Stefan, ORZAN, Simona
Source:
Special section on formal methods for industrial critical systemsInternational journal on software tools for technology transfer (Print). 7(3):280-291
Publisher Information:
Berlin: Springer, 2005.
Publication Year:
2005
Physical Description:
print, 25 ref
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Logiciel, Software, Génie logiciel, Software engineering, Algorithme réparti, Distributed algorithm, Algoritmo repartido, Bisimulation, Bisimulación, Complexité algorithme, Algorithm complexity, Complejidad algoritmo, Complexité temps, Time complexity, Complejidad tiempo, Espace état, State space, Espacio estado, Parallélisation, Parallelization, Paralelisacíon, Vérification modèle, Model checking, Verificación modelo, Système transition, Transition system, Sistema transición, Bisimulation equivalence, Distributed verification
Document Type:
Conference Conference Paper
File Description:
text
Language:
English
Author Affiliations:
CWI, Netherlands
Eindhoven University of Technology, Netherlands
ISSN:
1433-2779
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=16971341
Rights:
Copyright 2005 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.16971341
Database:
PASCAL Archive

Further Information

We present a new algorithm, and its distributed implementation, for reducing labeled transition systems modulo strong bisimulation. The base of this algorithm is the Kanellakis-Smolka naive method, which has a high theoretical complexity but is successful in practice and well suited to parallelization. This basic approach is combined with optimizations inspired by the Kanellakis-Smolka algorithm for the case of bounded fanout, which has the best known time complexity. The distributed implementation is improved with respect to previous attempts by a better overlap between communication and computation, which results in an efficient usage of both memory and processing power. We also discuss the time complexity of this algorithm and show experimental results with sequential and distributed prototype tools.