Abstract reduction in directed model checking CCS processes
Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
This paper proposes an interesting and effective approach to address state explosion issues that typically affect the verification of concurrent systems. In particular, the developed technique is applied to systems specified as sets of processes in the Calculus of Communicating Systems (CSS) and it is based on the combined use of semantic abstraction and heuristic search during state-space exploration. Semantic abstraction is achieved by considering, during the verification of a given property, only the subset of actions of the system behaviour that may impact on its satisfaction. Toward this, the authors introduce a suitable temporal logic for specifying system properties, called selective mu-calculus, which is derived from mu-calculus by modifying the modal operators so that only interesting actions can appear in the formulae. The selective mu-calculus has the same expressiveness of mu-calculus but enables to define a non-standard operational semantics which, in turn, allows the construction of an abstract transition system that has remarkably less states than the standard one. In particular, the operational semantics of the selective mu-calculus is based on a transition relation which abstracts from non-interesting actions but remembers the number of actual actions that must be performed in order to execute an interesting one. Such information is exploited by the heuristic employed during the state-space exploration. The use of heuristic search algorithms for driving the exploration of the state space are at the basis of direct model-checking techniques. The authors show how the non-standard semantics for the selective mu-calculus can be further exploited for defining an heuristic function which estimates the cost to reach a goal node from the current one. In particular, they prove that such function is admissible, viz. it never overestimates the actual cost, and then allows to exploit both greedy and optimal, e.g. A*, search strategies. The reported experimental results, which were conducted on a set of standard benchmark case studies, confirm that the approach performs better than traditional techniques mainly for that regards the state reduction. Only in some cases the employed time is a little bit worse. In conclusion, the manuscript, which is well written and almost self contained, shows how a clever combination of abstraction techniques and heuristic search, results in a good tool for harnessing the state explosion problem. Table 4 contains some typos in \textbf{Res}\(_2\) and \textbf{Res}\(_3\).
- Formal verification of concurrent systems via directed model checking
- Using heuristic search for finding deadlocks in concurrent systems
- Reduced models for efficient CCS verification
- Automated Technology for Verification and Analysis
- Compositionality and locality for improving model checking in the selective mu-calculus
- \(\text{DELFIN}^+\): an efficient deadlock detection tool for CCS processes
- Abstractions and pattern databases: the quest for succinctness and accuracy
- An introduction to the -calculus.
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Efficient verification of a multicast protocol for mobile computing
- Formal verification of concurrent systems via directed model checking
- Graph-Based Algorithms for Boolean Function Manipulation
- Guided model checking with a Bayesian meta-heuristic
- scientific article; zbMATH DE number 438994 (Why is no real title available?)
- scientific article; zbMATH DE number 42752 (Why is no real title available?)
- scientific article; zbMATH DE number 177511 (Why is no real title available?)
- scientific article; zbMATH DE number 734956 (Why is no real title available?)
- scientific article; zbMATH DE number 1746648 (Why is no real title available?)
- scientific article; zbMATH DE number 4119603 (Why is no real title available?)
- scientific article; zbMATH DE number 2087636 (Why is no real title available?)
- scientific article; zbMATH DE number 2102708 (Why is no real title available?)
- Local model checking in the modal mu-calculus
- Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
- Selective mu-calculus and formula-based equivalence of transition systems
- A local approach for temporal model checking of Java bytecode
- Using heuristic search for finding deadlocks in concurrent systems
- Formal verification of concurrent systems via directed model checking
- Extended beam search for non-exhaustive state space analysis
- Reduced models for efficient CCS verification
- \(\text{DELFIN}^+\): an efficient deadlock detection tool for CCS processes
This page was built for publication: Abstract reduction in directed model checking CCS processes
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q715051)
