Behaviorial Model of Heart Tissue
We first start with modeling the electrical behaviors of a heart tissue. A whole model of the heart consists of node automata (N0) which models the timed transitions among different time periods with different behaviors after the tissue is depolarized. The heart can then be modeled as: where N can be arbitarily large.
Study complex and chaotic heart conditions like Atrial Fibrillation.
Creating spatial and temporal map of the heart during Electrophysiology Studies
Abstract conduction delay with paths
In this abstraction we replace the cond state of N0 with path automata. The heart model H0 can be replaced by . A more general abstraction abstracts 3 nodes and 2 paths into 2 nodes and 1 path:. With this property we can further abstract the structure of the model. The heart model H0.5 can be further abstracted into where m=9 in the structure shown on the right.
Study heart conditions with additional pathways including reentry circuits.
Patient-specific heart model for general Electrophysiology Study.
Merging equivalent states
At this abstraction level, we merge the RRP state with the Rest state in the node automata and Double with the Idle state in the path automata due to the same behavior. We also further abstract the structure of the heart model so H1 can be abstracted with . The AV node has very large ERP period thus cannot be abstracted away.
Verify pacemaker algorithms in which the blocking property of the AV node cannot be ignored
Replacing the blocking property of ERP with non-determinism
The node automata do not trigger path conduction in response to external activation during its ERP state. In this abstraction level, this function is replaced by a non-determnistic transition in the path automata, as shown in the figure on the right. As a result of the abstraction, the AV node can be abstracted away and the heart model H2 can be abstracted by .
Verify pacemaker algorithms in which A-V conduction cannot be ignored
Abstracting the conduction property with non-determinism
Since the pacemaker only has two leads, the structure of the heart model can be further reduced to two node automata which can generate inputs to the pacemaker without timing constraints. The heart model H3 can be further abstracted to . This heart model covers all possible inputs to the pacemaker and is our most abstracted model.
Verify pacemaker algorithms with unconditional properties.