Digitale Bibliotheek
Sluiten Bladeren door artikelen uit een tijdschrift
<< vorige   
     Tijdschrift beschrijving
       Alle jaargangen van het bijbehorende tijdschrift
         Alle afleveringen van het bijbehorende jaargang
           Alle artikelen van de bijbehorende aflevering
                                       Details van artikel 7 van 7 gevonden artikelen
  The BDD Space Complexity of Different Forms of Concurrency
Titel: The BDD Space Complexity of Different Forms of Concurrency
Auteur: Michael Baldamus
Klaus Schneider
Verschenen in: Fundamenta informaticae
Paginering: Jaargang 50 (2003) nr. 2 pagina's 111-133
Jaar: 2003-07-11
Inhoud: The automated verification of concurrent systems by model checking is often confronted with the state space explosion problem. A widely adopted method to tackle this problem is to use binary decision diagrams (BDDs) for representing systems and state spaces implicitly. However, it may be that even the system representation itself is prohibitively large. It is therefore interesting to study which factors influence the size of a BDD that represents the transition relation of a system. In this article, we consider the BDD representations of synchronous, asynchronous, and interleaved processes with communication via shared variables and present upper bounds for their sizes. To this end, we introduce a general representation strategy where catastrophic exponential growth of the BDD can only be due to the specifics of communication and/or write conflict resolution; it is neither due to the number of processes nor to the concurrency discipline. Moreover, conditions on communication and write conflict resolution are presented that are sufficient for polynomial sized BDD representations.
Uitgever: IOS Press
Bronbestand: Elektronische Wetenschappelijke Tijdschriften

                             Details van artikel 7 van 7 gevonden artikelen
<< vorige   
 Koninklijke Bibliotheek - Nationale Bibliotheek van Nederland