Counterexample Generation for Infinite-State Chemical Reaction Networks

TL;DR

This paper introduces a novel SMT-based bounded model checking approach for generating counterexamples in infinite-state chemical reaction networks, effectively identifying critical property-violating paths with high probability.

Contribution

It presents the first method for counterexample generation in infinite-state CRNs using SMT solving, with optimizations for scalability to large models.

Findings

Successfully generated counterexamples for complex CRN models

Scalable approach with divide-and-conquer optimization

Effective identification of high-probability violating paths

Abstract

Counterexample generation is an indispensable part of model checking process. In stochastic model checking, counterexample generation is a challenging problem as it is not enough to find a single trace that violates the given property. Instead, a potentially large set of traces with enough probability to violate the property needs to be found. This paper considers counterexample generation for chemical reaction network (CRN) models with potentially infinite state space. A method based on bounded model checking using SMT solving is developed for counterexample generation for CRNs. It intends to find a small set of property violating paths of a given model such that they collectively have a total probability that is above a given threshold. A unique challenge is due to the highly connected state space of CRNs where a counterexample is only a tiny subset of all property violating paths. To address such challenges, this paper presents a number of optimizations including a divide-and-conquer technique to scale up the counterexample generation method for large CRN models. This paper reports results from experiments on a number of infinite-state CRN models.