Roberto Segala: Publications

Below you find a list of my publications classified by journals, book chapters, edited books, conferences, and others. By clicking on the links you can get abstracts, links to the original publications, author-created copies, links to other relevant documents.
Journals

  • [KPS+09] A Quantitative Doxastic Logic for Probabilistic Processes and Applications to Information-Hiding, R. Canetti, S. Kramer, C. Palamidessi, R. Segala, A. Turrini, C. Braun, R. Segala, in Journal of Applied Non-Classical Logic 19(4), pages 489-516, 2009.

  • [CCK+08] Analyzing Security Protocols Using Time-Bounded Task-PIOAs, R. Canetti, L. Cheung, D. Kaynar, M. Liskov, N. Lynch, O. Pereira, R. Segala, in Discrete Events Dynamic Systems 18(1), March 2008.

  • [LSV07] Observing Branching Structure through Probabilistic Contexts, N. Lynch, R. Segala, F. Vaandrager, in SIAM Journal on Computing, 37(4), pages 977-1013, 2007.

  • [DSS06], Dynamic Load Balancing with Group Communication, S. Dolev, R. Segala, A. Shvartsman, in Theoretical Computer Science 369, pages 348-360, 2006. An extended abstract appears in Proceedings of International Colloquium on Structural Information and Communication Complexity (SIROCCO), Lacanau, France, pages 111-125, July 1999.

  • [CLSV06] Switched PIOA: Parallel Composition via Distributed Scheduling, L. Cheung, N. Lynch, R. Segala, F. Vaandrager, in Theoretical Computer Science, 365, pages 83-108, 2006.

  • [LSV03] Hybrid I/O Automata, N. Lynch, R. Segala, F. Vaandrager, in Information and Computation, 185, pages 105--157, 2003.

  • [KNSS02] Automatic Verification of Real-Time Systems With Discrete Probability Distributions, M. Kwiatkowska, G. Normann, R. Segala, J. Sproston, in Theoretical Computer Science, vol. 282, pages 101--150, 2002. An extended abstract appears in Proceedings of the 5th International AMAST Workshop on Real Time and Probabilistic Systems, LNCS 1601, pages 79-95, May 1999.

  • [PSL00] Verification of the Randomized Consensus Algorithm of Aspnes and Herlihy: a Case Study, A. Pogosyants, R. Segala, N. Lynch, in Distributed Computing, 13(3):155-186, July 2000. An extended abstract appears in Proceedings of WDAG, Saarbrucken, Germany, LNCS 1320, pages 22-36, September 1997.

  • [GSSL98] Liveness in Timed and Untimed Systems, R. Segala, R. Gawlick, J.F. Sogaard-Andersen, N. Lynch, in Information and Computation, 141(2):119-171, 1998. An extended abstract appears in Proceedings of the 21st International Colloquium on Automata, Languages and Programming (ICALP), Jerusalem, Israel, LNCS 820, pages 166-177, 1994. Extended version available as MIT Technical Report number MIT/LCS/TR-587.

  • [Seg97] Quiescence, Fairness, Testing and the notion of Implementation, R. Segala, in Information and Computation, 138(2):194-210, November 1997. An extended abstract appears in Proceedings of the 4th International Conference on Concurrency Theory (CONCUR '93), Hildesheim, Germany, LNCS 715, pages 324-338, August 1993.

  • [SL95] Probabilistic Simulations for Probabilistic Processes, R. Segala, N. Lynch, Nordic Journal of Computing, 2(2):250-273, 1995. An extended abstract appears in Proceedings of the 5th International Conference on Concurrency Theory (CONCUR '94), Uppsala, Sweden, LNCS 836, pages 481-496, August 1994.

  • [DnS95] A Process Algebraic View of I/O automata, R. De Nicola, R. Segala, in Theoretical Computer Science, 138:391-423, March 1995.

  • [LS95] A Comparison of Simulation Techniques and Algebraic Techniques for Verifying Concurrent Systems, N. Lynch, R. Segala, in Journal of Formal Aspects of Computing Science, 7(3):231-265, 1995. An extended abstract appears in Proceedings of the Second North American Process Algebra Workshop, Cornell University, NY, 1993.

Books

Book Chapters

  • [Seg01] Verification of Randomized Distributed Algorithms, Lectures on Formal Methods and Performance Analysis, First EEF/Euro Summer School on Trends in Computer Science, LNCS 2090, pages 232-260, 2001.

Edited Books

  • [CS10] Seventh International Conference on the Quantitative Evaluaiton of Systems (QEST 2010), G. Ciardo and R. Segala, editors, 16-18 September 2010, Williamsburg, USA. IEEE Computer Society 2010.

  • [HS02] Proceedings of the Second Joint Workshop on Process Algebra and Performance Modelling, Probabilistic Methods in Verification, H. Hermanns and R. Segala, editors, LNCS 2399, Copenhagen, Denmark, July 2002.

Conferences

  • [ST10] Conditional Automata: A Tool for Safe Removal of Negligible Events, R. Segala, A. Turrini, in Proceedings of the 21st International Conference on Concurrency Theory (CONCUR '10), Paris, France, LNCS 6269, pages 539-553, August 2010.

  • [ST07] Approximated Computationally Bounded Simulation Relations for Probabilistic Automata, R. Segala, A. Turrini, in Proceedings of the 20th IEEE Computer Security Foundations Symposium, Venice, Italy, pages 140-156, July 2007.

  • [PS07] Logical Characterizations of Bisimulations for Discrete Probabilistic Systems A. Parma, R. Segala, in Proceedings of the 10th International Conference on Foundations of Software Science and Computational Structures (FOSSACS), Braga, Portugal, LNCS 4423, pages 287-301, April 2007.

  • [CCK+06] Time-Bounded Task-PIOAs: A Framework for Analyzing Security Protocols, R. Canetti, L. Cheung, D. Kaynar, M. Liskov, N. Lynch, O. Pereira, R. Segala, in Proceedings of the 20th International Symposium on Distributed Computing (DISC '06), Stockholm, Sweden, LNCS 4167, pages 238-253, September 2006.

  • [Seg06] Probability and Nondeterminism in Operational Models of Concurrency, R. Segala, in Proceedings of the 17th International Conference on Concurrency Theory (CONCUR '06), Bonn, Germany, LNCS 4137, pages 64-78, August 2006. Introductory tutorial.

  • [CCK+06a] Task-Structured Probabilistic I/O Automata. R. Canetti, L. Cheung, D. Kaynar, M. Liskov, N. Lynch, O. Pereira, R. Segala, in Proceedings the 8th International Workshop on Discrete Event Systems (WODES'06), Ann Arbor, Michigan, July 2006.

  • [CCK+06b] Using Task-Structured Probabilistic I/O Automata to Analyze Cryptographic Protocols. R. Canetti, L. Cheung, D. Kaynar, M. Liskov, N. Lynch, O. Pereira, R. Segala, in Proceedings of the Workshop on Formal and Computational Cryptography (FCC '06), pages 34--39, July 2006.

  • [ST05] Comparative Analysis of Bisimulation Relations on Alternating and Non-Alternating Probabilistic Models, R. Segala, A. Turrini, in Proceedings of the Second International Conference on the Quantitative Evaluation of Systems (QEST) 2005, Torino, Italy, pages 44--53, September 2005.

  • [CSKN05] Stochastic Transition Systems for Continuous State Spaces and Non-determinism, S. Cattani, R. Segala, M. Kwiatkowska, G. Norman, in Proceedings of the 8th International Conference on Foundations of Software Science and Computational Structures (FOSSACS), Edinburgh, UK, LNCS 3441, pages 125--139, April 2005.

  • [PS04] Axiomatization of Trace Semantics for Stochastic Nondeterministic Processes, A. Parma, R. Segala, in Proceedings of the First International Conference on the Quantitative Evaluation of Systems (QEST) 2004, Enschede, The Netherlands, pages 294--303, September 2004.

  • [CLSV04] Switched Probabilistic I/O automata, L. Cheung, N. Lynch, R. Segala, F. Vaandrager, in Proceedings of the First International Colloquium on Theoretical Aspects of Computing (ICTAC) 2004, Guiyang, China, LNCS 3407, pages 494--510, September 2004. Extended in [CLSV06].

  • [KLSV03] A Framework for Modeling Timed Systems with Restricted Hybrid Automata, D. Kaynar, N. Lynch, R. Segala, F. Vaandrager, in Proceedings of the 24th IEEE International Real-Time Systems Symposium (RTSS) 2003, Cancun, Mexico, December 2003. Covered extensively in [KLSV06].

  • [LSV03] Compositionality for Probabilistic Automata, N. Lynch, R. Segala, F. Vaandrager, in Proceedings of the 14th International Conference on Concurrency Theory (CONCUR '03), Marseille, France, LNCS 2761, pages 208--221, August 2003. Extended in [LSV07].

  • [CS02] Decision Algorithms for Probabilistic Bisimulation, S. Cattani, R. Segala, in Proceedings of the 13th International Conference on Concurrency Theory (CONCUR '02), Brno, Czech Republic, LNCS 2421, pages 371--385, August 2002.

  • [FS01] Coin Lemmas with Random Variables, Katia Folegati, R. Segala, in Proceedings of the First Joint Workshop on Process Algebra and Performance Modelling, Probabilistic Methods in Verification, Aachen, Germany, LNCS 2165, pages 71-86, September 2001

  • [KNS01] Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM, M. Kwiatkowska, G. Norman, R. Segala, in Proceedings of the 13th International Conference on Computer Aided Verification (CAV) 2001, Paris, France, LNCS 2102, pages 194-206, July 2001

  • [BS01] Axiomatizations for Probabilistic Bisimulation, E. Bandini, R. Segala, in Proceedings of the 28th International Colloquium on Automata, Languages and Programming (ICALP) 2001, Crete, Greece, LNCS 2076, pages 370-381, July 2001

  • [LSV01] Hybrid I/O Automata Revisited, N. Lynch, R. Segala, F. Vaandrager, in Proceedings of the 4th Hybrid Systems Computation and Control (HSCC) 2001, Rome, Italy, LNCS2034, pages 403-417, March 2001. Extended in [LSV03].

  • [KNSS00] Verifying Quantitative Properties of Continuous Probabilistic Real-Time Automata, M. Kwiatkowska, G. Normann, R. Segala, J. Sproston, in Proceedings of the 11th International Conference on Concurrency Theory (CONCUR '00), State College, PA, USA, LNCS 1877, pages 123-137, August 2000.

  • [FGS00] A New Definition of Multilevel Security, R. Focardi, R. Gorrieri, R. Segala, in Proceedings of the Workshop on Issues in the Theory of Security (WITS), Geneve, Switzerland, July 2000.

  • [KNSS00b] Verifying Soft Deadlines with Probabilistic Timed Automata, M. Kwiatkowska, G. Normann, R. Segala, J. Sproston, in Proceedings di WAVe 2000, June 2000.

  • [AKNPS00] Symbolic Model Checking of Concurrent Probabilistic Processes Using MTBDDs and the Kronecker Representation, L. de Alfaro, M. Kwiatkowska, G. Norman, D. Parker, R. Segala, in Proceedings of TACAS 2000, Berlin, LNCS 1785, April 2000.

  • [KNSS99] Automatic Verification of Real-Time Systems With Discrete Probability Distributions, M. Kwiatkowska, G. Normann, R. Segala, J. Sproston, in Proceedings of the 5th International AMAST Workshop on Real Time and Probabilistic Systems, LNCS 1601, pages 79-95, May 1999. Extended in [KNSS99].

  • [DSS99], Dynamic Load Balancing with Group Communication, S. Dolev, R. Segala, A. Shvartsman, in Proceedings of International Colloquium on Structural Information and Communication Complexity (SIROCCO), Lacanau, France, pages 111-125, July 1999. Extended in [DSS99].

  • [Seg98] The Essence of Coin Lemmas, R. Segala, in Proceedings of the first Workshop on Probabilistic Methods in Verification (PROBMIV), Indianapolis, USA, June 1998. A revised version appears in volume 22 of ENTCS.

  • [Seg97a] Compositional Verification of Randomized Distributed Algorithms, R. Segala, in Proceedings of Compositionality - The Significant Difference, Malente/Holstein, Germany, LNCS 1536, pages 515-540, September 1997. Covered extensively in [PSL00].

  • [BDMS98] System Support for Partition-Aware Network Applications, O. Babaoglu, R. Davoli, A. Montresor, R. Segala, in Proceedings of the 18th International Conference on Distributed Computing Systems (ICDCS '98), pages 184-191, Amsterdam, The Netherlands, May 1998.

  • [PSL97] Verification of the Randomized Consensus Algorithm of Aspnes and Herlihy: a Case Study, A. Pogosyants, R. Segala, N. Lynch, in Proceedings of WDAG, Saarbrucken, Germany, LNCS 1320, pages 22-36, September 1997. Covered extensively in [PSL00].

  • [Seg96] Testing Probabilistic Automata , R. Segala, in Proceedings of the 7th International Conference on Concurrency Theory (CONCUR '96), Pisa, Italy, LNCS 1119, pages 299-314, August 1996.

  • [LSVW95] Hybrid I/O Automata, N. Lynch, R. Segala, F. Vaandrager, H.B. Weinberg, in Hybrid Systems III, LNCS 1066, pages 496-510. (Papers from DIMACS Workshop on Verification and Control of Hybrid Systems, October, 1995). Revisited and extended in [LSV01] and [LSV03].

  • [Seg95a] A Compositional Trace-Based Semantics for Probabilistic Automata , R. Segala, in Proceedings of the 6th International Conference on Concurrency Theory (CONCUR '95), Philadelphia, PA, USA, LNCS 962, pages 234-248, August 1995.

  • [PS95] Formal Verification of Timed Properties for Randomized Distributed Algorithms, A. Pogosyants, R. Segala, in Proceedings of the 14th Annual ACM Symposium on Principles of Distributed Computing (PODC), Ottawa. Ontario, Canada, pages 174-183, August 1995.

  • [GSSL94] Liveness in Timed and Untimed Systems, R. Segala, R. Gawlick, J.F. Sogaard-Andersen, N. Lynch, in Proceedings of the 21st International Colloquium on Automata, Languages and Programming (ICALP), Jerusalem, Israel, LNCS 820, pages 166-177, 1994. Extended in [GSSL98]. More material available in MIT Technical Report MIT/LCS/TR-587.

  • [SL94] Probabilistic Simulations for Probabilistic Processes, R. Segala, N. Lynch, in Proceedings of the 5th International Conference on Concurrency Theory (CONCUR '94), Uppsala, Sweden, LNCS 836, pages 481-496, August 1994. Extended in [SL95].

  • [LSS94] Proving Time Bounds for Randomized Distributed Algorithms, N. Lynch, I. Saias, R. Segala, in Proceedings of the 13th Annual ACM Symposium on Principles of Distributed Computing (PODC), Los Angeles, CA, pages 314-323, August 1994.

  • [Seg93] Quiescence, Fairness, Testing and the notion of Implementation, R. Segala, in Proceedings of the 4th International Conference on Concurrency Theory (CONCUR '93), Hildesheim, Germany, LNCS 715, pages 324-338, August 1993. Extended in [Seg97].

  • [LS93] A Comparison of Simulation Techniques and Algebraic Techniques for Verifying Concurrent Systems, N. Lynch, R. Segala, in Proceedings of the Second North American Process Algebra Workshop, Cornell University, NY, 1993. Extended in [LS95].

Others

  • [CCK+05] Using Task-Structured Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol. R. Canetti, L. Cheung, D. Kaynar, M. Liskov, N. Lynch, O. Pereira, R. Segala, ePrint Report 2005/452.

  • [Seg95] Modeling and Verification of Randomized Distributed Real-Time Systems, R. Segala , PhD thesis, Laboratory for Computer Science, Massachusetts Institute of Technology, June 1995. Available as Technical Report MIT/LCS/TR-676.

  • [Seg92] A Process Algebraic View of I/O Automata, R. Segala, Master Thesis, available as MIT technical report number MIT/LCS/TR-557, 1992.
homepage