@Mastersthesis{mitra01masters, AUTHOR = "Sayan Mitra", TITLE = "{HIOA} - A Specification Language for Hybrid {I}nput/{O}utput Automata", SCHOOL ="Department of Computer Science and Automation, IISc", ADDRESS = "Indian Institute of Science, Bangalore", YEAR = 2001, url = "research/mastersthesis.ps.gz", pdfurl = "research/mastersthesis.pdf", keywords = {Hybrid systems} }, @inproceedings{MWLF-hscc03, author={Sayan Mitra and Yong Wang and Nancy Lynch and Eric Feron}, title={Safety Verification of Model Helicopter Controller using Hybrid {I}nput/{O}utput Automata}, booktitle={6th International Workshop on Hybrid Systems: Computation and Control (HSCC 2003)}, year={2003}, crossref={HSCC2003}, pages = {343-358}, url = {http://www.springerlink.com/content/9vlmduh36103d221/}, pdfurl = {research/2003/paper033.pdf}, ppturl = {research/presentations/HSCC03.ppt}, keywords = {Hybrid systems}, abstract = {This paper presents an application of the Hybrid Input/Output Automaton (HIOA) framework in verifying a realistic hybrid system. A supervisory pitch controller for a model helicopter system is designed and then verified. The design of the supervisory controller is limited by actuator bandwidth, sensor inaccuracies, and the sampling rates. Verification is carried out by induction over the length of an execution of the composed system. The HIOA model makes the inductive proofs tractable by decomposing them into independent discrete and continuous parts. The paper also presents language constructs for specifying HIOAs.} }, @techreport{MWLF-tr, author={Sayan Mitra and Yong Wang and Nancy Lynch and Eric Feron}, title={Application of Hybrid {I/O} Automata in Safety Verification of Pitch Controller for Model Helicopter System}, type={Technical Report}, number={MIT-LCS-TR-880}, month={January}, year={2003}, institution={MIT Laboratory for Computer Science}, address={Cambridge, MA 02139}, psurl={research/2003/QuanTR02.ps}, keywords = {Hybrid systems}, }, @InProceedings{MA03PVS, author = {Sayan Mitra and Myla Archer}, title = {Developing Strategies for Specialized Theorem Proving about Untimes, Timed, and Hybrid {I/O} Automata}, booktitle = {STRATA 2003}, OPTcrossref = {}, OPTkey = {}, OPTpages = {}, year = {2003}, address = {Rome, Italy}, OPTmonth = {September}, psurl={research/2003/strata.ps}, pdfurl={research/2003/strata.pdf}, keywords = {Automated theorem proving}, }, @InProceedings{ML:CDC04, author ={Sayan Mitra and Daniel Liberzon}, title ={Stability of hybrid automata with average dwell time: an invariant approach}, booktitle ={Proceedings of the 43rd IEEE Conference on Decision and Control}, month = {February}, year = {2005}, address = {Paradise Island, Bahamas}, pdfurl = {research/2004/cdc04.pdf}, keywords = {Hybrid systems}, 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 Input/Output Automaton (HIOA) of is used as the model for hybrid systems, and it is shown that some known stability theorems from system theory can be adapted to be applied in this framework. The average dwell time property of a given automaton is formalized as an invariant of a corresponding transformed automaton, such that the former has average dwell time if and only if the latter satisfies the invariant. Formal verification techniques can be used to check this invariance property. In particular, the HIOA framework facilitates inductive invariant proofs by systematically breaking them down into cases for the discrete actions and continuous trajectories of the automaton. The invariant approach to proving the average dwell time property is illustrated by analyzing the hysteresis switching logic unit of a supervisory control system.}, }, @InProceedings{MA04strat, author = {Sayan Mitra and Myla Archer}, title = {Reusable {PVS} Proof Strategies for Proving Abstraction Properties of {I}/{O} Automata}, booktitle = {STRATEGIES 2004, IJCAR Workshop on strategies in automated deduction}, year = {2004}, address = {Cork, Ireland}, month = {July}, psfurl = {research/2004/strategies.ps.gz}, ppturl = {research/presentations/strategies04.pdf}, keywords = {Automated theorem proving}, }, @InProceedings{KLM04, author = {Dilsun Kaynar and Nancy Lynch and Sayan Mitra}, title = {Specifying and Proving Timing Properties with {TIOA} Tools}, booktitle = {In the work in progress session of the 25th {IEEE} International Real-Time Systems Symposium ({RTSS-WIP})}, year = {2004}, address = {Lisbon, Portugal}, month = {December}, psfurl = {research/2004/wip04.ps.gz}, keywords = {Automated theorem proving} }, @article{MitraA05, author = {Sayan Mitra and Myla Archer}, title = {{PVS} Strategies for Proving Abstraction Properties of Automata.}, journal = {Electronic Notes in Theoretical Computer Science}, volume = 125, number = 2, year = 2005, pages = {45-65}, ee = {http://dx.doi.org/10.1016/j.entcs.2005.01.005}, bibsource = {DBLP, http://dblp.uni-trier.de}, pdfurl = {research/2004/ENTCS05.pdf}, keywords = {Automated theorem proving}, url = {http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B75H1-4FNNN9F-B&_user=571676&_rdoc=1&_fmt=&_orig=search&_sort=d&view=c&_acct=C000029040&_version=1&_urlVersion=0&_userid=571676&md5=6d6175f909435af03f0b9704d27a78a4}, abstract = {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 and the correct abstraction relation between the states of the automata, and then show that this relation is preserved by all corresponding action sequences of the two automata. This paper describes tool support based on the PVS theorem prover that can help users accomplish the second task: proving a candidate abstraction relation correct. This tool support relies on a clean and uniform technique for defining abstraction properties relating automata that uses library theories for defining abstraction relations and templates for specifying automata and abstraction theorems. The paper then describes how the templates and theories allow development of generic, high level PVS strategies that aid in the mechanization of abstraction proofs. These strategies first set up the standard subgoals for the abstraction proofs and then execute the standard initial proof steps for these subgoals, thus making the process of proving abstraction properties in PVS more automated. With suitable supplementary strategies to implement the natural proof steps needed to complete the proofs of any of the standard subgoals remaining to be proved, the abstraction proof strategies can form part of a set of mechanized proof steps that can be used interactively to translate high level proof sketches into PVS proofs. Using timed I/O automata examples taken from the literature, this paper illustrates use of the templates, theories, and strategies described to specify and prove two types of abstraction property: refinement and forward simulation.} }, @InProceedings{CLMT:disc05, author = {Gregory Chockler and Nancy Lynch and Sayan Mitra and Joshua Tauber}, title = { Proving atomicity: an assertional approach}, booktitle = {Proceedings of Nineteenth International Symposium on Distributed Computing ({DISC'05})}, pages = {152 - 168}, year = {2005}, editor = {Pierre Fraigniaud}, volume = { 3724}, OPTnumber = {}, series = {LNCS}, address = { Cracow, Poland }, month = {September}, OPTorganization = {}, publisher = {Springer}, OPTnote = {}, OPTannote = {}, keywords = {Distributed systems}, url = {http://www.springerlink.com/content/1wk299f2vemb15yj/}, pdfurl = {research/2005/disc05.pdf}, abstract = {Atomicity (or linearizability) is a commonly used consistency criterion for distributed services and objects. Although atomic object implementations are abundant, proving that algorithms achieve atomicity has turned out to be a challenging problem. In this paper, we initiate the study of systematic ways of verifying distributed implementations of atomic objects, beginning with read/write objects (registers). Our general approach is to replace the existing operational reasoning about events and partial orders with assertional reasoning about invariants and simulation relations. To this end, we define an abstract state machine that captures the atomicity property and prove correctness of the object implementations by establishing a simulation mapping between the implementation and the specification automata. We demonstrate the generality of our specification by showing that it is implemented by three different read/write register constructions: the message-passing register emulation of Attiya, Bar-Noy and Dolev, its optimized version based on real time, and the shared memory register construction of Vitanyi and Awerbuch. In addition, we show that a simplified version of our specification is implemented by a general atomic object construction based on the Lamport’s replicated state machine algorithm.} }, @InProceedings{LKLM:formats05, author = {Hongping Lim and Dilsun Kaynar and Nancy Lynch and Sayan Mitra}, title = {Translating timed {I/O} automata specifications for theorem proving in {PVS}}, booktitle = {Proceedings of Formal Modelling and Analysis of Timed Systems ({FORMATS'05})}, OPTpages = {}, year = {2005}, OPTeditor = {}, OPTvolume = {3829}, number = {3829}, series = {LNCS}, address = {Uppsala, Sweden}, month = {September}, publisher = {Springer}, keywords = {Formal verification}, url = {http://www.springerlink.com/content/f715l136524q6527/}, pdfurl = {research/2005/formats05.pdf}, pdfslidesurl = {research/presentations/FORMATS.pdf}, abstract = {Timed Input/Output Automaton (TIOA) is a mathematical framework for specification and analysis of systems that involve discrete and continuous evolution. In order to employ an interactive theorem prover in deducing properties of a TIOA, its state-transition based description has to be translated to the language of the theorem prover. In this paper, we describe a tool for translating TIOA to the language of the Prototype Verification System (PVS)---a specification system with an integrated interactive theorem prover. We describe the translation scheme, discuss the design decisions, and briefly present three case studies to illustrate the application the the translator in the verification process.} }, @InProceedings{LML:icnp05, author = {Ben Leong and Sayan Mitra and Barbara Liskov}, title = {Path vector face routing: Geographic routing with local face information}, booktitle = { Proceedings of 13th {IEEE} International Conference on Network Protocols ({ICNP'05})}, OPTcrossref = {}, OPTkey = {}, OPTpages = {}, year = {2005}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, address = {Boston, Massachusetts}, month = {November}, OPTorganization = {}, OPTpublisher = {}, OPTnote = {}, OPTannote = {}, pdfurl = {research/2005/icnp-pvfr.pdf}, url = {http://www2.computer.org/portal/web/csdl/doi/10.1109/ICNP.2005.32}, keywords = {Distributed systems}, abstract = {Existing geographic routing algorithms depend on the planarization of the network connectivity graph for correctness, and the planarization process gives rise to a well-defined notion of faces. In this paper, we demonstrate that we can improve routing performance by storing a small amount of local face information at each node. We present a protocol, Path Vector Exchange Protocol (PVEX), that maintains local face information at each node efficiently, and a new geographic routing algorithm, Greedy Path Vector Face Routing (GPVFR), that achieves better routing performance in terms of both path stretch and hop stretch than existing geographic routing algorithms by exploiting available local face information. Our simulations demonstrate that GPVFR/PVEX achieves significantly reduced path and hop stretch than Greedy Perimeter Stateless Routing (GPSR) and somewhat better performance than Greedy Other Adaptive Face Routing (GOAFR+) over a wide range of network topologies. The cost of this improved performance is a small amount of additional storage, and the bandwidth required for our algorithm is comparable to GPSR and GOAFR+ in quasi-static networks.} } @InProceedings{LMN:cdc05, author = {Nancy Lynch and Sayan Mitra and Tina Nolte}, title = {Motion coordination using virtual nodes}, booktitle = { Proceedings of 44th {IEEE} Conference on Decision and Control ({CDC05})}, OPTcrossref = {}, OPTkey = {}, OPTpages = {}, year = {2005}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, address = {Seville, Spain}, month = {December}, OPTorganization = {}, publisher = {IEEE}, OPTnote = {}, OPTannote = {}, keywords = {Distributed systems}, pdfurl = {research/2005/vn-cdc07.pdf}, abstract = {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 arrange themselves along a predetermined curve in the plane, and can maintain themselves in such a configuration in the presence of changes in the underlying mobile ad hoc network, specifically, when nodes may join or leave the system or may fail. Our strategy is to allow the mobile nodes to implement a virtual layer consisting of mobile client nodes, stationary Virtual Nodes (VNs) at predetermined locations in the plane, and local broadcast communication. The VNs coordinate among themselves to distribute the client nodes relatively evenly among the VNs' regions, and each VN directs its local client nodes to form themselves into the local portion of the target curve.} }, @INPROCEEDINGS{MLL:hscc06, AUTHOR = {Sayan Mitra and Daniel Liberzon and Nancy Lynch}, TITLE = {Verifying Average Dwell Time by Solving Optimization Problems}, BOOKTITLE = {Proceedings of Hybrid Systems: Computation and Control (HSCC 2006)}, KEY = {mllhscc06}, YEAR = 2006, pages = {476-490}, crossref = {HSCC2006}, url = {http://www.springerlink.com/content/x77vn1444121k38r/}, pdfurl = {research/2006/hscc06.pdf}, pdfslidesurl = {research/presentations/HSCC06.pdf}, keywords = {Hybrid systems}, 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 time (ADT) property defines restricted classes of switching signals which provide sufficient conditions for proving stability of switched systems. In this paper, we use a specialization of the Hybrid I/O Automaton model to capture both the discrete and the continuous mechanisms of hybrid systems. Based on this model, we develop methods for automatically verifying ADT properties and present simulation relations for establishing equivalence of hybrid systems with respect to ADT. Given a candidate ADT for a hybrid system, we formulate an optimization problem; a solution of this problem either establishes the ADT property or gives an execution fragment of the system that violates it. For two special classes of hybrid systems, we show that the corresponding optimization problems can be solved using standard mathematical programming techniques.We formally define equivalence of two hybrid systems with respect to ADT and present a simulation relation-based method for proving this equivalence. The proposed methods are applied to verify ADT properties of a linear hysteresis switch and a nondeterministic thermostat.}} } @INPROCEEDINGS{ML:paul06, AUTHOR = {Sayan Mitra and Nancy Lynch}, TITLE = { Approximate simulations for task-structured probabilistic {I/O} automata}, BOOKTITLE = { LICS workshop on Probabilistic Automata and Logics (PAul06)}, YEAR = 2006, ADDRESS = {Seattle, WA}, MONTH = {August}, URL = {http://theory.lcs.mit.edu/~mitras/research/PAul06-final.pdf}, pdfurl = {research/2006/PAul06-final.pdf}, pdfslidesurl = {research/presentations/PAul06.pdf}, ppturl = {research/presentations/PAul06.ppt}, keywords = {Formal verification}, abstract = {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 controlled actions of a PIOA as a means for restricting the nondeterminism in the model. The task-PIOA framework defines exact implementation relations based on inclusion of sets of trace distributions. In this paper we develop the theory of approximate implementations and equivalences for task-PIOAs. We propose a new kind of approximate simulation between task-PIOAs and prove that it is sound with respect to approximate implementations. Our notion of similarity of traces is based on a metric on trace distributions and therefore, we do not require the state spaces nor the space of external actions (output alphabet) of the underlying automata to be metric spaces. We discuss applications of approximate implementations to probabilistic safety verification.} } @ARTICLE{ML:ENTCS07, AUTHOR = {Sayan Mitra and Nancy Lynch}, TITLE = {Proving approximate implementation relations for Probabilistic {I/O} Automata.}, JOURNAL = {Electronic Notes in Theoretical Computer Science}, VOLUME = 174, NUMBER = 8, YEAR = 2007, PAGES = {71-93}, EE = {}, doi = {http://dx.doi.org/10.1016/j.entcs.2006.11.040}, publisher = {Elsevier Science Publishers B. V.}, address = {Amsterdam, The Netherlands, The Netherlands}, keywords = {Formal verification}, url ={http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B75H1-4NX9C9N-7&_user=571676&_rdoc=1&_fmt=&_orig=search&_sort=d&view=c&_acct=C000029040&_version=1&_urlVersion=0&_userid=571676&md5=0a0e5c131ecbe451e5f66a10be9bfdc2}, pdfurl ={research/2007/ENTCS_mitra_lynch_08.pdf}, abstract = {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 locally controlled actions and a task scheduler to resolve nondeterminism. The interaction between a scheduler and an automaton gives rise to a trace distribution—a probability distribution over the set of traces. We define a PIOA to be a (discounted) approximate implementation of another PIOA if the set of trace distributions produced by the first is close to that of the latter, where closeness is measured by the (resp. discounted) uniform metric over trace distributions. We propose simulation functions for proving approximate implementations corresponding to each of the above types of approximate implementation relations. Since our notion of similarity of traces is based on a metric on trace distributions, we do not require the state spaces nor the space of external actions of the automata to be metric spaces. We discuss applications of approximate implementations to verification of probabilistic safety and termination.} }, @INPROCEEDINGS{ALLMU:memocode06, AUTHOR = {Myla Archer and Hongping Lim and Nancy Lynch and Sayan Mitra and Shinya Umeno}, TITLE = { Specifying and Proving Properties of Timed {I/O} Automata in the {TIOA} Toolkit }, BOOKTITLE = {In Fourth ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'06)}, YEAR = 2006, PUBLISHER = {IEEE}, pdfurl = {research/2006/memocode06.pdf}, url = {http://ieeexplore.ieee.org/search/wrapper.jsp?arnumber=1695916}, keywords = {Formal verification}, abstract = {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 real-time software component controlling a physical process. The TIOA model is sufficiently general to subsume other models in use for timed systems. The TIOA toolkit, currently under development, is aimed at supporting system development based on TIOA specifications. The TIOA toolkit is an extension of the IOA toolkit, which provides a specification simulator, code generator, and both model checking and theorem proving support for analyzing specifications. This paper focuses on modeling of timed systems with TIOA and the TAMEbased theorem proving support provided in the TIOA toolkit for proving system properties, including timing properties. Several examples are provided by way of illustration.} } @inproceedings{GrosuM07, author = {Radu Grosu and Sayan Mitra and Pei Ye and Emilia Entcheva and I. V. Ramakrishnan and Scott A. Smolka}, title = {Learning Cycle-Linear Hybrid Automata for Excitable Cells.}, booktitle = {Hybrid Systems: Computation and Control (HSCC 2007)}, year = {2007}, pages = {245-258}, crossref = {HSCC2007}, bibsource = {DBLP, http://dblp.uni-trier.de}, pdfurl = {research/2007/clha_06.pdf}, pdfslidesurl = {research/presentations/CLHA_HSCC07.pdf}, keywords = {Systems biology}, url ={http://www.springerlink.com/content/ft80kx37733m1486/?p=ce29728d55dd44c880214a36bcbadf70&pi=20}, abstract = {We show how to automatically learn the class of Hybrid Automata called Cycle-Linear Hybrid Automata (CLHA) in order to model the behavior of excitable cells. Such cells, whose main purpose is to amplify and propagate an electrical signal known as the action potential (AP), serve as the “biologic transistors” of living organisms. The learning algorithm we propose comprises the following three phases: (1) Geometric analysis of the APs in the training set is used to identify, for each AP, the modes and switching logic of the corresponding Linear Hybrid Automata. (2) For each mode, the modified Prony’s method is used to learn the coefficients of the associated linear flows. (3) The modified Prony’s method is used again to learn the functions that adjust, on a per-cycle basis, the mode dynamics and switching logic of the Linear Hybrid Automata obtained in the first two phases. Our results show that the learned CLHA is able to successfully capture AP morphology and other important excitable-cell properties, such as refractoriness and restitution, up to a prescribed approximation error. Our approach is fully implemented in MATLAB and, to the best of our knowledge, provides the most accurate approximation model for ECs to date.} } @inproceedings{ML:HSCC07, author = {Sayan Mitra and Nancy Lynch}, title = {Trace-based Semantics for Probabilistic Timed I/O Automata}, booktitle = {Hybrid Systems: Computation and Control (HSCC 2007)}, year = {2007}, pages = {718--722}, url ={http://www.springerlink.com/content/4r07k692617666u0/}, pdfurl = {research/2007/151_hscc2007.pdf}, keywords = {Formal verification}, 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 choose the post-state of a discrete transition either nondeterministically or according to (possibly continuous) probability distributions. The framework supports modeling of large systems as compositions of concurrently executing PTIOAs, which interact through shared transition labels. We develop a trace-based semantics for PTIOAs and show that PTIOAs are compositional with respect a new notion of external behavior.} } @PhDThesis{Mitra07PhD, author = {Sayan Mitra}, title ={A Verification Framework for Hybrid Systems}, year = {2007}, month = {September}, school = {Massachusetts Institute of Technology}, address = {Cambridge, MA 02139}, pdfurl = {research/2007/thesis.pdf}, keywords = {Formal verification}, url = {http://dspace.mit.edu/handle/1721.1/42238} } @article{DAEM08, author={Myla Archer and Hongping Lim and Nancy Lynch and Sayan Mitra and Shinya Umeno}, title={Specifying and Proving Properties of Timed {I/O} Automata Using {T}empo}, journal={Design Automation for Embedded Systems}, year=2008, volume = {8}, number = {1-2}, url = {http://www.springerlink.com/content/a82q782044162874/?p=87ae03bf514f48c2a78644d7c6361d6b&pi=1}, pdfurl = {research/2008/DAES_tempo08.pdf}, keywords = {Formal verification}, abstract={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 real-time software component controlling a physical process. The TIOA model is sufficiently general to subsume other models in use for timed systems. The Tempo Toolset, currently under development, is aimed at supporting system development based on TIOA specifications. The Tempo Toolset is an extension of the IOA toolkit, which provides a specification simulator, a code generator, and both model checking and theorem proving support for analyzing specifications. This paper focuses on the modeling of timed systems and their properties with TIOA and on the use of TAME4TIOA, the TAME (Timed Automata Modeling Environment) based theorem proving support provided in Tempo, for proving system properties, including timing properties. Several examples are provided by way of illustration.} } @inproceedings{MC:TPHOLS08, author = {Sayan Mitra and K. Mani Chandy}, title = {A Formalized Theory for Verifying Stability and Convergence of Automata in PVS}, booktitle = {Theorem Proving in Higher Order Logics (TPHOLS 2008)}, year = {2008}, isbn = {}, pages = {230--245}, publisher = {LNCS}, address = {}, url = {http://www.springerlink.com/content/57175hhg02702578/}, pdfurl = {research/2008/paper45.pdf}, keywords = {Formal verification}, abstract = {Correctness of many hybrid and distributed systems require stability and convergence guarantees. Unlike the standard induction principle for verifying invariance, a theory for verifying stability or convergence of automata is currently not available. In this paper, we formalize one such theory proposed by Tsitsiklis.We build on the existing PVS metatheory for untimed, timed, and hybrid input/output automata, and incorporate the concepts about fairness, stability, Lyapunov-like functions, and convergence. The resulting theory provides two sets of sufficient conditions, which when instantiated and verified for particular automata, guarantee convergence and stability, respectively.}, } @article{MLL:TECS08, author = {Sayan Mitra and Daniel Liberzon and Nancy Lynch}, title = {Verifying Average Dwell Time of Hybrid Systems}, booktitle = {ACM Transactions on Embedded Computing Systems}, year = 2008, volume = {8}, issue = {1}, publisher = {ACM}, keywords = {Hybrid systems}, url = {http://portal.acm.org/citation.cfm?id=1457246.1457249&coll=portal&dl=ACM&idx=J840&part=transaction&WantType=Transactions&title=ACM%20Transactions%20on%20Embedded%20Computing%20Systems%20(TECS)}, pdfurl = {research/2008/TECS-2006-0040-Final.pdf}, abstract = {Average dwell time (ADT) properties characterize the rate at which a hybrid system performs mode switches. In this article, we present a set of techniques for verifying ADT properties. The stability of a hybrid system A can be verified by combining these techniques with standard methods for checking stability of the individual modes of A. We introduce a new type of simulation relation for hybrid automata—switching simulation—for establishing that a given automaton A switches more rapidly than another automaton B. We show that the question of whether a given hybrid automaton has ADT ta can be answered either by checking an invariant or by solving an optimization problem. For classes of hybrid automata for which invariants can be checked automatically, the invariant-based method yields an automatic method for verifying ADT; for automata that are outside this class, the invariant has to be checked using inductive techniques. The optimization-based method is automatic and is applicable to a restricted class of initialized hybrid automata. A solution of the optimization problem either gives a counterexample execution that violates the ADT property, or it confirms that the automaton indeed satisfies the property. The optimization and the invariant-based methods can be used in combination to find the unknown ADT of a given hybrid automaton.}, } @inproceedings{MC:FORMATS08, author = {K. Mani Chandy and Sayan Mitra and Concetta Pilotto}, title = {Convergence Verification: From Shared Memory to Partially Synchronous Systems}, booktitle = {Formal Modeling and Analysis of Timed Systems ({FORMATS}`08)}, year = 2008, series = {LNCS}, volume = {5215}, pages = {217--231}, publisher = {Springer Verlag}, pdfurl = {research/2008/paper8-final.pdf}, url = {http://www.springerlink.com/content/f2lx31113444n520/}, pdfslidesurl = {research/presentations/convergence verification.pdf}, keywords = {Distributed systems}, abstract = {Verification of partially synchronous distributed systems is difficult because of inherent concurrency and the potentially large state space of the channels. This paper identifies a subclass of such systems for which convergence properties can be verified based on the proof of convergence for the corresponding discrete-time shared state system. The proof technique extends to the class of systems in which an agent's state evolves continuously over time. The proof technique has been formalized in the PVS interface for timed I/O automata and applied to verify convergence of a mobile agent pattern formation algorithm.} } @inproceedings{GilbertLMN08, author = {Seth Gilbert and Nancy A. Lynch and Sayan Mitra and Tina Nolte}, title = {Self-stabilizing Mobile Robot Formations with Virtual Nodes}, booktitle = {10th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2008)}, year = {2008}, pages = {188-202}, ee = {http://dx.doi.org/10.1007/978-3-540-89335-6_16}, crossref = {DBLP:conf/sss/2008}, bibsource = {DBLP, http://dblp.uni-trier.de}, pdfurl ={research/2008/VI_cood_sss08.pdf}, pdfslidesurl = {research/presentations/SSS2008.pdf}, url = {http://www.springerlink.com/content/hk1163qut8657847/}, keywords = {Distributed systems}, 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 mobile ad hoc network, i.e., nodes joining, leaving, or failing. The mobile robots cooperate to implement a VSA Layer, in which a virtual stationary automaton (VSA) is associated with each region of the plane. The VSAs coordinate among themselves to distribute the robots as needed throughout the plane. The resulting motion coordination protocol is self-stabilizing, in that each robot can begin the execution in any arbitrary state and at any arbitrary location in the plane. In addition, self-stabilization ensures that the robots can adapt to changes in the desired formation.} }, @inproceedings{WMML:HSCC09, author = {Tichakorn Wongpiromsarn and Sayan Mitra and Richard M. Murray and Andrew G. Lamperski}, title = {Periodically Controlled Hybrid Systems: Verifying A Controller for An Autonomous Vehicle}, booktitle = {12th International Conference Hybrid Systems: Computation and Control (HSCC 2009)}, year = {2009}, pages = {396-410}, ee = {http://dx.doi.org/10.1007/978-3-642-00602-9_28}, crossref = {DBLP:conf/hybrid/2009}, url = {http://www.springerlink.com/content/u7kh0794281012w7/}, pdfurl = {research/2009/pchahscc09.pdf}, bibsource = {DBLP, http://dblp.uni-trier.de}, keywords = {Hybrid systems}, abstract = {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 actions may occur in the interim changing the discrete-state or the setpoint. Based on periodicity and subtangential conditions, a new sufficient condition for verifying invariance of PCHAs is presented. This technique is used in verifying safety of the planner-controller subsystem of an autonomous ground vehicle, and in deriving geometric properties of planner generated paths that can be followed safely by the controller under environmental uncertainties.} } @inproceedings{PMV:CONCUR08, author = {Pavithra Prabhakar and Sayan Mitra and Mahesh Viswanathan}, title = {On Convergence of Concurrent Systems under Regular Interactions}, booktitle = {20th International Conference on Concurrency Theory (CONCUR 2009)}, year = {2009}, url ={}, pdfurl = {research/2009/paper_156.pdf}, keywords = {Distributed systems}, abstract = {Convergence is often the key liveness property for distributed systems that interact with physical processes. Techniques for proving convergence (asymptotic stability) have been extensively studied by control theorists. In particular, for the asynchronous model of computation Tsitsiklis provides a set of necessary and sufficient conditions for proving stability and convergence under the assumption that each asynchronous operator (state transition function) is applied infinitely often. This paper generalize these results to obtain necessary and sufficient conditions for systems where the in?nite sequence of operators is a member of an arbitrary omega regular language. This enables us to apply our theory to distributed systems with changing communication topology, node failures and joins. We illustrate an application of the new set of conditions in verifying the convergence of a simple (continuous) consensus protocol.} } @inproceedings{MitraR:MEDHOC04, author = {Sayan Mitra and Jesse Rabek}, title = {Energy efficient connected clusters for mobile ad hoc networks}, booktitle = {Proceedings of 3rd Annual Mediterranean Ad Hoc Networking Workshop ({MED-HOC-NET'04})}, address ={Bodrum, Turkey}, year ={2004}, keywords = {Distributed systems}, abstract = {We propose a power-efficient clustering algorithm for wireless ad hoc networks. This algorithm controls the broadcast power of the nodes in such a way that the resulting network is guaranteed to be connected, clustered, and uses minimum required power for achieving that.} } @article{GLMN:TAAS09, author = {Gilbert, Seth and Lynch, Nancy and Mitra, Sayan and Nolte, Tina}, title = {Self-stabilizing robot formations over unreliable networks}, journal = {Special Issue on Self-adaptive and Self-organizing Wireless Networking Systems of ACM Transactions on Autonomous and Adaptive Systems (TAAS)}, volume = {4}, number = {3}, year = {2009}, issn = {1556-4665}, pages = {1--29}, doi = {http://doi.acm.org/10.1145/1552297.1552300}, publisher = {ACM}, address = {New York, NY, USA}, url ={http://portal.acm.org/ft_gateway.cfm?id=1552300&type=pdf&coll=ACM&dl=ACM&CFID=5352998&CFTOKEN=75194026}, pdfurl = {research/2009/GLMN_TAAS09.pdf}, keywords = {Distributed systems}, abstract ={We describe how a set of mobile robots can arrange themselves on any specified curve on the plane in the presence of dynamic changes both in the underlying ad hoc network and in the set of participating robots. Our strategy is for the mobile robots to implement a self-stabilizing virtual layer consisting of mobile client nodes, stationary Virtual Nodes (VNs), and local broadcast communication. The VNs are associated with predetermined regions in the plane and coordinate among themselves to distribute the client nodes relatively uniformly among the VNs’ regions. Each VN directs its local client nodes to align themselves on the local portion of the target curve. The resulting motion coordination protocol is self-stabilizing, in that each robot can begin the execution in any arbitrary state and at any arbitrary location in the plane. In addition, self-stabilization ensures that the robots can adapt to changes in the desired target formation.} } @inproceedings{DM:SSS09, author = {R. E. Lee DeVille and Sayan Mitra}, title = {Stability of Distributed Algorithms in the face of Incessant Faults}, booktitle = {Proceedings of 11th International Symposium on Stabilization, Safety, and Security of Distributed Systems ({SSS 2009})}, year = {2009}, pdfurl = {research/2009/DM_SSS09.pdf}, address = {Lyon, France}, keywords = {Distributed systems}, abstract = {For large distributed systems built from inexpensive components, one expects to see incessant failures. This paper proposes two models for such faults and analyzes two well-known self-stabilizing algorithms under these fault models. For a small number of processes, the properties of interest are verified automatically using probabilistic model-checking tools. For a large number of processes, these properties are characterized using asymptotic bounds from a direct Markov chain analysis and approximated by numerical simulations.} }