acknowledgments
We would like to thank the anonymous reviewers for their valuable comments. Research supported in part by NSF awards
CCR-0133583, CNS-0509230, and CCF-0523863.
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. caires, l., and cardelli, l. a spatial
logic for concurrency (part i). Inf.
Comput. 186, 2 (2003), 194–235.
6. caires, l., and cardelli, l. a spatial
logic for concurrency (part ii). Theor.
Comput. Sci. 322, 3 (2004), 517–565.
7. deoliveira, i., and cugnasca, P.
checking safe trajectories of
aircraft using hybrid automata. in
Proceedings of SAFECOMP 2002.
springer-Verlag, sept. 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. henzinger, t.a. the theory of
hybrid automata. in Proceedings of
11th IEEE Symposium on Logic in
Computer Science, 1996, 278–293.
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. kwon, y., and agha, g. scalable
modeling and performance evaluation
of wireless sensor networks. in IEEE
RT Tech. and App. Symp., 2006, 49–58.
15. lowe, d.g. object recognition from
local scale-invariant features. in
Proceedings of the International
Conference on Computer Vision 2,
1999, 1150–1157.
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. manna, Z., and Pnueli, a. The
Temporal Logic of Reactive and
Concurrent Systems: Specification.
springer, 1992.
19. Pereira, f., and desousa, J.
coordinated control of networked
vehicles: an autonomous underwater
system. Aut. Remote Ctrl. 65, 7
(2004), 1037–1045.
20. shusterman, e., and feder, m.
image compression via improved
quadtree decomposition algorithms.
IEEE Trans. Image Processing 3, 2
(mar. 1994), 207–215.
Radu Grosu
( grosu@cs.sunysb.edu), department of
computer science, stony Brook university,
stony Brook, ny.
Scott A. Smolka
( sas@cs.sunysb.edu), department of
computer science, stony Brook university,
stony Brook, ny.
Flavio Corradini
( flavio.corradini@unicam.it), department
of mathematics and computer science,
university of camerino, camerino (mc),
italy.
© 2009 acm 0001-0782/09/0300 $5.00
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.
IE T Syst. Biol., 2 (Jan. 2008), 24–32.
Anita Wasilewska
( anita@cs.sunysb.edu), department of
computer science, stony Brook university,
stony Brook, ny.
Emilia Entcheva
( emilia.entcheva@sunysb.edu), department
of Biomedical engineering, stony Brook
university, stony Brook, ny.
Ezio Bartocci
( ezio.bartocci@unicam.it), department
of mathematics and computer science,
university of camerino, camerino (mc),
italy. currently visiting the department
of computer science, stony Brook
university, stony Brook, ny.
You’ve come a long way.
Share what you’ve learned.
ACM has partnered with MentorNet, the award-winning nonprofit e-mentoring network in engineering,
science and mathematics. MentorNet’s award-winning One-on-One Mentoring Programs pair ACM
student members with mentors from industry, government, higher education, and other sectors.
• Communicate by email about career goals, course work, and many other topics.
• Spend just 20 minutes a week - and make a huge difference in a student’s life.
• Take part in a lively online community of professionals and students all over the world.
Make a difference to a student in your field.
Sign up today at: www.mentornet.net
Find out more at: www.acm.org/mentornet
MentorNet’s sponsors include 3M Foundation, ACM, Alcoa Foundation, Agilent Technologies, Amylin Pharmaceuticals, Bechtel Group Foundation, Cisco
Systems, Hewlett-Packard Company, IBM Corporation, Intel Foundation, Lockheed Martin Space Systems, National Science Foundation, Naval Research
Laboratory, NVIDIA, Sandia National Laboratories, Schlumberger, S.D. Bechtel, Jr. Foundation, Texas Instruments, and The Henry Luce Foundation.
