000 | 03907nam a22005535i 4500 | ||
---|---|---|---|
001 | 978-3-031-02011-7 | ||
003 | DE-He213 | ||
005 | 20240730163753.0 | ||
007 | cr nn 008mamaa | ||
008 | 220601s2015 sz | s |||| 0|eng d | ||
020 |
_a9783031020117 _9978-3-031-02011-7 |
||
024 | 7 |
_a10.1007/978-3-031-02011-7 _2doi |
|
050 | 4 | _aQA75.5-76.95 | |
072 | 7 |
_aUY _2bicssc |
|
072 | 7 |
_aCOM000000 _2bisacsh |
|
072 | 7 |
_aUY _2thema |
|
082 | 0 | 4 |
_a004 _223 |
100 | 1 |
_aBloem, Roderick. _eauthor. _4aut _4http://id.loc.gov/vocabulary/relators/aut _980485 |
|
245 | 1 | 0 |
_aDecidability of Parameterized Verification _h[electronic resource] / _cby Roderick Bloem, Swen Jacobs, Ayrat Kalimov, Igor Konnov. |
250 | _a1st ed. 2015. | ||
264 | 1 |
_aCham : _bSpringer International Publishing : _bImprint: Springer, _c2015. |
|
300 |
_aXI, 158 p. _bonline resource. |
||
336 |
_atext _btxt _2rdacontent |
||
337 |
_acomputer _bc _2rdamedia |
||
338 |
_aonline resource _bcr _2rdacarrier |
||
347 |
_atext file _bPDF _2rda |
||
490 | 1 |
_aSynthesis Lectures on Distributed Computing Theory, _x2155-1634 |
|
505 | 0 | _aAcknowledgments -- Introduction -- System Model and Specification Languages -- Standard Proof Machinery -- Token-passing Systems -- Rendezvous and Broadcast -- Guarded Protocols -- Ad Hoc Networks -- Related Work -- Parameterized Model Checking Tools -- Conclusions -- Bibliography -- Authors' Biographies . | |
520 | _aWhile the classic model checking problem is to decide whether a finite system satisfies a specification, the goal of parameterized model checking is to decide, given finite systems ����(n) parameterized by n ∈ ℕ, whether, for all n ∈ ℕ, the system ����(n) satisfies a specification. In this book we consider the important case of ����(n) being a concurrent system, where the number of replicated processes depends on the parameter n but each process is independent of n. Examples are cache coherence protocols, networks of finite-state agents, and systems that solve mutual exclusion or scheduling problems. Further examples are abstractions of systems, where the processes of the original systems actually depend on the parameter. The literature in this area has studied a wealth of computational models based on a variety of synchronization and communication primitives, including token passing, broadcast, and guarded transitions. Often, different terminology is used in the literature, and results are based on implicit assumptions. In this book, we introduce a computational model that unites the central synchronization and communication primitives of many models, and unveils hidden assumptions from the literature. We survey existing decidability and undecidability results, and give a systematic view of the basic problems in this exciting research area. | ||
650 | 0 |
_aComputer science. _99832 |
|
650 | 0 |
_aCoding theory. _94154 |
|
650 | 0 |
_aInformation theory. _914256 |
|
650 | 0 |
_aData structures (Computer science). _98188 |
|
650 | 1 | 4 |
_aComputer Science. _99832 |
650 | 2 | 4 |
_aCoding and Information Theory. _980486 |
650 | 2 | 4 |
_aData Structures and Information Theory. _931923 |
700 | 1 |
_aJacobs, Swen. _eauthor. _4aut _4http://id.loc.gov/vocabulary/relators/aut _980487 |
|
700 | 1 |
_aKalimov, Ayrat. _eauthor. _4aut _4http://id.loc.gov/vocabulary/relators/aut _980488 |
|
700 | 1 |
_aKonnov, Igor. _eauthor. _4aut _4http://id.loc.gov/vocabulary/relators/aut _980489 |
|
710 | 2 |
_aSpringerLink (Online service) _980490 |
|
773 | 0 | _tSpringer Nature eBook | |
776 | 0 | 8 |
_iPrinted edition: _z9783031008832 |
776 | 0 | 8 |
_iPrinted edition: _z9783031031397 |
830 | 0 |
_aSynthesis Lectures on Distributed Computing Theory, _x2155-1634 _980491 |
|
856 | 4 | 0 | _uhttps://doi.org/10.1007/978-3-031-02011-7 |
912 | _aZDB-2-SXSC | ||
942 | _cEBK | ||
999 |
_c84969 _d84969 |