000			03608nam a22004455i 4500
999			_c387310 _d387310
001			387310
003			ES-MaUEC
005			20230312131449.0
006			a||||fo|||| 00| 0
007			cr nn 008mamaa
008			220601s2015 sz | s |||| 0|eng d
020			_a9783031020117
024	7		_a10.1007/978-3-031-02011-7 _2doi
040			_aES-MaUEC _bspa _cES-MaUEC _dES-MaUEC
050		4	_aQA76.76.V47 _b2015 EB
100	1		_aBloem, Roderick P. _eautor _4aut _4http://id.loc.gov/vocabulary/relators/aut _9687271
245	1	0	_aDecidability of Parameterized Verification _cby Roderick Bloem, Swen Jacobs, Ayrat Kalimov, Igor Konnov
250			_a1st edition 2015
264		1	_aCham _bSpringer International Publishing _c2015
300			_a1 recurso en línea (XI, 158 páginas)
336			_atexto _btxt _2rdacontent
337			_aelectrónico _bc _2rdamedia
338			_arecurso electrónico _bcr _2rdacarrier
347			_aarchivo de texto _bPDF
490	0		_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.
988			_aSynthesis Collection of Technology_2015
650		7	_2embne _9414956 _aSoftware _xVerificación
650		7	_2embne _9156434 _aProceso distribuido (Informática)
700	1		_aJacobs, Swen _eautor _4aut _4http://id.loc.gov/vocabulary/relators/aut _9687272
700	1		_aKalimov, Ayrat _eautor _4aut _4http://id.loc.gov/vocabulary/relators/aut _9687273
700	1		_aKonnov, Igor, _eautor _4aut _4http://id.loc.gov/vocabulary/relators/aut _9687274 _d1958-
776	0	8	_iPrinted edition: _z9783031008832
776	0	8	_iPrinted edition: _z9783031031397
856	4	0	_uhttps://go.openathens.net/redirector/universidadeuropea.es?url=https://doi.org/10.1007/978-3-031-02011-7 _zAcceso a este recurso digital (usuarios Universidad Europea de Madrid)
942			_2lcc _cLE
998			_b03/2023 _dz _esc _zSI