Modeling and Analysis of Stochastic Systems with Perturbed Parameters

Project Member(s): Feng, Y.

Funding or Partner Organisation: Ministry of Education, Singapore

Start year: 2015

Summary: Probabilistic model checking is a verification technology that has been studied actively for more than a decade and is being applied in domains as diverse as network protocol design and systems biology. The models and case studies to which the technology has been applied typically employ well understood theoretical probability distributions (such as the use of a fair coin toss) to simplify the specification of stochastic model elements (thereby allowing probabilities and other key quantitative parameters to be specified with simple constant values). However, the technology has limited ability to deal with more complex stochastic characteristics of real-world problems and systems, which are governed by probabilities and other quantitative parameters whose values must be empirically estimated and/or vary over time. In this project, we propose to apply matrix perturbation theory and related mathematical techniques to model and analyse the effects of perturbations to probability parameters in the verifications of probabilistic systems. Our initial research has demonstrated that small perturbations to probability parameters can produce quantitatively and even qualitatively significant variation in computed verification results, and existing approaches and tools can be misleading or even invalid. If successful, the project will achieve two significant outcomes: First, it will expand the applicability of probabilistic model checking to a greater range of system models and to system models of greater complexity and realism. Second, by providing a mathematically sound and rigorous characterisation of how the results are affected by perturbations of the model, it will increase the confidence of model builders in the verification results they obtain.

Publications:

Fu, C, Turrini, A, Huang, X, Song, L, Feng, Y & Zhang, L 1970, 'Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems', Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, Twenty-Seventh International Joint Conference on Artificial Intelligence {IJCAI-18}, International Joint Conferences on Artificial Intelligence Organization, Stockholm, Sweden, pp. 4757-4763.
View/Download from: Publisher's site

Feng, Y & Zhang, L 2017, 'Precisely deciding CSL formulas through approximate model checking for CTMCs', Journal of Computer and System Sciences, vol. 89, pp. 361-371.
View/Download from: Publisher's site

Feng, Y & Ying, M 1970, 'Toward Automatic Verification of Quantum Cryptographic Protocols.', CONCUR, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 441-455.

Keywords: Markov chains, parameterized models, perturbation, probabilistic model checking, quantitative verification

FOR Codes: Computation Theory and Mathematics not elsewhere classified, Software Engineering, Expanding Knowledge in the Information and Computing Sciences, Information and Communication Services not elsewhere classified, Theory of computation not elsewhere classified, Empirical software engineering, Other information and communication services not elsewhere classified

Acknowledgement of Country

UTS acknowledges the Gadigal people of the Eora Nation, the Boorooberongal people of the Dharug Nation, the Bidiagal people and the Gamaygal people, upon whose ancestral lands our university stands. We would also like to pay respect to the Elders both past and present, acknowledging them as the traditional custodians of knowledge for these lands.