Simulation and verification for ion channel noises in neuronal cells

Ion channel noises form the basis of the electrical activity of neurons and have significant clinic implications because these noises reflect how reliable a neuron responses to a given stimulus. Therefore, abundant theoretical work has been done to mathematically model these noises. Traditionally, these noises are numerically simulated in computers but recently a new method called probabilistic model checking has played an increasingly important role in computational biology. In this paper, we model ion channel noises as Continuous-time Markov Chains (CTMCs) and use them as a case study to compare the advantages and disadvantages of simulation and probabilistic model checking. We introduce the algorithms for simulation and demonstrate how to model check the CTMC model of ion channel noises. The results illustrate that simulation is more flexible to implement and closer to real-life observations while model checking can explore all the status of the system and therefore is more suitable to analyze the expected performance and verify important properties. By combining both methods, a deeper insight into ion channel noises can be obtained.