Probabilistic Methods in State Space Analysis
Identifieur interne : 002217 ( Istex/Corpus ); précédent : 002216; suivant : 002218Probabilistic Methods in State Space Analysis
Auteurs : Matthias Kuntz ; Kai LampkaSource :
- Lecture Notes in Computer Science [ 0302-9743 ] ; 2004.
Abstract
Abstract: Several methods have been developed to validate the correctness and performance of hard- and software systems. One way to do this is to model the system and carry out a state space exploration in order to detect all possible states. In this paper, a survey of existing probabilistic state space exploration methods is given. The paper starts with a thorough review and analysis of bitstate hashing, as introduced by Holzmann. The main idea of this initial approach is the mapping of each state onto a specific bit within an array by employing a hash function. Thus a state is represented by a single bit, rather than by a full descriptor. Bitstate hashing is efficient concerning memory and runtime, but it is hampered by the non deterministic omission of states. The resulting positive probability of producing wrong results is due to the fact that the mapping of full state descriptors onto much smaller representatives is not injective. – The rest of the paper is devoted to the presentation, analysis, and comparison of improvements of bitstate hashing, which were introduced in order to lower the probability of producing a wrong result, but maintaining the memory and runtime efficiency. These improvements can be mainly grouped into two categories: The approaches of the first group, the so called multiple hashing schemes, employ multiple hash functions on either a single or on multiple arrays. The approaches of the remaining category follow the idea of hash compaction. I.e. the diverse schemes of this category store a hash value for each detected state, rather than associating a single or multiple bit positions with it, leading to persuasive reductions of the probability of error if compared to the original bitstate hashing scheme.
Url:
DOI: 10.1007/978-3-540-24611-4_10
Links to Exploration step
ISTEX:F16EC372915570209346ECBAC440F10BF2284998Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Probabilistic Methods in State Space Analysis</title><author><name sortKey="Kuntz, Matthias" sort="Kuntz, Matthias" uniqKey="Kuntz M" first="Matthias" last="Kuntz">Matthias Kuntz</name><affiliation><mods:affiliation>Institut für Informatik, Friedrich-Alexander-Universität Erlangen-Nürnberg</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: mskuntz@informatik.uni-erlangen.de</mods:affiliation></affiliation></author><author><name sortKey="Lampka, Kai" sort="Lampka, Kai" uniqKey="Lampka K" first="Kai" last="Lampka">Kai Lampka</name><affiliation><mods:affiliation>Institut für Informatik, Friedrich-Alexander-Universität Erlangen-Nürnberg</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: kilampka@informatik.uni-erlangen.de</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:F16EC372915570209346ECBAC440F10BF2284998</idno><date when="2004" year="2004">2004</date><idno type="doi">10.1007/978-3-540-24611-4_10</idno><idno type="url">https://api.istex.fr/document/F16EC372915570209346ECBAC440F10BF2284998/fulltext/pdf</idno><idno type="wicri:Area/Istex/Corpus">002217</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002217</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Probabilistic Methods in State Space Analysis</title><author><name sortKey="Kuntz, Matthias" sort="Kuntz, Matthias" uniqKey="Kuntz M" first="Matthias" last="Kuntz">Matthias Kuntz</name><affiliation><mods:affiliation>Institut für Informatik, Friedrich-Alexander-Universität Erlangen-Nürnberg</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: mskuntz@informatik.uni-erlangen.de</mods:affiliation></affiliation></author><author><name sortKey="Lampka, Kai" sort="Lampka, Kai" uniqKey="Lampka K" first="Kai" last="Lampka">Kai Lampka</name><affiliation><mods:affiliation>Institut für Informatik, Friedrich-Alexander-Universität Erlangen-Nürnberg</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: kilampka@informatik.uni-erlangen.de</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="s">Lecture Notes in Computer Science</title><imprint><date>2004</date></imprint><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series><idno type="istex">F16EC372915570209346ECBAC440F10BF2284998</idno><idno type="DOI">10.1007/978-3-540-24611-4_10</idno><idno type="ChapterID">10</idno><idno type="ChapterID">Chap10</idno></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Several methods have been developed to validate the correctness and performance of hard- and software systems. One way to do this is to model the system and carry out a state space exploration in order to detect all possible states. In this paper, a survey of existing probabilistic state space exploration methods is given. The paper starts with a thorough review and analysis of bitstate hashing, as introduced by Holzmann. The main idea of this initial approach is the mapping of each state onto a specific bit within an array by employing a hash function. Thus a state is represented by a single bit, rather than by a full descriptor. Bitstate hashing is efficient concerning memory and runtime, but it is hampered by the non deterministic omission of states. The resulting positive probability of producing wrong results is due to the fact that the mapping of full state descriptors onto much smaller representatives is not injective. – The rest of the paper is devoted to the presentation, analysis, and comparison of improvements of bitstate hashing, which were introduced in order to lower the probability of producing a wrong result, but maintaining the memory and runtime efficiency. These improvements can be mainly grouped into two categories: The approaches of the first group, the so called multiple hashing schemes, employ multiple hash functions on either a single or on multiple arrays. The approaches of the remaining category follow the idea of hash compaction. I.e. the diverse schemes of this category store a hash value for each detected state, rather than associating a single or multiple bit positions with it, leading to persuasive reductions of the probability of error if compared to the original bitstate hashing scheme.</div></front></TEI><istex><corpusName>springer</corpusName><author><json:item><name>Matthias Kuntz</name><affiliations><json:string>Institut für Informatik, Friedrich-Alexander-Universität Erlangen-Nürnberg,</json:string><json:string>E-mail: mskuntz@informatik.uni-erlangen.de</json:string></affiliations></json:item><json:item><name>Kai Lampka</name><affiliations><json:string>Institut für Informatik, Friedrich-Alexander-Universität Erlangen-Nürnberg,</json:string><json:string>E-mail: kilampka@informatik.uni-erlangen.de</json:string></affiliations></json:item></author><language><json:string>eng</json:string></language><abstract>Abstract: Several methods have been developed to validate the correctness and performance of hard- and software systems. One way to do this is to model the system and carry out a state space exploration in order to detect all possible states. In this paper, a survey of existing probabilistic state space exploration methods is given. The paper starts with a thorough review and analysis of bitstate hashing, as introduced by Holzmann. The main idea of this initial approach is the mapping of each state onto a specific bit within an array by employing a hash function. Thus a state is represented by a single bit, rather than by a full descriptor. Bitstate hashing is efficient concerning memory and runtime, but it is hampered by the non deterministic omission of states. The resulting positive probability of producing wrong results is due to the fact that the mapping of full state descriptors onto much smaller representatives is not injective. – The rest of the paper is devoted to the presentation, analysis, and comparison of improvements of bitstate hashing, which were introduced in order to lower the probability of producing a wrong result, but maintaining the memory and runtime efficiency. These improvements can be mainly grouped into two categories: The approaches of the first group, the so called multiple hashing schemes, employ multiple hash functions on either a single or on multiple arrays. The approaches of the remaining category follow the idea of hash compaction. I.e. the diverse schemes of this category store a hash value for each detected state, rather than associating a single or multiple bit positions with it, leading to persuasive reductions of the probability of error if compared to the original bitstate hashing scheme.</abstract><qualityIndicators><score>8</score><pdfVersion>1.3</pdfVersion><pdfPageSize>430 x 660 pts</pdfPageSize><refBibsNative>false</refBibsNative><keywordCount>0</keywordCount><abstractCharCount>1758</abstractCharCount><pdfWordCount>15945</pdfWordCount><pdfCharCount>84415</pdfCharCount><pdfPageCount>45</pdfPageCount><abstractWordCount>285</abstractWordCount></qualityIndicators><title>Probabilistic Methods in State Space Analysis</title><genre.original><json:string>OriginalPaper</json:string></genre.original><chapterId><json:string>10</json:string><json:string>Chap10</json:string></chapterId><genre><json:string>conference [eBooks]</json:string></genre><serie><editor><json:item><name>Gerhard Goos</name><affiliations><json:string>Karlsruhe University, Germany</json:string></affiliations></json:item><json:item><name>Juris Hartmanis</name><affiliations><json:string>Cornell University, NY, USA</json:string></affiliations></json:item><json:item><name>Jan van Leeuwen</name><affiliations><json:string>Utrecht University, The Netherlands</json:string></affiliations></json:item></editor><issn><json:string>0302-9743</json:string></issn><language><json:string>unknown</json:string></language><eissn><json:string>1611-3349</json:string></eissn><title>Lecture Notes in Computer Science</title><copyrightDate>2004</copyrightDate></serie><host><editor><json:item><name>Christel Baier</name><affiliations><json:string>Institute for Theoretical Computer Science, Technical University Dresden, Germany</json:string><json:string>E-mail: baier@tcs.inf.tu-dresden.de</json:string></affiliations></json:item><json:item><name>Boudewijn R. Haverkort</name><affiliations><json:string>Centre for Telematics and Information Technology, Faculty for Electrical Engineering, Mathematics and Computer Science, University of Twente, P.O. Box 217, 7500, AE, Netherlands</json:string><json:string>E-mail: b.r.h.m.haverkort@utwente.nl</json:string></affiliations></json:item><json:item><name>Holger Hermanns</name><affiliations><json:string>VASY, INRIA, Grenoble Rhône-Alpes, France</json:string><json:string>E-mail: hermanns@cs.uni-sb.de</json:string></affiliations></json:item><json:item><name>Joost-Pieter Katoen</name><affiliations><json:string>Software Modeling and Verification, RWTH Aachen University, Germany</json:string><json:string>E-mail: katoen@cs.rwth-aachen.de</json:string></affiliations></json:item><json:item><name>Markus Siegle</name><affiliations><json:string>Institut für Technische Informatik, Universität der Bundeswehr München,</json:string><json:string>E-mail: markus.siegle@unibw.de</json:string></affiliations></json:item></editor><subject><json:item><value>Computer Science</value></json:item><json:item><value>Computer Science</value></json:item><json:item><value>Computation by Abstract Devices</value></json:item><json:item><value>Logics and Meanings of Programs</value></json:item><json:item><value>Software Engineering</value></json:item><json:item><value>Operating Systems</value></json:item><json:item><value>Processor Architectures</value></json:item><json:item><value>Simulation and Modeling</value></json:item></subject><isbn><json:string>978-3-540-22265-1</json:string></isbn><language><json:string>unknown</json:string></language><eissn><json:string>1611-3349</json:string></eissn><title>Validation of Stochastic Systems</title><genre.original><json:string>Proceedings</json:string></genre.original><bookId><json:string>978-3-540-24611-4</json:string></bookId><volume>2925</volume><pages><last>383</last><first>339</first></pages><issn><json:string>0302-9743</json:string></issn><genre><json:string>Book Series</json:string></genre><eisbn><json:string>978-3-540-24611-4</json:string></eisbn><copyrightDate>2004</copyrightDate><doi><json:string>10.1007/b98484</json:string></doi></host><publicationDate>2004</publicationDate><copyrightDate>2004</copyrightDate><doi><json:string>10.1007/978-3-540-24611-4_10</json:string></doi><id>F16EC372915570209346ECBAC440F10BF2284998</id><score>1</score><fulltext><json:item><original>true</original><mimetype>application/pdf</mimetype><extension>pdf</extension><uri>https://api.istex.fr/document/F16EC372915570209346ECBAC440F10BF2284998/fulltext/pdf</uri></json:item><json:item><original>false</original><mimetype>application/zip</mimetype><extension>zip</extension><uri>https://api.istex.fr/document/F16EC372915570209346ECBAC440F10BF2284998/fulltext/zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/document/F16EC372915570209346ECBAC440F10BF2284998/fulltext/tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Probabilistic Methods in State Space Analysis</title><respStmt xml:id="ISTEX-API" resp="Références bibliographiques récupérées via GROBID" name="ISTEX-API (INIST-CNRS)"></respStmt></titleStmt><publicationStmt><authority>ISTEX</authority><publisher>Springer Berlin Heidelberg</publisher><pubPlace>Berlin, Heidelberg</pubPlace><availability><p>SPRINGER</p></availability><date>2004</date></publicationStmt><sourceDesc><biblStruct type="inbook"><analytic><title level="a" type="main" xml:lang="en">Probabilistic Methods in State Space Analysis</title><author><persName><forename type="first">Matthias</forename><surname>Kuntz</surname></persName><email>mskuntz@informatik.uni-erlangen.de</email><affiliation>Institut für Informatik, Friedrich-Alexander-Universität Erlangen-Nürnberg,</affiliation></author><author><persName><forename type="first">Kai</forename><surname>Lampka</surname></persName><email>kilampka@informatik.uni-erlangen.de</email><affiliation>Institut für Informatik, Friedrich-Alexander-Universität Erlangen-Nürnberg,</affiliation></author></analytic><monogr><title level="m">Validation of Stochastic Systems</title><title level="m" type="sub">A Guide to Current Research</title><idno type="pISBN">978-3-540-22265-1</idno><idno type="eISBN">978-3-540-24611-4</idno><idno type="pISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="DOI">10.1007/b98484</idno><idno type="BookID">978-3-540-24611-4</idno><idno type="BookTitleID">83139</idno><idno type="BookSequenceNumber">2925</idno><idno type="BookVolumeNumber">2925</idno><idno type="BookChapterCount">13</idno><editor><persName><forename type="first">Christel</forename><surname>Baier</surname></persName><email>baier@tcs.inf.tu-dresden.de</email><affiliation>Institute for Theoretical Computer Science, Technical University Dresden, Germany</affiliation></editor><editor><persName><forename type="first">Boudewijn</forename><forename type="first">R.</forename><surname>Haverkort</surname></persName><email>b.r.h.m.haverkort@utwente.nl</email><affiliation>Centre for Telematics and Information Technology, Faculty for Electrical Engineering, Mathematics and Computer Science, University of Twente, P.O. Box 217, 7500, AE, Netherlands</affiliation></editor><editor><persName><forename type="first">Holger</forename><surname>Hermanns</surname></persName><email>hermanns@cs.uni-sb.de</email><affiliation>VASY, INRIA, Grenoble Rhône-Alpes, France</affiliation></editor><editor><persName><forename type="first">Joost-Pieter</forename><surname>Katoen</surname></persName><email>katoen@cs.rwth-aachen.de</email><affiliation>Software Modeling and Verification, RWTH Aachen University, Germany</affiliation></editor><editor><persName><forename type="first">Markus</forename><surname>Siegle</surname></persName><email>markus.siegle@unibw.de</email><affiliation>Institut für Technische Informatik, Universität der Bundeswehr München,</affiliation></editor><imprint><publisher>Springer Berlin Heidelberg</publisher><pubPlace>Berlin, Heidelberg</pubPlace><date type="published" when="2004"></date><biblScope unit="volume">2925</biblScope><biblScope unit="page" from="339">339</biblScope><biblScope unit="page" to="383">383</biblScope></imprint></monogr><series><title level="s">Lecture Notes in Computer Science</title><editor><persName><forename type="first">Gerhard</forename><surname>Goos</surname></persName><affiliation>Karlsruhe University, Germany</affiliation></editor><editor><persName><forename type="first">Juris</forename><surname>Hartmanis</surname></persName><affiliation>Cornell University, NY, USA</affiliation></editor><editor><persName><forename type="first">Jan</forename><surname>van Leeuwen</surname></persName><affiliation>Utrecht University, The Netherlands</affiliation></editor><biblScope><date>2004</date></biblScope><idno type="pISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="seriesId">558</idno></series><idno type="istex">F16EC372915570209346ECBAC440F10BF2284998</idno><idno type="DOI">10.1007/978-3-540-24611-4_10</idno><idno type="ChapterID">10</idno><idno type="ChapterID">Chap10</idno></biblStruct></sourceDesc></fileDesc><profileDesc><creation><date>2004</date></creation><langUsage><language ident="en">en</language></langUsage><abstract xml:lang="en"><p>Abstract: Several methods have been developed to validate the correctness and performance of hard- and software systems. One way to do this is to model the system and carry out a state space exploration in order to detect all possible states. In this paper, a survey of existing probabilistic state space exploration methods is given. The paper starts with a thorough review and analysis of bitstate hashing, as introduced by Holzmann. The main idea of this initial approach is the mapping of each state onto a specific bit within an array by employing a hash function. Thus a state is represented by a single bit, rather than by a full descriptor. Bitstate hashing is efficient concerning memory and runtime, but it is hampered by the non deterministic omission of states. The resulting positive probability of producing wrong results is due to the fact that the mapping of full state descriptors onto much smaller representatives is not injective. – The rest of the paper is devoted to the presentation, analysis, and comparison of improvements of bitstate hashing, which were introduced in order to lower the probability of producing a wrong result, but maintaining the memory and runtime efficiency. These improvements can be mainly grouped into two categories: The approaches of the first group, the so called multiple hashing schemes, employ multiple hash functions on either a single or on multiple arrays. The approaches of the remaining category follow the idea of hash compaction. I.e. the diverse schemes of this category store a hash value for each detected state, rather than associating a single or multiple bit positions with it, leading to persuasive reductions of the probability of error if compared to the original bitstate hashing scheme.</p></abstract><textClass><keywords scheme="Book Subject Collection"><list><label>SUCO11645</label><item><term>Computer Science</term></item></list></keywords></textClass><textClass><keywords scheme="Book Subject Group"><list><label>I</label><label>I16013</label><label>I1603X</label><label>I14029</label><label>I14045</label><label>I13014</label><label>I21025</label><item><term>Computer Science</term></item><item><term>Computation by Abstract Devices</term></item><item><term>Logics and Meanings of Programs</term></item><item><term>Software Engineering</term></item><item><term>Operating Systems</term></item><item><term>Processor Architectures</term></item><item><term>Simulation and Modeling</term></item></list></keywords></textClass></profileDesc><revisionDesc><change when="2004">Published</change><change xml:id="refBibs-istex" who="#ISTEX-API" when="2016-3-20">References added</change></revisionDesc></teiHeader></istex:fulltextTEI><json:item><original>false</original><mimetype>text/plain</mimetype><extension>txt</extension><uri>https://api.istex.fr/document/F16EC372915570209346ECBAC440F10BF2284998/fulltext/txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="Springer, Publisher found" wicri:toSee="no header"><istex:xmlDeclaration>version="1.0" encoding="UTF-8"</istex:xmlDeclaration><istex:docType PUBLIC="-//Springer-Verlag//DTD A++ V2.4//EN" URI="http://devel.springer.de/A++/V2.4/DTD/A++V2.4.dtd" name="istex:docType"></istex:docType><istex:document><Publisher><PublisherInfo><PublisherName>Springer Berlin Heidelberg</PublisherName><PublisherLocation>Berlin, Heidelberg</PublisherLocation></PublisherInfo><Series><SeriesInfo SeriesType="Series" TocLevels="0"><SeriesID>558</SeriesID><SeriesPrintISSN>0302-9743</SeriesPrintISSN><SeriesElectronicISSN>1611-3349</SeriesElectronicISSN><SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle></SeriesInfo><SeriesHeader><EditorGroup><Editor AffiliationIDS="Aff1"><EditorName DisplayOrder="Western"><GivenName>Gerhard</GivenName><FamilyName>Goos</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff2"><EditorName DisplayOrder="Western"><GivenName>Juris</GivenName><FamilyName>Hartmanis</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff3"><EditorName DisplayOrder="Western"><GivenName>Jan</GivenName><Particle>van</Particle><FamilyName>Leeuwen</FamilyName></EditorName></Editor><Affiliation ID="Aff1"><OrgName>Karlsruhe University</OrgName><OrgAddress><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgName>Cornell University</OrgName><OrgAddress><State>NY</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff3"><OrgName>Utrecht University</OrgName><OrgAddress><Country>The Netherlands</Country></OrgAddress></Affiliation></EditorGroup></SeriesHeader><Book Language="En"><BookInfo BookProductType="Proceedings" ContainsESM="No" Language="En" MediaType="eBook" NumberingDepth="2" NumberingStyle="ContentOnly" OutputMedium="All" TocLevels="0"><BookID>978-3-540-24611-4</BookID><BookTitle>Validation of Stochastic Systems</BookTitle><BookSubTitle>A Guide to Current Research</BookSubTitle><BookVolumeNumber>2925</BookVolumeNumber><BookSequenceNumber>2925</BookSequenceNumber><BookDOI>10.1007/b98484</BookDOI><BookTitleID>83139</BookTitleID><BookPrintISBN>978-3-540-22265-1</BookPrintISBN><BookElectronicISBN>978-3-540-24611-4</BookElectronicISBN><BookChapterCount>13</BookChapterCount><BookCopyright><CopyrightHolderName>Springer Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2004</CopyrightYear></BookCopyright><BookSubjectGroup><BookSubject Code="I" Type="Primary">Computer Science</BookSubject><BookSubject Code="I16013" Priority="1" Type="Secondary">Computation by Abstract Devices</BookSubject><BookSubject Code="I1603X" Priority="2" Type="Secondary">Logics and Meanings of Programs</BookSubject><BookSubject Code="I14029" Priority="3" Type="Secondary">Software Engineering</BookSubject><BookSubject Code="I14045" Priority="4" Type="Secondary">Operating Systems</BookSubject><BookSubject Code="I13014" Priority="5" Type="Secondary">Processor Architectures</BookSubject><BookSubject Code="I21025" Priority="6" Type="Secondary">Simulation and Modeling</BookSubject><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup><BookContext><SeriesID>558</SeriesID></BookContext></BookInfo><BookHeader><EditorGroup><Editor AffiliationIDS="Aff4"><EditorName DisplayOrder="Western"><GivenName>Christel</GivenName><FamilyName>Baier</FamilyName></EditorName><Contact><Email>baier@tcs.inf.tu-dresden.de</Email></Contact></Editor><Editor AffiliationIDS="Aff5"><EditorName DisplayOrder="Western"><GivenName>Boudewijn</GivenName><GivenName>R.</GivenName><FamilyName>Haverkort</FamilyName></EditorName><Contact><Email>b.r.h.m.haverkort@utwente.nl</Email></Contact></Editor><Editor AffiliationIDS="Aff6"><EditorName DisplayOrder="Western"><GivenName>Holger</GivenName><FamilyName>Hermanns</FamilyName></EditorName><Contact><Email>hermanns@cs.uni-sb.de</Email></Contact></Editor><Editor AffiliationIDS="Aff7"><EditorName DisplayOrder="Western"><GivenName>Joost-Pieter</GivenName><FamilyName>Katoen</FamilyName></EditorName><Contact><Email>katoen@cs.rwth-aachen.de</Email></Contact></Editor><Editor AffiliationIDS="Aff8"><EditorName DisplayOrder="Western"><GivenName>Markus</GivenName><FamilyName>Siegle</FamilyName></EditorName><Contact><Email>markus.siegle@unibw.de</Email></Contact></Editor><Affiliation ID="Aff4"><OrgDivision>Institute for Theoretical Computer Science</OrgDivision><OrgName>Technical University Dresden</OrgName><OrgAddress><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff5"><OrgDivision>Centre for Telematics and Information Technology, Faculty for Electrical Engineering, Mathematics and Computer Science</OrgDivision><OrgName>University of Twente</OrgName><OrgAddress><Postbox>P.O. Box 217</Postbox><Postcode>7500</Postcode><State>AE</State><Country>Netherlands</Country></OrgAddress></Affiliation><Affiliation ID="Aff6"><OrgDivision>VASY</OrgDivision><OrgName>INRIA</OrgName><OrgAddress><City>Grenoble Rhône-Alpes</City><Country>France</Country></OrgAddress></Affiliation><Affiliation ID="Aff7"><OrgDivision>Software Modeling and Verification</OrgDivision><OrgName>RWTH Aachen University</OrgName><OrgAddress><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff8"><OrgDivision>Institut für Technische Informatik</OrgDivision><OrgName>Universität der Bundeswehr München</OrgName><OrgAddress><Country> </Country></OrgAddress></Affiliation></EditorGroup></BookHeader><Part ID="Part3"><PartInfo TocLevels="0"><PartID>3</PartID><PartSequenceNumber>3</PartSequenceNumber><PartTitle>Representing Large State Spaces</PartTitle><PartChapterCount>4</PartChapterCount><PartContext><SeriesID>558</SeriesID><BookTitle>Validation of Stochastic Systems</BookTitle></PartContext></PartInfo><Chapter ID="Chap10" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" NumberingDepth="2" NumberingStyle="ContentOnly" TocLevels="0"><ChapterID>10</ChapterID><ChapterDOI>10.1007/978-3-540-24611-4_10</ChapterDOI><ChapterSequenceNumber>10</ChapterSequenceNumber><ChapterTitle Language="En">Probabilistic Methods in State Space Analysis</ChapterTitle><ChapterFirstPage>339</ChapterFirstPage><ChapterLastPage>383</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2004</CopyrightYear></ChapterCopyright><ChapterGrants Type="Regular"><MetadataGrant Grant="OpenAccess"></MetadataGrant><AbstractGrant Grant="OpenAccess"></AbstractGrant><BodyPDFGrant Grant="Restricted"></BodyPDFGrant><BodyHTMLGrant Grant="Restricted"></BodyHTMLGrant><BibliographyGrant Grant="Restricted"></BibliographyGrant><ESMGrant Grant="Restricted"></ESMGrant></ChapterGrants><ChapterContext><SeriesID>558</SeriesID><PartID>3</PartID><BookID>978-3-540-24611-4</BookID><BookTitle>Validation of Stochastic Systems</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff9"><AuthorName DisplayOrder="Western"><GivenName>Matthias</GivenName><FamilyName>Kuntz</FamilyName></AuthorName><Contact><Email>mskuntz@informatik.uni-erlangen.de</Email></Contact></Author><Author AffiliationIDS="Aff9"><AuthorName DisplayOrder="Western"><GivenName>Kai</GivenName><FamilyName>Lampka</FamilyName></AuthorName><Contact><Email>kilampka@informatik.uni-erlangen.de</Email></Contact></Author><Affiliation ID="Aff9"><OrgDivision>Institut für Informatik</OrgDivision><OrgName>Friedrich-Alexander-Universität Erlangen-Nürnberg</OrgName><OrgAddress><Country> </Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>Several methods have been developed to validate the correctness and performance of hard- and software systems. One way to do this is to model the system and carry out a state space exploration in order to detect all possible states. In this paper, a survey of existing probabilistic state space exploration methods is given. The paper starts with a thorough review and analysis of bitstate hashing, as introduced by Holzmann. The main idea of this initial approach is the mapping of each state onto a specific bit within an array by employing a hash function. Thus a state is represented by a single bit, rather than by a full descriptor. Bitstate hashing is efficient concerning memory and runtime, but it is hampered by the non deterministic omission of states. The resulting positive probability of producing wrong results is due to the fact that the mapping of full state descriptors onto much smaller representatives is not injective. – The rest of the paper is devoted to the presentation, analysis, and comparison of improvements of bitstate hashing, which were introduced in order to lower the probability of producing a wrong result, but maintaining the memory and runtime efficiency. These improvements can be mainly grouped into two categories: The approaches of the first group, the so called multiple hashing schemes, employ multiple hash functions on either a single or on multiple arrays. The approaches of the remaining category follow the idea of hash compaction. I.e. the diverse schemes of this category store a hash value for each detected state, rather than associating a single or multiple bit positions with it, leading to persuasive reductions of the probability of error if compared to the original bitstate hashing scheme.</Para></Abstract></ChapterHeader><NoBody></NoBody></Chapter></Part></Book></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Probabilistic Methods in State Space Analysis</title></titleInfo><titleInfo type="alternative" contentType="CDATA" lang="en"><title>Probabilistic Methods in State Space Analysis</title></titleInfo><name type="personal"><namePart type="given">Matthias</namePart><namePart type="family">Kuntz</namePart><affiliation>Institut für Informatik, Friedrich-Alexander-Universität Erlangen-Nürnberg</affiliation><affiliation>E-mail: mskuntz@informatik.uni-erlangen.de</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Kai</namePart><namePart type="family">Lampka</namePart><affiliation>Institut für Informatik, Friedrich-Alexander-Universität Erlangen-Nürnberg</affiliation><affiliation>E-mail: kilampka@informatik.uni-erlangen.de</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre type="conference [eBooks]" displayLabel="OriginalPaper"></genre><originInfo><publisher>Springer Berlin Heidelberg</publisher><place><placeTerm type="text">Berlin, Heidelberg</placeTerm></place><dateIssued encoding="w3cdtf">2004</dateIssued><copyrightDate encoding="w3cdtf">2004</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><physicalDescription><internetMediaType>text/html</internetMediaType></physicalDescription><abstract lang="en">Abstract: Several methods have been developed to validate the correctness and performance of hard- and software systems. One way to do this is to model the system and carry out a state space exploration in order to detect all possible states. In this paper, a survey of existing probabilistic state space exploration methods is given. The paper starts with a thorough review and analysis of bitstate hashing, as introduced by Holzmann. The main idea of this initial approach is the mapping of each state onto a specific bit within an array by employing a hash function. Thus a state is represented by a single bit, rather than by a full descriptor. Bitstate hashing is efficient concerning memory and runtime, but it is hampered by the non deterministic omission of states. The resulting positive probability of producing wrong results is due to the fact that the mapping of full state descriptors onto much smaller representatives is not injective. – The rest of the paper is devoted to the presentation, analysis, and comparison of improvements of bitstate hashing, which were introduced in order to lower the probability of producing a wrong result, but maintaining the memory and runtime efficiency. These improvements can be mainly grouped into two categories: The approaches of the first group, the so called multiple hashing schemes, employ multiple hash functions on either a single or on multiple arrays. The approaches of the remaining category follow the idea of hash compaction. I.e. the diverse schemes of this category store a hash value for each detected state, rather than associating a single or multiple bit positions with it, leading to persuasive reductions of the probability of error if compared to the original bitstate hashing scheme.</abstract><relatedItem type="host"><titleInfo><title>Validation of Stochastic Systems</title><subTitle>A Guide to Current Research</subTitle></titleInfo><name type="personal"><namePart type="given">Christel</namePart><namePart type="family">Baier</namePart><affiliation>Institute for Theoretical Computer Science, Technical University Dresden, Germany</affiliation><affiliation>E-mail: baier@tcs.inf.tu-dresden.de</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Boudewijn</namePart><namePart type="given">R.</namePart><namePart type="family">Haverkort</namePart><affiliation>Centre for Telematics and Information Technology, Faculty for Electrical Engineering, Mathematics and Computer Science, University of Twente, P.O. Box 217, 7500, AE, Netherlands</affiliation><affiliation>E-mail: b.r.h.m.haverkort@utwente.nl</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Holger</namePart><namePart type="family">Hermanns</namePart><affiliation>VASY, INRIA, Grenoble Rhône-Alpes, France</affiliation><affiliation>E-mail: hermanns@cs.uni-sb.de</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Joost-Pieter</namePart><namePart type="family">Katoen</namePart><affiliation>Software Modeling and Verification, RWTH Aachen University, Germany</affiliation><affiliation>E-mail: katoen@cs.rwth-aachen.de</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Markus</namePart><namePart type="family">Siegle</namePart><affiliation>Institut für Technische Informatik, Universität der Bundeswehr München</affiliation><affiliation>E-mail: markus.siegle@unibw.de</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><genre type="Book Series" displayLabel="Proceedings"></genre><originInfo><copyrightDate encoding="w3cdtf">2004</copyrightDate><issuance>monographic</issuance></originInfo><subject><genre>Book Subject Collection</genre><topic authority="SpringerSubjectCodes" authorityURI="SUCO11645">Computer Science</topic></subject><subject><genre>Book Subject Group</genre><topic authority="SpringerSubjectCodes" authorityURI="I">Computer Science</topic><topic authority="SpringerSubjectCodes" authorityURI="I16013">Computation by Abstract Devices</topic><topic authority="SpringerSubjectCodes" authorityURI="I1603X">Logics and Meanings of Programs</topic><topic authority="SpringerSubjectCodes" authorityURI="I14029">Software Engineering</topic><topic authority="SpringerSubjectCodes" authorityURI="I14045">Operating Systems</topic><topic authority="SpringerSubjectCodes" authorityURI="I13014">Processor Architectures</topic><topic authority="SpringerSubjectCodes" authorityURI="I21025">Simulation and Modeling</topic></subject><identifier type="DOI">10.1007/b98484</identifier><identifier type="ISBN">978-3-540-22265-1</identifier><identifier type="eISBN">978-3-540-24611-4</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="BookTitleID">83139</identifier><identifier type="BookID">978-3-540-24611-4</identifier><identifier type="BookChapterCount">13</identifier><identifier type="BookVolumeNumber">2925</identifier><identifier type="BookSequenceNumber">2925</identifier><identifier type="PartChapterCount">4</identifier><part><date>2004</date><detail type="part"><title>Representing Large State Spaces</title></detail><detail type="volume"><number>2925</number><caption>vol.</caption></detail><extent unit="pages"><start>339</start><end>383</end></extent></part><recordInfo><recordOrigin>Springer Berlin Heidelberg, 2004</recordOrigin></recordInfo></relatedItem><relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title></titleInfo><name type="personal"><namePart type="given">Gerhard</namePart><namePart type="family">Goos</namePart><affiliation>Karlsruhe University, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Juris</namePart><namePart type="family">Hartmanis</namePart><affiliation>Cornell University, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jan</namePart><namePart type="family">van Leeuwen</namePart><affiliation>Utrecht University, The Netherlands</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><originInfo><copyrightDate encoding="w3cdtf">2004</copyrightDate><issuance>serial</issuance></originInfo><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="SeriesID">558</identifier><recordInfo><recordOrigin>Springer Berlin Heidelberg, 2004</recordOrigin></recordInfo></relatedItem><identifier type="istex">F16EC372915570209346ECBAC440F10BF2284998</identifier><identifier type="DOI">10.1007/978-3-540-24611-4_10</identifier><identifier type="ChapterID">10</identifier><identifier type="ChapterID">Chap10</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer Berlin Heidelberg, 2004</accessCondition><recordInfo><recordContentSource>SPRINGER</recordContentSource><recordOrigin>Springer-Verlag Berlin Heidelberg, 2004</recordOrigin></recordInfo></mods></metadata></istex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Ticri/CIDE/explor/TelematiV1/Data/Istex/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002217 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 002217 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Ticri/CIDE
|area= TelematiV1
|flux= Istex
|étape= Corpus
|type= RBID
|clé= ISTEX:F16EC372915570209346ECBAC440F10BF2284998
|texte= Probabilistic Methods in State Space Analysis
}}
| This area was generated with Dilib version V0.6.31. |  |