Publications Areas Presentations Bibliography Scholar DBLP

Current research interests

Modelling and analysis of real-time, hybrid and probabilistic systems. Software tools for and applications of the above. Typical applications include control systems, robotics, mobile networks, biological systems. The goal of my research is (a) to develop the foundations for analyzing hybrid systems and (b) to facilitate design and verification of actual systems by creating software tools for synthesis, simulation, and verification.

Related Software

The Timed I/O Automaton Language (TIOA) provides the semantic basis for the Tempo Toolset. This toolset is being implemented by researchers at MIT, UConn, and VeroModo Inc. The toolset currently consists of a simulator for TIOA specifications, an interface to the UPPAAL model checker, and an interface to the PVS theorem prover. I have contributed to the development of the TIOA Language and the PVS-interface. For example, the translation scheme of this paper and the strategies proposed in this paper are embodied in the current version of the Tempo toolset.

In this page I intend to collect benchmarks for hybrid systems analysis tools.

Publications and Preprints


A Verification Framework for Hybrid Systems.
Ph.D. Thesis. Massachusetts Institute of Technology, Cambridge, MA 02139, September 2007.
[ bib | .pdf ]

Verifying Statistical Zero Knowledge with Approximate Implementations. With Ling Cheung and Olivier Pereira.
Submitted for review, February 2007.
[ bib | .pdf ]

Trace-based semantics of Probabilistic timed I/O automata. With Nancy Lynch.
In Hybrid Systems: Computation and Control (HSCC 07), LNCS 4416, pages 718-722, April 2007.
[ bib | .pdf | full version with proofs ]

Learning Cycle-linear hybrid automata of excitable cell models. With Radu Grosu, Pei Ye, Scott Smolka, Emilia Entcheva, and I.V. Ramakrishnan.
In Hybrid Systems: Computation and Control (HSCC 07), LNCS 4416, pages 245-258, April 2007.
[ bib | .pdf ]

Proving approximate implementation relations for Probabilistic I/O Automata. With Nancy Lynch.
In Electronic Notes in Theoretical Computer Science , volume 174, number 8, pages 71-93.
[ bib | .pdf ]


Approximate simulations for task-structured probabilistic I/O automata. With Nancy Lynch. LICS workshop on Probabilistic Automata and Logics (PAul06), Seattle, WA, August 2006.
[ bib | .pdf ]

Specifying and Proving Properties of Timed I/O Automata in the TIOA Toolkit . With Myla Archer, HongPing Lim, Nancy Lynch and Shinya Umeno. In Fourth ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'06) .
[ bib | .pdf ]

Verifying average dwell time by solving optimization problems. With Daniel Liberzon and Nancy Lynch. In Ashish Tiwari and Joao P. Hespanha, editors, Hybrid Systems: Computation and Control (HSCC 06), LNCS 3927, Santa Barbara, CA, March 2006. Springer.
[ bib | .pdf | full version .pdf | Version submitted for journal review .pdf ]


PVS strategies for proving abstraction properties of automata. With Myla Archer. Electronic Notes in Theoretical Computer Science, 125(2):45-65, 2005.
[ bib | .pdf (from ENTCS) |.pdf (local) ]

Proving atomicity: an assertional approach. With Gregory Chockler, Nancy Lynch and Joshua Tauber. In Pierre Fraigniaud, editor, Proceedings of Nineteenth International Symposium on Distributed Computing (DISC'05), volume 3724 of LNCS, pages 152 - 168, Cracow, Poland, September 2005. Springer.
[ bib | .pdf | full version .pdf]

Path vector face routing: Geographic routing with local face information. With Ben Leong and Barbara Liskov. In Proceedings of 13th IEEE International Conference on Network Protocols (ICNP'05), Boston, Massachusetts, November 2005.
[ bib | .pdf ]

Translating timed I/O automata specifications for theorem proving in PVS. Hongping Lim, Dilsun Kaynar and Nancy Lynch. In Proceedings of Formal Modelling and Analysis of Timed Systems (FORMATS'05), number 3829 in LNCS, Uppsala, Sweden, September 2005. Springer.
[ bib | .pdf ]

TIOA Language. With Dilsun Kaynar, Nancy Lynch and Steve Garland. MIT Computer Science and Artificial Intelligence Laboratory, Cambridge, MA, 2005.
[ bib | pdf ]

Motion coordination using virtual nodes. With Nancy Lynch and Tina Nolte. In Proceedings of 44th IEEE Conference on Decision and Control (CDC05), Seville, Spain, December.
[ bib | .pdf | bib for Tech-Report | Tech-Report MIT-LCS-TR-986]


Stability of hybrid automata with average dwell time: an invariant approach. With Daniel Liberzon. In Proceedings of the 43rd IEEE Conference on Decision and Control, Paradise Island, Bahamas, February 2005.
[ bib | .pdf | full version .pdf ]

Specifying and proving timing properties with TIOA tools. Dilsun Kaynar, Nancy Lynch, and Sayan Mitra. In In the work in progress session of the 25th IEEE International Real-Time Systems Symposium (RTSS-WIP), Lisbon, Portugal, December 2004.
[ bib | .ps.gz ]

Energy efficient connected clusters for mobile ad hoc networks. With Jesse Rabek. Third Annual Mediterranean Ad Hoc Networking Workshop (MED-HOC-NET'04), Bodrum, Turkey, 2004.
[ bib| .pdf ]

Reusable PVS proof strategies for proving abstraction properties of I/O automata. With Myla Archer. In STRATEGIES 2004, IJCAR Workshop on strategies in automated deduction, Cork, Ireland, July 2004. (Short version of this ENTCS paper)
[ bib | .ps.gz | A position paper on the same topic appeared in STRATA'03 .ps ]


Safety verification of model helicopter controller using hybrid Input/Output automata. With Yong Wang, Nancy Lynch, and Eric Feron. In HSCC'03, Hybrid System: Computation and Control, Prague, the Czech Republic, April 3-5 2003. Available as LNCS volume 2623, pages 343-358. Springer.
[ bib | .ps | bib for Tech-Report | Tech-Report MIT-LCS-TR-880 ]


HIOA - a specification language for hybrid Input/Output automata. Sayan Mitra. Master's thesis, Department of Computer Science and Automation, IISc, Indian Institute of Science, Bangalore, 2001.
[ bib | .ps.gz ]


Learning Cycle-Linear Hybrid Automata for Excitable Cells, HSCC`07, Pisa, Italy, April 2007. .pdf slides
Verifying Hybrid Systems: Stability and Implementations, Invited talk at the Self-Organizing Systems group meeting, University of Washington, Seattle, WA, January 2007.
Approximate Simulations for Task-PIOAs (90 min talk), TDS Seminar, Cambridge, MA, October 06. .pdf slides
Approximate Simulations for Task-PIOAs, PAuL 06, Seattle, WA, August 06. .pdf slides
Verifying Average Dwell Time through Optimization, HSCC 06, Santa Barbara, CA, March 06. .pdf slides
Translating TIOA specs for theorem proving in PVS, FORMATS 05, Uppsala, Sweden, Sept 05. .pdf slides
Motion coordination with virtual nodes, TDS Seminar, MIT, March 2005 .ppt slides
Formal models for stability anaysis of hybrid systems, My RQE talk, MIT, Dec 2004 .ppt slides
Modeling and Analysis of Complex Computational Systems, MURI Review, UIUC, June 2004 .ppt slides
Strategies for Proving Abstraction Properties... STRATEGIES/IJCAR, 2004, Cork, Ireland. .ppt slides
Building PVS Interfaces for Abstraction Proofs (Extended), TDS Seminar, MIT, 2003 .ppt slides
Verification of Helicopter System HSCC Prague, Czech Republic April 3-5, 2003 .ppt slides

Copyright Notice: The material presented here is to ensure timely dissemination of scholarly work. All persons copying this information are expected to adhere to the terms/constraints invoked by each author's copyright.

Publications Areas Presentations Bibliography Scholar DBLP