pdfauthor Verifying Average Dwell Time of Hybrid Systems (2009)
Sayan Mitra, Daniel Liberzon, Nancy Lynch
Average dwell time (ADT) properties characterize the rate at which a hybrid system performs mode switches. In this paper, we present a set of techniques for verifying ADT properties. The stability of...
Periodically Controlled Hybrid Systems: Verifying A Controller for An Autonomous Vehicle (2008)
Wongpiromsarn, Tichakorn, Mitra, Sayan, Murray, Richard M., Lamperski, Andrew
This paper introduces Periodically Controlled Hybrid Automata (PCHA) for describing a class of hybrid control systems. In a PCHA, control actions occur roughly periodically while internal and input...
Abstract PVS Strategies for Proving Abstraction Properties of Automata (2008)
Abstractions are important in specifying and proving properties of complex systems. To prove that a given automaton implements an abstract specification automaton, one must first find the correct...
Verifying Statistical Zero Knowledge with Approximate Implementations ⋆ (2008)
Ling Cheung, Sayan Mitra, Olivier Pereira
Abstract. Statistical zero-knowledge (SZK) properties play an important role in designing cryptographic protocols that enforce honest behavior while maintaining privacy. This paper presents a novel...
S.: Specifying and proving properties of timed I/O automata in the TIOA toolkit (2008)
Myla Archer, Hongping Lim, Nancy Lynch, Sayan Mitra, Shinya Umeno
Timed I/O Automata (TIOA) is a mathematical framework for modeling and verification of distributed systems that involve discrete and continuous dynamics. TIOA can be used for example, to model a...
Sayan Mitra, Daniel Liberzon, Nancy Lynch
The switched system model abstracts away the discrete mechanisms of a hybrid system in terms of an exogenous switching signal. Dwell Time and Average Dwell Time (ADT) criteria, introduced by Morse...
pdfauthor Verifying Average Dwell Time of Hybrid Systems (2008)
Sayan Mitra, Daniel Liberzon, Nancy Lynch
Average dwell time (ADT) properties characterize the rate at which a hybrid system performs mode switches. In this paper, we present a set of techniques for verifying ADT properties. The stability of...
Verifying Statistical Zero Knowledge with Approximate Implementations ⋆ (2008)
Ling Cheung, Sayan Mitra, Olivier Pereira
Abstract. Statistical zero-knowledge (SZK) properties play an important role in designing cryptographic protocols that enforce honest behavior while maintaining privacy. This paper presents a novel...
S.: Specifying and proving properties of timed I/O automata in the TIOA toolkit (2008)
Myla Archer, Hongping Lim, Nancy Lynch, Sayan Mitra, Shinya Umeno
Timed I/O Automata (TIOA) is a mathematical framework for modeling and verification of distributed systems that involve discrete and continuous dynamics. TIOA can be used for example, to model a...
www.elsevier.com/locate/entcs PVS Strategies for Proving Abstraction Properties of Automata (2008)
Abstractions are important in specifying and proving properties of complex systems. To prove that a given automaton implements an abstract specification automaton, one must first find the correct...
Self-stabilizing mobile robot formations with virtual nodes (2008)
Seth Gilbert, Nancy Lynch, Sayan Mitra, Tina Nolte
Abstract. In this paper, we describe how virtual infrastructure can be used to coordinate the motion of mobile robots in a 2-dimensional plane in the presence of dynamic changes in the underlying...
Safety Verication of Model Helicopter Controller using Hybrid Input/Output Automata (2007)
Sayan Mitra, Yong Wang, Nancy Lynch, Eric Feron
Abstract: This paper presents an application of the Hybrid I/O Automaton modelling framework [9] to a realistic hybrid system verication problem. A supervisory pitch controller for ensuring the...
Sayan Mitra, Yong Wang, Nancy Lynch, Eric Feron
Abstract: This paper presents an application of the Hybrid I/O Automaton modelling framework [9] to a realistic hybrid system verication problem. A supervisory pitch controller for ensuring the...
A verification framework for hybrid systems (2007)
Thesis (Ph. D.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2007.
A verification framework for hybrid systems (2007)
Thesis (Ph. D.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2007.
Abstract. We describe the main features of the Probabilistic Timed I/O Automata (PTIOA)—a framework for modeling and analyzing discretely communicating probabilistic hybrid systems. A PTIOA can...
Abstract. We propose the Probabilistic Timed I/O Automaton (PTIOA) framework for modelling and analyzing discretely communicating probabilistic hybrid systems. State transition of a PTIOA can be...
Certified by........................................................................ (2007)
Sayan Mitra, Sayan Mitra, Nancy A. Lynch
Combining discrete state transitions with differential equations, Hybrid system models provide an expressive formalism for describing software systems that interact with a physical environment....
Approximate simulations for task-structured probabilistic I/O automata (2006)
A Probabilistic I/O Automaton (PIOA) is a countable-state automaton model that allows nondeterministic and probabilistic choices in state transitions. A task-PIOA adds a task structure on the locally...
Approximate simulations for task-structured probabilistic I/O automata (2006)
A Probabilistic I/O Automaton (PIOA) is a countable-state automaton model that allows nondeterministic and probabilistic choices in state transitions. A task-PIOA adds a task structure on the locally...
Proving Approximate Implementations for Probabilistic I/O Automata?? Abstract (2006)
In this paper we introduce the notion of approximate implementations for Probabilistic I/O Automata (PIOA) and develop methods for proving such relationships. We employ a task structure on the...
Proving Atomicity: An Assertional Approach (2005)
Chockler, Gregory, Lynch, Nancy, Mitra, Sayan, Tauber, Joshua
Atomicity (or linearizability) is a commonly used consistency criterion for distributed services and objects. Although atomic object implementations are abundant, proving that algorithms achieve...
Proving Atomicity: An Assertional Approach (2005)
Chockler, Gregory, Lynch, Nancy, Mitra, Sayan, Tauber, Joshua
Atomicity (or linearizability) is a commonly used consistency criterion for distributed services and objects. Although atomic object implementations are abundant, proving that algorithms achieve...
Motion Coordination Using Virtual Nodes (2005)
Lynch, Nancy, Mitra, Sayan, Nolte, Tina
We describe how a virtual node abstraction layer can be used to coordinate the motion of real mobile nodes in a region of 2-space. In particular, we consider how nodes in a mobile ad hoc network can...
Motion Coordination Using Virtual Nodes (2005)
Lynch, Nancy, Mitra, Sayan, Nolte, Tina
We describe how a virtual node abstraction layer can be used to coordinate the motion of real mobile nodes in a region of 2-space. In particular, we consider how nodes in a mobile ad hoc network can...
Verifying average dwell time by solving optimization problems (2005)
Sayan Mitra, Nancy Lynch, Daniel Liberzon
Abstract. In the switched system model, discrete mechanisms of a hybrid system are abstracted away in terms of an exogenous switching signal which brings about the mode switches. The Average Dwell...
Path Vector Face Routing: Geographic Routing with Local Face Information (2005)
Ben Leong Sayan, Ben Leong, Sayan Mitra, Barbara Liskov
Existing geographic routing algorithms depend on the planarization of the network connectivity graph for correctness, and the planarization process gives rise to a welldefined notion of...
Verifying average dwell time by solving optimization problems (2005)
Sayan Mitra, Nancy Lynch, Daniel Liberzon
Abstract. In the switched system model, discrete mechanisms of a hybrid system are abstracted away in terms of an exogenous switching signal which brings about the mode switches. The Average Dwell...
Proving atomicity: An assertional approach (2005)
Gregory Chockler, Nancy Lynch, Sayan Mitra, Joshua Tauber
Abstract. Atomicity (or linearizability) is a commonly used consistency criterion for distributed services and objects. Although atomic object implementations are abundant, proving that algorithms...
Verifying average dwell time by solving optimization problems (2005)
Sayan Mitra, Nancy Lynch, Daniel Liberzon
Abstract. In the switched system model, discrete mechanisms of a hybrid system are abstracted away in terms of an exogenous switching signal which brings about the mode switches. The Average Dwell...
Verifying average dwell time by solving optimization problems (2005)
Abstract. A switched system is a hybrid system whose discrete mechanisms are abstracted away in terms of an exogenous switching signal which brings about the mode switches. For switched systems, the...
Proving atomicity: An assertional approach (2005)
Gregory Chockler, Nancy Lynch, Sayan Mitra, Joshua Tauber
Atomicity (or linearizability) is a commonly used consistency criterion for distributed services and objects. Although atomic object implementations are abundant, proving that algorithms achieve...
Stability of hybrid automata with average dwell time: an invariant approach (2004)
Abstract — A formal method based technique is presented for proving the average dwell time property of a hybrid system, which is useful for establishing stability under slow switching. The Hybrid...
Specifying and proving timing properties with TIOA tools (2004)
Dilsun Kaynar, Nancy Lynch, Sayan Mitra
This paper introduces the TIOA specification language for timed systems, for example, communication protocols with timeouts or timing-sensitive distributed algorithms. TIOA specifications denote...
Energy efficient connected clusters for mobile ad hoc networks (2004)
a wireless infrastuctureless network with mobile nodes. Clustering is a common basis for building higher level applications for such networks. The merit of a clustered decomposition depends on the...
Path Vector Face Routing: Geographic Routing with Local Face Information (2004)
this paper, we argue that the above notion of locality is unduly restrictive and propose a new F-locality model, where the set of nodes known to v is the set F (v) of nodes with whom v shares a face...
Stability of hybrid automata with average dwell time: an invariant approach (2004)
Abstract — A formal method based technique is presented for proving the average dwell time property of a hybrid system, which is useful for establishing stability under slow switching. The Hybrid...
Safety verification of model helicopter controller using hybrid input/output automata (2003)
Sayan Mitra, Yong Wang, Nancy Lynch, Eric Feron
Abstract. This paper presents an application of the Hybrid I/O Automaton (HIOA) framework [12] in verifying a realistic hybrid system. A supervisory pitch controller for a model helicopter system is...
I deeply acknowledge the guidance provided by my research supervisor professor L.M. Patnaik. The freedom he offered in my pursuits allowed me to learn a lot about research. For this, and for...
Simcox, Amanda, Mitra, Sayan, Truesdell, Sharon, Paul, Litty, Chen, Ting, Butchar, Jonathan P., ...
Analysis of cells in culture has made substantial contributions to biological research. The versatility and scale of in vitro manipulation and new applications such as high-throughput gene silencing...