| 000 | 07253nam a2200793 i 4500 | ||
|---|---|---|---|
| 001 | 7284816 | ||
| 003 | IEEE | ||
| 005 | 20200413152919.0 | ||
| 006 | m eo d | ||
| 007 | cr cn |||m|||a | ||
| 008 | 151025s2015 caua foab 000 0 eng d | ||
| 020 |
_a9781627057448 _qebook |
||
| 020 |
_z9781627057431 _qprint |
||
| 024 | 7 |
_a10.2200/S00658ED1V01Y201508DCT013 _2doi |
|
| 035 | _a(CaBNVSL)swl00405740 | ||
| 035 | _a(OCoLC)926621333 | ||
| 040 |
_aCaBNVSL _beng _erda _cCaBNVSL _dCaBNVSL |
||
| 050 | 4 |
_aQA76.76.V47 _bB563 2015 |
|
| 082 | 0 | 4 |
_a005.14 _223 |
| 100 | 1 |
_aBloem, Roderick P., _eauthor. |
|
| 245 | 1 | 0 |
_aDecidability of parameterized verification / _cRoderick Bloem and Ayrat Khalimov, Swen Jacobs, Igor Konnov, Helmut Veith, and Josef Widder, Sasha Rubin. |
| 264 | 1 |
_aSan Rafael, California (1537 Fourth Street, San Rafael, CA 94901 USA) : _bMorgan & Claypool, _c2015. |
|
| 300 |
_a1 PDF (xi, 158 pages) : _billustrations. |
||
| 336 |
_atext _2rdacontent |
||
| 337 |
_aelectronic _2isbdmedia |
||
| 338 |
_aonline resource _2rdacarrier |
||
| 490 | 1 |
_aSynthesis lectures on distributed computing theory, _x2155-1634 ; _v# 13 |
|
| 538 | _aMode of access: World Wide Web. | ||
| 538 | _aSystem requirements: Adobe Acrobat Reader. | ||
| 500 | _aPart of: Synthesis digital library of engineering and computer science. | ||
| 504 | _aIncludes bibliographical references (pages 145-155). | ||
| 505 | 0 | _a1. Introduction -- 1.1 Motivation -- 1.2 Who should read this book? -- 1.3 Organization of the book -- | |
| 505 | 8 | _a2. System model and specification languages -- 2.1 Preliminary terminology and definitions -- 2.2 System model -- 2.2.1 Some standard synchronization primitives -- 2.2.2 Runs and deadlocks -- 2.3 Parameterized family of uniform concurrent systems -- 2.4 Parameterized specifications -- 2.4.1 Indexed temporal logics -- 2.4.2 Action-based specifications -- 2.4.3 Specifications in the literature -- 2.5 Model checking problems for concurrent systems -- 2.5.1 Computability assumptions -- | |
| 505 | 8 | _a3. Standard proof machinery -- 3.1 Techniques to prove undecidability of PMCP -- 3.2 How to prove decidability of the PMCP -- 3.2.1 Well-structured transition systems -- 3.2.2 Vector addition systems with states (and petri nets) -- 3.2.3 Decompositions and cutoffs -- | |
| 505 | 8 | _a4. Token-passing systems -- 4.1 System model -- 4.1.1 Direction-aware parameterized systems -- 4.1.2 Token-passing systems -- 4.2 Results for direction-unaware token-passing systems -- 4.2.1 Decidability for simple token-passing in uni-directional rings -- 4.2.2 Decidability for simple token-passing in graphs -- 4.2.3 Undecidability results for multi-valued tokens -- 4.3 Results for direction-aware token-passing systems -- 4.3.1 Cutoffs for change-bounded tokens in bi-directional rings -- 4.3.2 Undecidability for direction-aware TPSs -- 4.4 Discussion -- 4.4.1 Variations of the model -- | |
| 505 | 8 | _a5. Rendezvous and broadcast -- 5.1 System model -- 5.2 Decidability results -- 5.2.1 Counter representation -- 5.2.2 Decidability for all three primitives -- 5.2.3 Decidability for pairwise rendezvous -- 5.3 Undecidability results -- 5.3.1 Undecidability for broadcast -- 5.3.2 Undecidability for asynchronous rendezvous -- 5.4 Discussion -- 5.4.1 Variations of the model -- | |
| 505 | 8 | _a6. Guarded protocols -- 6.1 Motivating example -- 6.2 System model -- 6.2.1 Classes of guarded protocols -- 6.2.2 Specifications -- 6.3 Undecidability: Boolean and conjunctive guards -- 6.4 Decidability: init-conjunctive and disjunctive guards -- 6.4.1 Preliminaries -- 6.4.2 Proof schemas -- 6.4.3 Init-conjunctive guards -- 6.4.4 Disjunctive guards -- 6.5 Disjunctive guards vs. rendezvous -- 6.6 Variations on the model: guards and synchronization primitives -- 6.7 Discussion -- | |
| 505 | 8 | _a7. Ad hoc networks -- 7.1 Running example -- 7.2 System model -- 7.3 PMC problems for ad hoc networks -- 7.4 Parameterized connectivity graphs BPk, BPCk, BDk, C, all -- 7.5 Results for (non-lossy) AHNs -- 7.5.1 Undecidability results for (non-lossy) AHNs -- 7.5.2 Decidability results for (non-lossy) AHNs -- 7.6 Decidability results for lossy ad hoc networks -- 7.7 Discussion -- 7.7.1 Variations of the model -- | |
| 505 | 8 | _a8. Related work -- 8.1 Abstraction techniques -- 8.2 Regular model checking -- 8.3 Symbolic techniques -- 8.4 Dynamic cutoff detection -- 8.5 Network invariants -- 8.6 Invisible invariants -- 8.7 Other aspiring approaches -- | |
| 505 | 8 | _a9. Parameterized model checking tools -- | |
| 505 | 8 | _a10. Conclusions -- Bibliography -- Authors' biographies. | |
| 506 | 1 | _aAbstract freely available; full-text restricted to subscribers or individual document purchasers. | |
| 510 | 0 | _aCompendex | |
| 510 | 0 | _aINSPEC | |
| 510 | 0 | _aGoogle scholar | |
| 510 | 0 | _aGoogle book search | |
| 520 | 3 | _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 M(n) parameterized by n / N, whether, for all n / N, the system M(n) satisfies a specification. In this book we consider the important case of M(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. | |
| 530 | _aAlso available in print. | ||
| 588 | _aTitle from PDF title page (viewed on October 25, 2015). | ||
| 650 | 0 |
_aComputer software _xVerification. |
|
| 650 | 0 |
_aElectronic data processing _xDistributed processing. |
|
| 653 | _aparametrized model checking | ||
| 653 | _aconcurrent systems | ||
| 653 | _adistributed systems | ||
| 653 | _aformal verification | ||
| 653 | _amodel checking | ||
| 653 | _adecidability | ||
| 653 | _acutoffs | ||
| 700 | 1 |
_aJacobs, Swen., _eauthor. |
|
| 700 | 1 |
_aKhalimov, Ayrat., _eauthor. |
|
| 700 | 1 |
_aKonnov, Igor, _d1958-, _eauthor. |
|
| 700 | 1 |
_aRubin, Sasha., _eauthor. |
|
| 700 | 1 |
_aVeith, Helmut., _eauthor. |
|
| 700 | 1 |
_aWidder, Josef., _eauthor. |
|
| 776 | 0 | 8 |
_iPrint version: _z9781627057431 |
| 830 | 0 | _aSynthesis digital library of engineering and computer science. | |
| 830 | 0 |
_aSynthesis lectures on distributed computing theory ; _v# 13. _x2155-1634 |
|
| 856 | 4 | 2 |
_3Abstract with links to resource _uhttp://ieeexplore.ieee.org/servlet/opac?bknumber=7284816 |
| 999 |
_c562162 _d562162 |
||