Name
Abstract | ||
|---|---|---|
The Parameterized Compositional Model Checking Problem PCMCP is to decide, using compositional proofs, whether a property holds for every instance of a parameterized family of process networks. Compositional analysis focuses attention on the neighborhood structure of processes in the network family. For the verification of safety properties, the PCMCP is shown to be much more tractable than the more general Parameterized Model Checking Problem PMCP. For example, the PMCP is undecidable for ring networks while the PCMCP is decidable in polynomial time. This result generalizes to toroidal mesh networks and related networks for describing parallel architectures. Decidable models of the PCMCP are also shown for networks of control and user processes. The results are based on the demonstration of compositional cutoffs; that is, small instances whose compositional proofs generalize to the entire parametric family. There are, however, control-user models where the PCMCP and the PMCP are both undecidable. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1007/978-3-662-49674-9_39 | TACAS |
Field | DocType | Volume |
Discrete mathematics,Parameterized complexity,Model checking,Parametric family,Computer science,Decidability,Theoretical computer science,Mathematical proof,Ring network,Time complexity,Undecidable problem | Conference | 9636 |
ISSN | Citations | PageRank |
0302-9743 | 4 | 0.42 |
References | Authors | |
19 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Kedar S. Namjoshi | 1 | 948 | 50.41 |
| Richard J. Trefler | 2 | 222 | 14.59 |