Learning and detecting emergent behavior in networks of cardiac myocytes

ABSTRACT

We address the problem of specifying and detecting emergent behavior in networks of cardiac myocytes, spiral electric waves in particular, a precursor to atrial and ventricular fibrillation. To solve this problem we: (1) apply discrete mode abstraction to the cycle-linear hybrid automata (CLHA) we have recently developed for modeling the behavior of myocyte networks; (2) introduce the new concept of spatial superposition of CLHA modes; (3) develop a new spatial logic, based on spatial superposition, for specifying emergent behavior; (4) devise a new method for learning the formulae of this logic from the spatial patterns under investigation; and (5) apply bounded model checking to detect the onset of spiral waves. We have implemented our methodology as the EMERALD tool suite, a component of our EHA framework for specification, simulation, analysis, and control of excitable hybrid automata. We illustrate the effectiveness of our approach by applying EMERALD to the scalar electrical fields produced by our CELLEXCITE simulation environment for excitable-cell networks.

REFERENCES

• 1: Aiello, M., Benthem, J., and Bezhanishvili, G. Reasoning about space: The modal way. J. Log. Comput. 13, 6 (2003), 889--920.
• 2: Bartocci, E., Corradini, F., Entcheva, E., Grosu, R., and Smolka, S.A. CELLEXCITE: An efficient simulation environment for excitable cells. BMC Bioinformatics, 9, Suppl 2 (2008), S3.
• 3: Biere, A., Cimatti, A., Clarke, E., Strichman, O., and Zhu, Y. Bounded model checking. In Adv. in Comp. vol. 58: Highly Depend. Software. Acad. Press, 2003.
• 4: Bray, M.A., Lin, S.F., Aliev, R.R., Roth, B.J., and Wikswo, J.P.J. Experimental and theoretical analysis of phase singularity dynamics in cardiac tissue. J. Cardiovasc. Electrophysiol. 12, 6 (2001), 716--722.
• 5: Luís Caires , Luca Cardelli, A spatial logic for concurrency (part I), Information and Computation, v.186 n.2, p.194-235, 01 November 2003 [doi>10.1016/S0890-5401(03)00137-8]
• 6: Luís Caires , Luca Cardelli, A spatial logic for concurrency--II, Theoretical Computer Science, v.322 n.3, p.517-565, 6 September 2004 [doi>10.1016/j.tcs.2003.10.041]
• 7: Ítalo Romani de Oliveira , Paulo Sérgio Cugnasca, Checking Safe Trajectories of Aircraft Using Hybrid Automata, Proceedings of the 21st International Conference on Computer Safety, Reliability and Security, p.224-235, September 10-13, 2002
• 8: Frank, E., Hall, M.A., Holmes, G., Kirkby, R., Pfahringer, B. Witten, I.H., and Trigg, L. WEKA: A machine learning workbench for data mining. In The Data Mining and Knowledge Discovery Handbook, 1305--1314. Springer, 2005.
• 9: Ghosh, R., Tiwari, A., and Tomlin, C. Automated symbolic reachability analysis: with application to Delta-Notch signaling automata. In HSCC, 233--248, 2003.
• 10: Grosu, R., Bartocci, E., Corradini, F., Entcheva, E., Smolka, S.A., and Ye, P. EHA: An environment for the specification, simulation, analysis and control of networks of excitable hybrid automata. http://www.cs.sunysb.edu/~eha, 2009.
• 11: Grosu, R., Mitra, S., Ye, P., Entcheva, E., Ramakrishnan, I.V., and Smolka, S.A. Learning cycle-linear hybrid automata for excitable cells. In Proceedings of HSCC'07, the 10th International Conference on Hybrid Systems: Computation and Control, volume 4416 of LNCS, Pisa, Italy, April 2007. Springer Verlag, 245--258.
• 12: T. A. Henzinger, The theory of hybrid automata, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.278, July 27-30, 1996
• 13: Hodgkin, A.L. and Huxley, A.F. A quantitative description of membrane currents and its application to conduction and excitation in nerve. J. Physiol., 117 (1952), 500--544.
• 14: YoungMin Kwon , Gul Agha, Scalable Modeling and Performance Evaluation of Wireless Sensor Networks, Proceedings of the 12th IEEE Real-Time and Embedded Technology and Applications Symposium, p.49-58, April 04-07, 2006 [doi>10.1109/RTAS.2006.39]
• 15: David G. Lowe, Object Recognition from Local Scale-Invariant Features, Proceedings of the International Conference on Computer Vision-Volume 2, p.1150, September 20-25, 1999
• 16: Lu, Y. Concept hierarchy in data mining: Specification, generation and implementation. Master's thesis, Simon Fraser University, Dec. 1997.
• 17: Luo, C.H., and Rudy, Y. A dymanic model of the cardiac ventricular action potential: I. simulations of ionic currents and concentration changes. Circ. Res., 74 (1994), 1071--1096.
• 18: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 19: F. Lobo Pereira , J. Borges De Sousa, Coordinated Control of Networked Vehicles: An Autonomous Underwater System, Automation and Remote Control, v.65 n.7, p.1037-1045, July 2004 [doi>10.1023/B:AURC.0000038711.03622.09]
• 20: Shusterman, E., and Feder, M. Image compression via improved quadtree decomposition algorithms. IEEE Trans. Image Processing 3, 2 (Mar. 1994), 207--215.
• 21: Umeno, S., and Lynch, N. Safety verification of an aircraft landing protocol: A refinement approach. In Proceedings of HSCC 2007, Apr. 2007.
• 22: Wasilewska, A., and Ruiz, E.M. A classification model: Syntax and semantics for classification. In RSFDGrC (2), 2005, 59--68.
• 23: Wedge, N.A., Branicky, M.S., and Cavusoglu, M.C. Computationally efficient cardiac biolectricity models toward whole-heart simulation. In Proceedings of International Conference on IEEE Engineering in Medicine and Biology Society, 2004, 1--4.
• 24: Ye, P., Entcheva, E., Grosu, R., and Smolka, S. Efficient modeling of excitable cells using hybrid automata. In Proceedings of CMSB'05, the Third Workshop on Computational Methods in Systems Biology, Edinburgh, Scotland, April 2005, 216--227.
• 25: Ye, P., Entcheva, E., Smolka, S.A., and Grosu, R. Modeling excitable cells using cycle-linear hybrid automata. IET Syst. Biol., 2 (Jan. 2008), 24--32.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
      D.2.4 Software/Program Verification

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs