JOURNAL PUBLICATIONS

• Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications (with E.M.Clarke and E.A.Emerson), ACM Transactions On Programming Languages And Systems, Vol.\ 8,No. 2, April 1986, Pages 244-263.
• Complexity of Propositional Linear Temporal Logics (with E.M.Clarke), Journal of the Association for Computing Machinery, Vol. 32,No. 3,July 1985, pp 733-749.
• Can Message Buffers be Axiomatized in Linear Temporal Logic(with E.M.Clarke, N.Francez and A.R.Meyer), Information and Control, Vol. 63, Nos. 1/2, October/November 1984.
• Deciding Full Branching Time Logic (with E.A.Emerson), Information and Control, Vol. 61, No. 3, June 1984.
• A Multiprocess Network Logic with Temporal and Spatial Modalities (with J. Reif), Journal of Computer and System Sciences, Vol. 30, No. 1, February 1985.
• The Complementation Problem for Buchi Automata and Applications to Temporal Logic (with M. Vardi and P. Wolper), Theoretical Computer Science, 49, No 2,3 1987, pp 217-237.
• On Verifying That A Concurrent Program Satisfies A Nondeterministic Specification, Information Processing Letters 32 (1989).
• Reasoning About Systems With Many Processes (with S.M.German), Journal of the ACM, July 1992, Volume 39, Number 3, pp 675-735.
• Reasoning in a Restricted Temporal Logic (with Lenore Zuck), Information and Computation, Vol 102, No 2, February 1993.
• Proving Correctness with respect to Nondeterministic Safety Specifications, Information Processing Letters 39(1991)45-49.
• Quantitative Temporal Reasoning (With E.A. Emerson, Al Mok and Jai Srinivasan), Journal of Real-Time Systems, 4, 331-352 (1992).
• Safety, Liveness and Fairness in Temporal Logic, Formal Aspects in Computing, 1994, vol. 6, pp 495-511.
• Temporal Triggers in Active Databases (with Ouri Wolfson), IEEE Transactions on Knowledge and Data Engineering, Vol 7, No 3, June 1995.
• Symmetry and Modelchecking (with E. A. Emerson), Formal Methods in System Design, 9(1/2), 1996, pp 105-130.
• Using Symmetry When Modelchecking under Fairness Assumptions: An Automata Theoretic Approach (with E. A. Emerson), ACM Transactions on Programming Languages and Systems, Vol. 19, No. 4, JUly 1997.
• Minimization of Communication Cost Through Caching in Mobile Environments (with Ouri Wolfson), IEEE Transactions on Parallel and Distributed Systems, Vol 9, Number 4, April 1998, pp 378-390.
• Incremental Verification of Architecture Specification Language for Real-time Systems (with Jeff Tsai, Avinash Sahay and Ray Paul), To appear in the Journal of Software Engineering and Knowledge Engineering.
• Towards a Theory of Cost Management for Digital Libraries (with Wolfson, Yesha and Sloan), ACM Transactions on Database Systems, Vol. 23(4), Dec. 1998, pp 411-452.
• On-the-fly Modelchecking under Fairness that Exploits Symmetry (with V. Gyuris), Formal Methods in System Design, Vol 15, Issue 3, Nov 1999, pp 217-238.
• Updating and Querying Databases that Track Mobile Units (with O. Wolfson, S. Chamberlin, Y. Yesha), Distrbuted and Parallel Databases, 7(3), 1999.
• Parametrized Verification of Linear Networks using automata as invariants (with V. Gyuris), Formal Aspects of Computing, Vol. 11, pp 402-425, 1999.
• On Model-checking for Fragments of mu-calculus (with E. A. Emerson and C. Jutla), Theoretical Computer Sciecne 258(1-2)(2001)pp 491-522.
• Reasoning about Qualitative Spatial Relationships (with C. Y. Yu), Journal of Automated Reasoning, Vol. 25, no. 4, November 2000, pp 291-328.
• SMC: A Symmetry based Model Checker for safety and liveness properties (with V. Gyuris and E. A. Emerson), ACM Transactions on Software Engineering Methodologies, Vol. 9, No. 2, April 2000, pp 133-166.
• Symmetry and Reduced Symmetry in Model Checking(with P. Godefroid), ACM Transactions on Programming Languages, Volume 26, Issue 4, July 2004, Pages 702-734.
• Employing Symmetry Reductions in Model Checking, Computer Languages, Systems and Structures 30 (2004) pp 99-137 (invited paper).

CONFERENCE PUBLICATIONS

• Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications (with E.M.Clarke and E.A.Emerson), Proceedings Of The 10th Acm Symposium On Principles Of Programming Languages, Austin, Texas, January 1983.
• Complexity of Propositional Linear Temporal Logics (with E.M.Clarke), Proceedings Of The 14th Annual Acm Symposium On Theory Of Computing, Sanfransisco, May 1982.
• Deciding Full Branching Time Logic(with E.A.Emerson), Proceedings Of The 16th Annual ACM Symposium On Theory Of Computing, Washington D.C., April-May 1984.
• A Multiprocess Network Logic with Temporal and Spatial Modalities(with J. Reif), Proceedings Of The 10th International Colloquium On Automata, Languages And Programming, July 1983, Barcelona, Spain.
• The Complementation Problem for Buchi Automata and Applications to Temporal Logic (with M. Vardi and P. Wolper), Proceedings Of The 12th International Colloquium On Automata, Languages And Programming, Greece, August 1985.
• Can Message Buffers be Characterized in Linear Temporal Logic(with E.M.Clarke, N.Francez and Y.Gurevich), Proceedings of ACM SIGACT/SIGOPS Symposium on Principles of Distributed Computing, Ottawa, Canada, 1982.
• Reasoning about Infinite Computations(with M.Vardi, P.Wolper), Proceedings of IEEE Symposium on Foundations of Computer Science, Tucson,Arizona, October, 1983.
• Triple Exponential Decision Procedure for the Logic CTL* (with E. A. Emerson), Workshop on Logics of Programs, Carnegie-Mellon University, Pittsburgh, Pennsylvania, June 1983.
• Distributed Algorithms to Ensure Fair Interprocess Communications, Proceedings ACM SIGACT/SIGOPS Symposium on Principles of Distributed Computing, Vancouver,Canada, August 1984.
• On Characterization of Safety and Liveness Properties in Temporal Logic, Proceedings of the 4th ACM SIGACT/SIGOPS Symposium on Principles of Distributed Computing, Minaki,Canada, August 1985.
• Reasoning with Many Processes (with S. M. German), Proceedings of the second IEEE Symposium On Logic in Computer Science, Cornell University, Ithaca, June 1987.
• On the Eventuality Operator in Temporal Logic (with Lenore Zuck), Proceedings of the second IEEE Symposium On Logic in Computer Science, Cornell University, Ithaca, June 1987.
• Using Temporal Logic for Automatic Verification of Finite State Systems (with M.Browne, E.M.Clarke and E.A.Emerson), Proceedings of the Advanced Course "Logics and Models for Verifications and Specifications of Concurrent Systems", Colle-sur-Loup, France, October 1984, Also Appeared in Springer-verlag Lecture Notes in Computer Science.
• Efficient Distributed Recovery Using Message Logging (With Jennifer Welch), Proceedings Of The 8th Acm Symposium On Principles Of Distributed Computing, August 1989, Edmonton, Canada.
• Quantitative Temporal Reasoning (With E.A. Emerson, Al Mok and Jai Srinivasan), Proceedings Of The Workshop On Automatic Verification Methods For Finite State Systems, June 1989, Grenoble, France.
• Automatic Temporal Verification of Buffer Systems (with Lenore Zuck), Proceedings of the Workshop on Computer Aided Verification, Denmark, June 1991.
• Symmetry and Modelchecking (with E. A. Emerson), Presented at the Fifth International Conference on Computer Aided Verification, Elounda, Crete, Greece June 28- July 1, 1993; Appeared in Lecture Notes in Computer Science 697, Springer-Verlag.
• Modelchecking for fragments of $\mu$-calculus (with E. A. Emerson and C. S. Jutla), Presented at the Fifth International Conference on Computer Aided Verification, Elounda, Crete, Greece June 28- July 1, 1993; Appeared in Lecture Notes in Computer Science 697, Springer-Verlag.
• Verification of a Real-life Protocol Using Symbolic Modelchecking (with V. G. Naik), 6th International Conference on Computer Aided Verification, Stanford, California, June 1994; Also appeared in Springer-Verlag Lecture Notes in Computer Science.
• Data Replication for Mobile Computers (with Y. Huang and O. Wolfson), Proceedings of the ACM-SIGMOD 1994 International Conference on Management of Data, Minneapolis, Minnesotta, May 1994.
• Reasoning about Spatial Relationships in Picture Retrieval Systems (with C. Yu and R. Haddad), Proceedings of the 20th VLDB Conference, Sept 12-15 1994, Santiago, Chile.
• Temporal Conditions and Integrity Constraints (with O. Wolfson), Proceedings of the ACM-SIGMOD 1995 International Conference on Management of Data, San Jose, California, May 1995.
• Temporal Condition Evaluation and Retroactive/Proactive Updates in ACtive Database Systems, International Workshop on Active and Realtime Database Systems, June 1995, Skovde, Sweden.
• Similarity based Retrieval of Pictures Using Indices on Spatial Relationships (with C. Yu et al.), Proceedings of the 21st VLDB Conference, Sept 1995, Zurich, Switzerland.
• Utilizing Symmetry when Modelchecking Under Fairness Assumptions, (with E. A. Emerson), International Conference on Computer Aided Verification, Leize, Belgium, July 1995.
• G-tree: Performance evaluation and application in Fuzzy databases (with C. Yu et al), International Conference on Information and Knowlege Management 1996 ( accepted for presentation).
• Modeling and Querying Moving Objects (with Ouri Wolfson et al),IEEE International Conference on Data Engineering, April 1997, Birmingham, U.K.
• Similarity based Retrieval of Videos (with C. Yu and R. Venkatasubramanian), IEEE International Conference on Data Engineering, April 1997, Birmingham, U.K.
• An Architecture for Consumer-Oriented Online Database Services (with Ouri Wolfson et al), Research Issues in Data Engineering Workshop 1996 (RIDE'96), NewOrleans, Louisiana.
• Modeling and Querying Moving Objects (with Ouri Wolfson et al), IEEE International Conference on Data Engineering, April 1997, Birmingham, U.K.
• Similarity based Retrieval of Videos (with C. Yu and R. Venkatasubramanian), IEEE International Conference on Data Engineering, April 1997, Birmingham, U.K.
• On-the-fly Modelchecking under Fairness that Exploits Symmetry (with V. Gyuris), 9th International Conference on Computer Aided Verification, Haifa, Israel, June 1997; Springer-Verlag Lecture Notes in Computer Science 1254.
• Parametrized Verification of Linear Networks using Automata as Invariants, 9th International Conference on Computer Aided Verification, Haifa, Israel, June 1997; Springer-Verlag Lecture Notes in Computer Science 1254.
• SMC: A Symmetry based ModelChecker for Verification of Liveness Properties, Preliminary version presented in 9th International Conference on Computer Aided Verification, Haifa, Israel, June 1997; Springer-Verlag Lecture Notes in Computer Science 1254.
• Query Processing in Video Retrieval Systems (with K. Liu, C. Yu and Rishie), 14th Intnl Conference on Data Engineering, Orlando, Florida, March 1998.
• View Maintenance in Mobile Computing (with O. Wolfson, S. Dao, K. Narayanan, R. Raj), SIGMOD RECORD, Association of Computing Machinery Press, Dec. 1995.
• Symmetry Reductions in Model Checking (with Clarke, Emerson and Jha), 10th International Conference on Computer Aided Verification, Vancouver, Canada, June 1998.
• Databases for Tracking Mobile Units in Real Time (with O. Wolfson et al), Proceedings of the Seventh International Conference on Database Theory (ICDT), Jerusalem, Israel, Jan. 10-12, 1999, also to appear in the Springer-Verlag Lecture Notes in Computer Science.
• DOMINO : Database for Moving Object Tracking (with O. Wolfson et al), ACM Symposium on Modification of Data (demo paper), June 1999, Philadelphia, Pennsylvania.
• Tracking Objects using Database TechnologY: DOMINO, (with O. Wolfson, et al), The fourth workshop on Next Generation Information Technologies and Systems (NGITS '99), Israel, July 1999.
• Symmetry and Reduced Symmetry in Modelchecking (with P. Godefroid), International Conference on Computer Aided Verification, July 2001, Paris, France.
• Similarity based Retrieval from Sequence Databases using Automata as Queries (with Tao Hu and Vikas Choudhry), Eleventh International Conference on Knowledge and Information Management, Nov 4-9, 2002, McLean, VA.
• Formal Languages and Algorithms for Similarity based Retrieval from Sequence Databases, 12th International Conference on Foundations of Software Technology and Theoretical Computer Science, Dec 12-14, 2002, Indian Institute of Technology, Kanpur; Also to in Springer-Verlag Lecture Notes in Computer Science.
• An Economic Model for Resource Exchange in Mobile Peer to Peer Networks (with O. Wolfson and B. Xu), 16th International Conference on Scientific and Statistical Database Management (SSDBM), June 2004, Santorini Island, Greece.
• Applications of a Transportation Information Architecture, (with J. Dillenbrug, Nelson et al), Proc. of the IEEE International conference on networking, Sensing, and Control (ICNSC 2004), Taipei, Taiwan, Mar. 2004.
• Checking Extended CTL properties using Guarded Quotient Structures (with Xiaodong Wang, Min Zhou), Proceedings of IEEE Sysmposium on Software Engineering and Formal Methods, Beijing, Septmeber 2004.
• Model checking of Systems employing Commutative Functions (with Xiaodong Wang, Min Zhou), To be presented at the International Conference on Verification, Model checking and Abstract Interpretation, Paris, January, 2005.
• Language based Policy Analysis in SPKI Trust Management Systems (with Arun Eamani) To be presented at the Fourth Annual PKI Annual R\&D Workshop: Multuple Paths to Trust, NIST Gaithersburg, Maryland, April 2005.
• Taming Interface Specifications (with T. Margaria, B. Steffan and L. D. Zuck), revised version of the paper that appeared in CONCUR 2005 conference, Sept 2005.

OTHER REFEREED ARTICLES

• Retrieval of Pictures Using Approximate Matching (with Clement Yu), a chapter in the book ``Multimedia Databases---Issues and Research Directions'', Edited by V.S. Subrahmanian and Sushil Jajodia, Springer-Verlag 1996.

OTHER ARTICLES

• Triggers on Database Histories (with Ouri Wolfson), Bulletin of the Technical Committee on Data Engineering, December 1992, Vol 15, No 1-4, IEEE Compute Society.
• Scholarly Review on Concurrency appeared in IEEE Computing Reviews; also published in SIGACT NEWS.
• A Graph Model for Wong and Youseffi's Decomposition - A Strategy for Query Processing, Tech Report TR-06-81, Aiken Computational Laboratory, Harvard University 1981.