NDLI: Sticks and stones: a coding scheme for parameterized verification

Please wait, while we are loading the content...

Lamport on mutual exclusion: 27 years of planting seeds

The ABCD's of Paxos

Sticks and stones: a coding scheme for parameterized verification

Leslie Lamport's properties and actions

Implementing atomic objects in a dynamic environment

The LATEX legacy: 2.09 and all that

On beyond registers: wait-free readable objects

Restoration by path concatenation: fast recovery of MPLS paths

Computing almost shortest paths

Distributed MST for constant diameter graphs

String realizers of posets with applications to distributed computing

On the generalized dining philosophers problem

An improved lower bound for the time complexity of mutual exclusion

A note on group mutual exclusion

Nearly optimal perfectly-periodic schedules

The do-all problem in broadcast networks

Competitive concurrent distributed queuing

Bandwidth constrained placement in a WAN

Compressed bloom filters

A hierarchy of conditions for consensus solvability

The concurrency hierarchy, and algorithms for unbounded concurrency

On scalable and efficient distributed failure detectors

Average probe complexity in quorum systems

Lock-free reference counting

Detecting distributed cycles of garbage in large-scale systems

The IceCube approach to the reconciliation of divergent replicas

Exploitng event stream interpretation in publish-subscribe systems

Replicated condition monitoring

Computing property-preserving behaviour abstractions from trace reductions: abstraction-based verification of linear-time properties under fairness

Reliability and performance of hierarchical RAID with multiple controllers

Distributed multi-broadcast in unknown radio networks

Analysis of a cone-based distributed topology control algorithm for wireless multi-hop networks

Practical multi-candidate election system

An optimally robust hybrid mix network

Selective private function evaluation with applications to private statistics

Optimal scheduling for disconnected cooperation

Adding networks

Randomized shared queues

Dynamic input/output automata, a formal model for dynamic systems

A framework for semantic reasoning about Byzantine quorum systems

An efficient communication strategy for ad-hoc mobile networks

Correction: practical implementations of non-blocking synchronization primitives

Sticks and stones: a coding scheme for parameterized verification

Content Provider	ACM Digital Library
Author	Pnueli, Amir
Abstract	We consider the problem of Uniform Algorithmic Verification of Parameterized Systems, which requires establishing in a single verification effort the correctness of a parameterized family of systems for any value of the parameter. As has been observed by several researchers, using regular expressions or equivalent formalisms (e.g. WS1S) as assertional language, we can perform symbolic model checking of systems of unbounded number of states.We start by showing that the verification problem can be viewed as taking place in a space of 3 dimensions: Time, Control, and Data. We will illustrate how regular expressions can be naturally applied to deal with any of these dimensions in case it becomes unbounded. Unfortunately, extending the tool of regular expressions to 2 dimension leads to undecidability.We therefore consider alternate ways of dealing with systems which have both unbounded control and unbounded data. By appropriate abstractions and encoding it is frequently possible to encode these two dimensions within a single dimension, using a coding scheme to which we refer as “sticks and stones”. The method will be illustrated on parameterized versions of the Bakery and Peterson's algorithms for mutual exclusion. Among other things, we will show that, in some cases, we can use languages more expressive than regular expressions and still get manageable verification algorithms. This is, for example, the case of Peterson's algorithm for N processes, which cannot be analyzed in terms of purely regular expressions.
File Format	PDF
ISBN	1581133839
DOI	10.1145/383962.383971
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2001-08-01
Publisher Place	New York
Access Restriction	Subscribed
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in