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
2007
-
-
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 ]
2006
-
-
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
]
2005
-
-
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]
2004
-
-
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
]
2003
-
-
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
]
2001
-
-
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 ]
Presentations
-
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.