Symmetry reduction for the local mu-calculus

DOI10.1007/978-3-319-89963-3_22MaRDI QIDQ2324237zbMATH OpenOpenAlexFDO

Authors Kedar S. Namjoshi, Richard Trefler

Publication date 16 September 2019

Full work available at URL https://arxiv.org/abs/1903.10405

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: Model checking large networks of processes is challenging due to state explosion. In many cases, individual processes are isomorphic, but there is insufficient global symmetry to simplify model checking. This work considers the verification of local properties, those defined over the neighborhood of a process. Considerably generalizing earlier results on invariance, it is shown that all local mu-calculus properties, including safety and liveness properties, are preserved by neighborhood symmetries. Hence, it suffices to check them locally over a set of representative process neighborhoods. In general, local verification approximates verification over the global state space; however, if process interactions are outward-facing, the relationship is shown to be exact. For many network topologies, even those with little global symmetry, analysis with representatives provides a significant, even exponential, reduction in the cost of verification. Moreover, it is shown that for network families generated from building-block patterns, neighborhood symmetries are easily determined, and verification over the entire family reduces to verification over a finite set of representative process neighborhoods.

Recommendations

• Local symmetry and compositional verification
• scientific article; zbMATH DE number 1796126
• scientific article; zbMATH DE number 1487862
• scientific article; zbMATH DE number 1418460
• Symmetry Reduction for Probabilistic Model Checking

Cited in

(7)

• Scaling network verification using symmetry and surgery
• Local symmetry and compositional verification
• Uncovering symmetries in irregular process networks
• scientific article; zbMATH DE number 1507205 (Why is no real title available?)
• CONCUR 2004 - Concurrency Theory
• Cut-off theorems for the \textit{PV}-model
• A template-based approach for the generation of abstractable and reducible models of featured networks

This page was built for publication: Symmetry reduction for the local mu-calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2324237)