Decidability of Parameterized Verification (Record no. 84969)

000 -LEADER
fixed length control field 03907nam a22005535i 4500
001 - CONTROL NUMBER
control field 978-3-031-02011-7
005 - DATE AND TIME OF LATEST TRANSACTION
control field 20240730163753.0
008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION
fixed length control field 220601s2015 sz | s |||| 0|eng d
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
ISBN 9783031020117
-- 978-3-031-02011-7
082 04 - CLASSIFICATION NUMBER
Call Number 004
100 1# - AUTHOR NAME
Author Bloem, Roderick.
245 10 - TITLE STATEMENT
Title Decidability of Parameterized Verification
250 ## - EDITION STATEMENT
Edition statement 1st ed. 2015.
300 ## - PHYSICAL DESCRIPTION
Number of Pages XI, 158 p.
490 1# - SERIES STATEMENT
Series statement Synthesis Lectures on Distributed Computing Theory,
505 0# - FORMATTED CONTENTS NOTE
Remark 2 Acknowledgments -- 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 ## - 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 ����(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.
700 1# - AUTHOR 2
Author 2 Jacobs, Swen.
700 1# - AUTHOR 2
Author 2 Kalimov, Ayrat.
700 1# - AUTHOR 2
Author 2 Konnov, Igor.
856 40 - ELECTRONIC LOCATION AND ACCESS
Uniform Resource Identifier https://doi.org/10.1007/978-3-031-02011-7
942 ## - ADDED ENTRY ELEMENTS (KOHA)
Koha item type eBooks
264 #1 -
-- Cham :
-- Springer International Publishing :
-- Imprint: Springer,
-- 2015.
336 ## -
-- text
-- txt
-- rdacontent
337 ## -
-- computer
-- c
-- rdamedia
338 ## -
-- online resource
-- cr
-- rdacarrier
347 ## -
-- text file
-- PDF
-- rda
650 #0 - SUBJECT ADDED ENTRY--SUBJECT 1
-- Computer science.
650 #0 - SUBJECT ADDED ENTRY--SUBJECT 1
-- Coding theory.
650 #0 - SUBJECT ADDED ENTRY--SUBJECT 1
-- Information theory.
650 #0 - SUBJECT ADDED ENTRY--SUBJECT 1
-- Data structures (Computer science).
650 14 - SUBJECT ADDED ENTRY--SUBJECT 1
-- Computer Science.
650 24 - SUBJECT ADDED ENTRY--SUBJECT 1
-- Coding and Information Theory.
650 24 - SUBJECT ADDED ENTRY--SUBJECT 1
-- Data Structures and Information Theory.
830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE
-- 2155-1634
912 ## -
-- ZDB-2-SXSC

No items available.