Sayan Mitra's home page at MIT

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.

Publications

Formal models and analysis

: Proving approximate implementation relations for Probabilistic I/O Automata. With Nancy Lynch.
In Electronic Notes in Theoretical Computer Science , 174(8), pages 71-93.
[ bib | .pdf ]
: Trace-based semantics of Probabilistic timed I/O automata. With Nancy Lynch.
To appear in Hybrid Systems: Computation and Control (HSCC 07), LNCS 4416, pages 245-258, April 2007.
[ bib | .pdf | full version with proofs ]
: 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 | Version submitted for journal review .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, Santa Barbara, CA, March 2006. Springer.
[ bib | .pdf | full version .pdf | Version submitted for journal review .pdf ]
: 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]
: 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 ]

Language and tools

: 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 ]
: 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 ]
: 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 ]
: 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) ]
: TIOA Language. Dilsun Kaynar, Nancy Lynch and Steve Garland. MIT Computer Science and Artificial Intelligence Laboratory, Cambridge, MA, 2005.
[ bib | pdf ]
: 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 ]

Applications: systems biology, security, wireless networks, mobile robots

: Verifying Statistical Zero Knowledge with Approximate Implementations. With Ling Cheung and Olivier Pereira.
Submitted for review, February 2007.
[ bib | .pdf ]
: 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 ]
: 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 ]
: 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]
: 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 ]
: 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 ]

Some recent 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.

Sayan Mitra