We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:


Current browse context:


Change to browse by:


References & Citations

DBLP - CS Bibliography


(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Counterexample Generation for Infinite-State Chemical Reaction Networks

Authors: Mohammad Ahmadi (1), Zhen Zhang (2), Chris Myers (3), Chris Winstead (2), Hao Zheng (1) ((1) University of South Florida,(2) Utah State University,(3) University of Colorado Boulder)
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.
Subjects: Logic in Computer Science (cs.LO)
Cite as: arXiv:2207.05207 [cs.LO]
  (or arXiv:2207.05207v1 [cs.LO] for this version)

Submission history

From: Mohammad Ahmadi [view email]
[v1] Mon, 11 Jul 2022 21:53:36 GMT (1825kb,D)

Link back to: arXiv, form interface, contact.