| 000 -LEADER |
|---|
| fixed length control field |
07253nam a2200793 i 4500 |
| 001 - CONTROL NUMBER |
|---|
| control field |
7284816 |
| 003 - CONTROL NUMBER IDENTIFIER |
|---|
| control field |
IEEE |
| 005 - DATE AND TIME OF LATEST TRANSACTION |
|---|
| control field |
20200413152919.0 |
| 006 - FIXED-LENGTH DATA ELEMENTS--ADDITIONAL MATERIAL CHARACTERISTICS |
|---|
| fixed length control field |
m eo d |
| 007 - PHYSICAL DESCRIPTION FIXED FIELD--GENERAL INFORMATION |
|---|
| fixed length control field |
cr cn |||m|||a |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION |
|---|
| fixed length control field |
151025s2015 caua foab 000 0 eng d |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
9781627057448 |
| Qualifying information |
ebook |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| Canceled/invalid ISBN |
9781627057431 |
| Qualifying information |
print |
| 024 7# - OTHER STANDARD IDENTIFIER |
|---|
| Standard number or code |
10.2200/S00658ED1V01Y201508DCT013 |
| Source of number or code |
doi |
| 035 ## - SYSTEM CONTROL NUMBER |
|---|
| System control number |
(CaBNVSL)swl00405740 |
| 035 ## - SYSTEM CONTROL NUMBER |
|---|
| System control number |
(OCoLC)926621333 |
| 040 ## - CATALOGING SOURCE |
|---|
| Original cataloging agency |
CaBNVSL |
| Language of cataloging |
eng |
| Description conventions |
rda |
| Transcribing agency |
CaBNVSL |
| Modifying agency |
CaBNVSL |
| 050 #4 - LIBRARY OF CONGRESS CALL NUMBER |
|---|
| Classification number |
QA76.76.V47 |
| Item number |
B563 2015 |
| 082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER |
|---|
| Classification number |
005.14 |
| Edition number |
23 |
| 100 1# - MAIN ENTRY--PERSONAL NAME |
|---|
| Personal name |
Bloem, Roderick P., |
| Relator term |
author. |
| 245 10 - TITLE STATEMENT |
|---|
| Title |
Decidability of parameterized verification / |
| Statement of responsibility, etc. |
Roderick Bloem and Ayrat Khalimov, Swen Jacobs, Igor Konnov, Helmut Veith, and Josef Widder, Sasha Rubin. |
| 264 #1 - PRODUCTION, PUBLICATION, DISTRIBUTION, MANUFACTURE, AND COPYRIGHT NOTICE |
|---|
| Place of production, publication, distribution, manufacture |
San Rafael, California (1537 Fourth Street, San Rafael, CA 94901 USA) : |
| Name of producer, publisher, distributor, manufacturer |
Morgan & Claypool, |
| Date of production, publication, distribution, manufacture, or copyright notice |
2015. |
| 300 ## - PHYSICAL DESCRIPTION |
|---|
| Extent |
1 PDF (xi, 158 pages) : |
| Other physical details |
illustrations. |
| 336 ## - CONTENT TYPE |
|---|
| Content type term |
text |
| Source |
rdacontent |
| 337 ## - MEDIA TYPE |
|---|
| Media type term |
electronic |
| Source |
isbdmedia |
| 338 ## - CARRIER TYPE |
|---|
| Carrier type term |
online resource |
| Source |
rdacarrier |
| 490 1# - SERIES STATEMENT |
|---|
| Series statement |
Synthesis lectures on distributed computing theory, |
| International Standard Serial Number |
2155-1634 ; |
| Volume/sequential designation |
# 13 |
| 538 ## - SYSTEM DETAILS NOTE |
|---|
| System details note |
Mode of access: World Wide Web. |
| 538 ## - SYSTEM DETAILS NOTE |
|---|
| System details note |
System requirements: Adobe Acrobat Reader. |
| 500 ## - GENERAL NOTE |
|---|
| General note |
Part of: Synthesis digital library of engineering and computer science. |
| 504 ## - BIBLIOGRAPHY, ETC. NOTE |
|---|
| Bibliography, etc. note |
Includes bibliographical references (pages 145-155). |
| 505 0# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
1. Introduction -- 1.1 Motivation -- 1.2 Who should read this book? -- 1.3 Organization of the book -- |
| 505 8# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
2. 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# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
3. 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# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
4. 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# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
5. 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# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
6. 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# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
7. 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# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
8. 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# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
9. Parameterized model checking tools -- |
| 505 8# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
10. Conclusions -- Bibliography -- Authors' biographies. |
| 506 1# - RESTRICTIONS ON ACCESS NOTE |
|---|
| Terms governing access |
Abstract freely available; full-text restricted to subscribers or individual document purchasers. |
| 510 0# - CITATION/REFERENCES NOTE |
|---|
| Name of source |
Compendex |
| 510 0# - CITATION/REFERENCES NOTE |
|---|
| Name of source |
INSPEC |
| 510 0# - CITATION/REFERENCES NOTE |
|---|
| Name of source |
Google scholar |
| 510 0# - CITATION/REFERENCES NOTE |
|---|
| Name of source |
Google book search |
| 520 3# - SUMMARY, ETC. |
|---|
| Summary, etc. |
While 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 ## - ADDITIONAL PHYSICAL FORM AVAILABLE NOTE |
|---|
| Additional physical form available note |
Also available in print. |
| 588 ## - SOURCE OF DESCRIPTION NOTE |
|---|
| Source of description note |
Title from PDF title page (viewed on October 25, 2015). |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name entry element |
Computer software |
| General subdivision |
Verification. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name entry element |
Electronic data processing |
| General subdivision |
Distributed processing. |
| 653 ## - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
parametrized model checking |
| 653 ## - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
concurrent systems |
| 653 ## - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
distributed systems |
| 653 ## - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
formal verification |
| 653 ## - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
model checking |
| 653 ## - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
decidability |
| 653 ## - INDEX TERM--UNCONTROLLED |
|---|
| Uncontrolled term |
cutoffs |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Jacobs, Swen., |
| Relator term |
author. |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Khalimov, Ayrat., |
| Relator term |
author. |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Konnov, Igor, |
| Dates associated with a name |
1958-, |
| Relator term |
author. |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Rubin, Sasha., |
| Relator term |
author. |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Veith, Helmut., |
| Relator term |
author. |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Widder, Josef., |
| Relator term |
author. |
| 776 08 - ADDITIONAL PHYSICAL FORM ENTRY |
|---|
| Relationship information |
Print version: |
| International Standard Book Number |
9781627057431 |
| 830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE |
|---|
| Uniform title |
Synthesis digital library of engineering and computer science. |
| 830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE |
|---|
| Uniform title |
Synthesis lectures on distributed computing theory ; |
| Volume/sequential designation |
# 13. |
| International Standard Serial Number |
2155-1634 |
| 856 42 - ELECTRONIC LOCATION AND ACCESS |
|---|
| Materials specified |
Abstract with links to resource |
| Uniform Resource Identifier |
http://ieeexplore.ieee.org/servlet/opac?bknumber=7284816 |
