Probabilistic Methods in State Space Analysis
Identifieur interne : 001D30 ( Istex/Checkpoint ); précédent : 001D29; suivant : 001D31Probabilistic Methods in State Space Analysis
Auteurs : Matthias Kuntz [Allemagne] ; Kai Lampka [Allemagne]Source :
- 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
Affiliations:
Links toward previous steps (curation, corpus...)
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></author><author><name sortKey="Lampka, Kai" sort="Lampka, Kai" uniqKey="Lampka K" first="Kai" last="Lampka">Kai Lampka</name></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><idno type="wicri:Area/Istex/Curation">002217</idno><idno type="wicri:Area/Istex/Checkpoint">001D30</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001D30</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></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country></affiliation></author><author><name sortKey="Lampka, Kai" sort="Lampka, Kai" uniqKey="Lampka K" first="Kai" last="Lampka">Kai Lampka</name><affiliation></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country></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><affiliations><list><country><li>Allemagne</li></country></list><tree><country name="Allemagne"><noRegion><name sortKey="Kuntz, Matthias" sort="Kuntz, Matthias" uniqKey="Kuntz M" first="Matthias" last="Kuntz">Matthias Kuntz</name></noRegion><name sortKey="Lampka, Kai" sort="Lampka, Kai" uniqKey="Lampka K" first="Kai" last="Lampka">Kai Lampka</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Ticri/CIDE/explor/TelematiV1/Data/Istex/Checkpoint
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001D30 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Checkpoint/biblio.hfd -nk 001D30 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Ticri/CIDE
|area= TelematiV1
|flux= Istex
|étape= Checkpoint
|type= RBID
|clé= ISTEX:F16EC372915570209346ECBAC440F10BF2284998
|texte= Probabilistic Methods in State Space Analysis
}}
| This area was generated with Dilib version V0.6.31. |  |