Improved Model Checking Algorithm for Mobile Ambients
- Resource Type
- Conference
- Authors
- Jiang, Hua; Li, Lingxiang
- Source
- 2023 4th International Symposium on Computer Engineering and Intelligent Communications (ISCEIC) Computer Engineering and Intelligent Communications (ISCEIC), 2023 4th International Symposium on. :319-323 Aug, 2023
- Subject
- Communication, Networking and Broadcast Technologies
Computing and Processing
Signal Processing and Analysis
Computational modeling
Model checking
Mathematical models
Calculus
Mobile computing
model checking
mobile ambient
predicate μ-calculus
nested predicate equations
- Language
Mobile Ambients is a formal model for describing distributed mobile computing. It has become a hot topic in the formal theoretical research of mobile computing in the past 20 years, and very fruitful theoretical research results have been achieved in this area. An efficient model checking algorithm for Mobile Ambients is one of the key factors to promote the practical application of such theoretical results. In this paper, we improve the core algorithm of model checking on finite control Mobile Ambients for the predicate ambient logic of first-order $\mu-$calculus, which reduces the number of times to calculate the fixed-point initial value from computation nodes and hence accelerates computing fixed-points in the model checking algorithm.