Name
Abstract | ||
|---|---|---|
The use of specialised approximations for reachability, instead of exact reachability, has given rise to scalable methods to verify deadlock freedom in the context of distributed finite-state systems. In this work, we extend these approaches to check static properties. These properties capture the immediate/static behaviour of a system. The static nature of these properties make them a good match for the sort of over-approximations we use. Local-deadlock freedom and mutual exclusion are two commonly desired properties for distributed systems that naturally fit into our framework. Local-deadlock freedom, in particular, specifies that no subsystem can reach a permanently blocked state. We show by a series of experiments that our approximate framework can prove such properties for a number of interesting systems, and it can do so more efficiently compared to complete approaches. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.1007/978-3-319-70848-5_15 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Programming language,Computer science,sort,Deadlock,Reachability,Theoretical computer science,Mutual exclusion,Scalability | Conference | 10623 |
ISSN | Citations | PageRank |
0302-9743 | 0 | 0.34 |
References | Authors | |
15 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Pedro R. G. Antonino | 1 | 33 | 4.57 |
| Thomas Gibson-Robinson | 2 | 105 | 10.12 |
| A. W. Roscoe | 3 | 1436 | 247.82 |