Tue 18 Jan 2022 10:50 - 11:20 at Salon I - Probabilistic Systems Chair(s): Pavithra Prabhakar

Stochastic model checking (SMC) is a formal verification technique for the analysis of systems with probabilistic behavior. Scalability has been a major limiting factor for SMC tools to analyze real-world systems with large or infinite state spaces. The infinite-state Continuous-time Markov Chain (CTMC) model checker, STAMINA, tackles this problem by selectively exploring only a portion of a model’s state space, where a majority of the probability mass resides, to efficiently give an accurate probability bound to properties under verification. In this paper, we present two major improvements to STAMINA, namely, a method of calculating and distributing estimated state reachability probabilities that improves state space truncation efficiency and combination of the previous two CTMC analyses into one for generating the probability bound. Demonstration of the improvements on several benchmark examples, including hazard analysis of infinite-state combinational genetic circuits, yield significant savings in both run-time and state space size (and hence memory), compared to both the previous version of STAMINA and the infinite-state CTMC model checker INFAMY. The improved STAMINA demonstrates significant scalability to allow for the verification of complex real-world infinite-state systems.

Tue 18 Jan

Displayed time zone: Eastern Time (US & Canada) change

10:20 - 11:50
Probabilistic SystemsVMCAI at Salon I
Chair(s): Pavithra Prabhakar Kansas State University
10:20
30m
Paper
Out of Control: Reducing Probabilistic Models by Control-State EliminationInPerson
VMCAI
Tobias Winkler RWTH Aachen University, Johannes Lehmann RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University
10:50
30m
Paper
STAMINA 2.0: Improving Scalability of Infinite-StateStochastic Model CheckingRemote
VMCAI
Riley Roberts Utah State University, Thakur Neupane The MathWorks, Inc., Lukas Buecherl University of Colorado, Boulder, Chris Myers University of Colorado, Boulder, Zhen Zhang Utah State University
11:20
30m
Paper
EPMC Gets Knowledge in Multi-Agent SystemsRemote
VMCAI
Chen Fu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Ernst Moritz Hahn University of Twente, Yong Li Institute of Software, Chinese Academy of Sciences, Sven Schewe University of Liverpool, Meng Sun Peking University, Andrea Turrini State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun Zhang Institute of Software, Chinese Academy of Sciences