A state space distribution policy based on abstract interpretation
| Autor: | Orzan, S.M., Pol, van de, J.C., Valero Espada, M.A., Brim, L., Leucker, M. |
|---|---|
| Přispěvatelé: | Specification and Analysis of Embedded Systems, Formal System Analysis |
| Jazyk: | angličtina |
| Rok vydání: | 2005 |
| Předmět: |
Model checking
Theoretical computer science General Computer Science Abstract Interpretation Abstract interpretation Theoretical Computer Science Reduction (complexity) State space reduction Distribution (mathematics) Distributed model checking Distributed algorithm Distributed Model Checking State space Mathematics Computer Science(all) |
| Zdroj: | Electronic Notes in Theoretical Computer Science, 128(3), 35-45 Proceedings 3rd International Workshop on Parallel and Distributed Methods in Verification (PDMC '04, London, UK, September 4, 2004), 35-45 STARTPAGE=35;ENDPAGE=45;TITLE=Proceedings 3rd International Workshop on Parallel and Distributed Methods in Verification (PDMC '04, London, UK, September 4, 2004) |
| ISSN: | 1571-0661 |
| Popis: | We aim at improving the performance of distributed algorithms for model checking and state space reduction. To this end, we introduce a new distribution policy of states over workers. This policy reduces the number of transitions between states located at different workers. This in turn is expected to reduce the communication costs of the distributed algorithms.The main idea is to use Abstract Interpretation techniques to compute a small approximation of the state space, starting from some high level description of the system. Based on this approximation, the connectivity of concrete states is predicted. This information is used to distribute states with expected connectivity to the same worker. Experiments show a considerable reduction of cross transitions, at the expense of a modest unbalance of nodes per worker. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect