The power of simulation relations

ABSTRACT

We illustrate the role of simulation relations in the process of verification of large concurrent and distributed systems, showing in particular how simulation relations can be used successfully for the analysis of security protocols.

REFERENCES

• 1: Ran Canetti , Ling Cheung , Dilsun Kaynar , Moses Liskov , Nancy Lynch , Olivier Pereira , Roberto Segala, Analyzing Security Protocols Using Time-Bounded Task-PIOAs, Discrete Event Dynamic Systems, v.18 n.1, p.111-159, March 2008 [doi>10.1007/s10626-007-0032-1]
• 2: Bengt Jonsson, Simulations Between Specifications of Distributed Systems, Proceedings of the 2nd International Conference on Concurrency Theory, p.346-360, August 26-29, 1991
• 3: Dilsun K. Kaynar , Nancy Lynch , Roberto Segala , Frits Vaandrager, The Theory of Timed I/O Automata (Synthesis Lectures in Computer Science), Morgan & Claypool Publishers, 2006
• 4: Leslie Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.872-923, May 1994 [doi>10.1145/177492.177726]
• 5: Nancy Lynch , Roberto Segala , Frits Vaandrager, Hybrid I/O automata, Information and Computation, v.185 n.1, p.105-157, August 25, 2003 [doi>10.1016/S0890-5401(03)00067-1]
• 6: Nancy A. Lynch , Mark R. Tuttle, Hierarchical correctness proofs for distributed algorithms, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.137-151, August 10-12, 1987, Vancouver, British Columbia, Canada [doi>10.1145/41840.41852]
• 7: Nancy Lynch , Frits Vaandrager, Forward and backward simulations I.: untimed systems, Information and Computation, v.121 n.2, p.214-233, Sept. 1995 [doi>10.1006/inco.1995.1134]
• 8: Nancy Lynch , Roberto Segala , Frits Vaandrager, Observing Branching Structure through Probabilistic Contexts, SIAM Journal on Computing, v.37 n.4, p.977-1013, September 2007 [doi>10.1147/S0097539704446487]
• 9: R. Milner, Communication and Concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 10: Roberto Segala, Modeling and verification of randomized distributed real-time systems, Massachusetts Institute of Technology, Cambridge, MA, 1996
• 11: Roberto Segala , Andrea Turrini, Approximated Computationally Bounded Simulation Relations for Probabilistic Automata, Proceedings of the 20th IEEE Computer Security Foundations Symposium, p.140-156, July 06-08, 2007 [doi>10.1109/CSF.2007.8]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)

General Terms:
Theory, Verification

Keywords:
automata, simulation relations