A three-valued model abstraction framework for PCTL* stochastic model checkingVirtual
Stochastic model checking can automatically verify and analyse the software-driven autonomous systems with stochastic behaviors, which is a formal verification technique based on system models. When coping with large-scale systems, it suffers from state space explosion problem very seriously. Model abstraction is a potential technique for mitigating this problem. At present, only a few properties specified by PCTL (Probabilistic Computation Tree Logic), such as probabilistic safety and probabilistic reachability, can be preserved in the practical model abstraction of stochastic model checking, which are the proper subset of PCTL* properties. For dealing with this, an effective and efficient three-valued model abstraction framework for full PCTL* stochastic model checking is proposed in this paper. We propose a new abstract model to preserve full PCTL* properties for nondeterministic and probabilistic system, which orthogonally integrates interval probability of transition and game for nondeterminism. A game-based three-valued PCTL* stochastic model checking algorithm is developed to verify abstract model, and a BPSO (binary particle swarm optimization) algorithm integrated with sample learning is designed to refine the indefinite result of three-valued PCTL* stochastic model checking abstract model. It is proved that full PCTL* properties are preserved when the result of three-valued stochastic model checking is definite, and the efficiency of this framework is demonstrated by some large cases.
paper (ase2022-jf-paper46-upload_original_journal_paper_here.pdf) | 2.25MiB |
Thu 13 OctDisplayed time zone: Eastern Time (US & Canada) change
16:00 - 18:00 | Technical Session 32 - Formal Methods and Models IITool Demonstrations / Journal-first Papers / Research Papers at Banquet B Chair(s): Khouloud Gaaloul University of Michigan - Dearborn | ||
16:00 10mDemonstration | CBMC-SSM: Bounded Model Checking of C Programs with Symbolic Shadow Memory Tool Demonstrations Bernd Fischer Stellenbosch University, South Africa, Salvatore La Torre Università degli Studi di Salerno, Gennaro Parlato University of Molise, Peter Schrammel University of Sussex and Diffblue Ltd | ||
16:10 20mResearch paper | Tseitin or not Tseitin? The Impact of CNF Transformations on Feature-Model Analyses Research Papers Elias Kuiter Otto-von-Guericke-University Magdeburg, Sebastian Krieter University of Ulm, Chico Sundermann University of Ulm, Thomas Thüm University of Ulm, Gunter Saake University of Magdeburg, Germany | ||
16:30 20mPaper | A three-valued model abstraction framework for PCTL* stochastic model checkingVirtual Journal-first Papers Yang Liu Shanghai Maritime University/National University of Singapore, Yan Ma Nanjing University of Finance and Economics / National University of Singapore, Yongsheng Yang Shanghai Maritime University File Attached | ||
16:50 20mResearch paper | Finding and Understanding Incompleteness Bugs in SMT SolversVirtual Research Papers | ||
17:10 20mResearch paper | Checking LTL Satisfiability via End-to-end LearningVirtual Research Papers Weilin Luo School of Computer Science and Engineering, Sun Yat-sen University, Hai Wan School of Data and Computer Science, Sun Yat-sen University, Delong Zhang SUN YAT-SEN UNIVERSITY, Jianfeng Du Guangdong University of Foreign Studies, Hengdi Su SUN YAT-SEN UNIVERSITY | ||
17:30 20mResearch paper | QVIP: An ILP-based Formal Verification Approach for Quantized Neural NetworksVirtual Research Papers Yedi Zhang ShanghaiTech University, Zhe Zhao ShanghaiTech University, Guangke Chen ShanghaiTech University, Fu Song ShanghaiTech University, Min Zhang East China Normal University, Taolue Chen Birkbeck University of London, Jun Sun Singapore Management University |