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