Advertisement

A Rewriting Logic Sampler

  • José Meseguer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3722)

Abstract

Rewriting logic is a simple computational logic very well suited as a semantic framework within which many different models of computation, systems and languages can be naturally modeled. It is also a flexible logical framework in which many different logical formalisms can be both represented and executed. As the title suggests, this paper does not try to give a comprehensive overview of rewriting logic. Instead, after introducing the basic concepts, it focuses on some recent research directions emphasizing: (i) extensions of the logic to model real-time systems and probabilistic systems; and (ii) some exciting application areas such as: semantics of programming languages, security, and bioinformatics.

Keywords

Inference Rule Semantic Framework Linear Time Temporal Logic Statistical Model Check Proof Term 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Agha, G., Gunter, C., Greenwald, M., Khanna, S., Meseguer, J., Sen, K., Thati, P.: Formal modeling and analysis of DoS using probabilistic rewrite theories. In: Workshop on Foundations of Computer Security (FCS 2005) (Affiliated with LICS 2005) (2005)Google Scholar
  2. 2.
    Agha, G., Meseguer, J., Sen, K.: PMaude: Rewrite-based specification language for probabilistic object systems. In: 3rd Workshop on Quantitative Aspects of Programming Languages, QAPL 2005 (2005)Google Scholar
  3. 3.
    Ahrendt, W., Roth, A., Sasse, R.: Automatic validation of transformation rules for Java verification against a rewriting semantics (June 2005) (manuscript)Google Scholar
  4. 4.
    Basin, D., Clavel, M., Meseguer, J.: Reflective metalogical frameworks. ACM Transactions on Computational Logic (2004)Google Scholar
  5. 5.
    Basin, D., Clavel, M., Meseguer, J.: Rewriting logic as a metalogical framework. In: Kapoor, S., Prasad, S. (eds.) FST TCS 2000. LNCS, vol. 1974, pp. 55–80. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  6. 6.
    Basin, D., Denker, G.: Maude versus Haskell: An experimental comparison in security protocol analysis. In: Futatsugi, K. (ed.) [52], pp. 235–256, http://www.elsevier.nl/locate/entcs/volume36.html
  7. 7.
    Borovanský, P., Kirchner, C., Kirchner, H., Moreau, P.-E.: ELAN from a rewriting logic point of view. Theoretical Computer Science 285, 155–185 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Braga, C.: Rewriting Logic as a Semantic Framework for Modular Structural Operational Semantics. PhD thesis, Departamento de Informática, Pontificia Universidade Católica de Rio de Janeiro, Brasil (2001)Google Scholar
  9. 9.
    Braga, C., Meseguer, J.: Modular rewriting semantics in practice. In: Proc. WRLA 2004. ENTCS (2004)Google Scholar
  10. 10.
    Bruni, R., Meseguer, J.: Generalized rewrite theories. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 252–266. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  11. 11.
    Cervesato, I., Stehr, M.-O.: Representing the msr cryptoprotocol specification language in an extension of rewriting logic with dependent types. In: Degano, P. (ed.) Proc. Fifth International Workshop on Rewriting Logic and its Applications (WRLA 2004), Barcelona, Spain, March 27 - 28. Elsevier ENTCS (2004)Google Scholar
  12. 12.
    Chalub, F.: An implementation of modular SOS in maude. Master’s thesis, Universidade Federal Fluminense (May 2005), http://www.ic.uff.br/~frosario/dissertation.pdf
  13. 13.
    Chalub, F., Braga, C.: A Modular Rewriting Semantics for CML. Journal of Universal Computer Science 10(7), 789–807 (2004), http://www.jucs.org/jucs_10_7/a_modular_rewriting_semantics MathSciNetGoogle Scholar
  14. 14.
    Chen, F., Roşu, G., Venkatesan, R.P.: Rule-based analysis of dimensional safety. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 197–207. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  15. 15.
    Clavel, M.: Reflection in Rewriting Logic: Metalogical Foundations and Metaprogramming Applications. CSLI Publications, Stanford (2000)zbMATHGoogle Scholar
  16. 16.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J.: Metalevel computation in Maude. In: Kirchner, C., Kirchner, H. (eds.) [60], pp. 3–24, http://www.elsevier.nl/locate/entcs/volume15.html
  17. 17.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.: Maude: specification and programming in rewriting logic. Theoretical Computer Science 285, 187–243 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: Maude 2.0 Manual (June 2003), http://maude.cs.uiuc.edu
  19. 19.
    Clavel, M., Durán, F., Eker, S., Meseguer, J.: Building equational proving tools by reflection in rewriting logic. In: CAFE: An Industrial-Strength Algebraic Formal Method, pp. 1–31. Elsevier, Amsterdam (2000), http://maude.cs.uiuc.edu CrossRefGoogle Scholar
  20. 20.
    Clavel, M., Durán, F., Eker, S., Meseguer, J., Stehr, M.-O.: Maude as a formal meta-tool. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, pp. 1684–1703. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  21. 21.
    Clavel, M., Durán, F., Martí-Oliet, N.: Polytypic programming in Maude. In: Futatsugi, K. (ed.) [52], pp. 339–360, http://www.elsevier.nl/locate/entcs/volume36.html
  22. 22.
    Clavel, M., Meseguer, J.: Reflection and strategies in rewriting logic. In: Meseguer, J. (ed.) Proceedings First International Workshop on Rewriting Logic and its Applications, WRLA 1996, Asilomar, California, September 3–6. Electronic Notes in Theoretical Computer Science, vol. 4, pp. 125–147. Elsevier, Amsterdam (1996), http://www.elsevier.nl/locate/entcs/volume4.html Google Scholar
  23. 23.
    Clavel, M., Meseguer, J.: Reflection in conditional rewriting logic. Theoretical Computer Science 285, 245–288 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  24. 24.
    Clavel, M., Meseguer, J., Palomino, M.: Reflection in membership equational logic, many-sorted equational logic, horn logic with equality, and rewriting logic. In: Gadducci, F., Montanari, U. (eds.) Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2002)Google Scholar
  25. 25.
    Clavel, M., Palomino, M.: The ITP tool’s manual. Universidad Complutense, Madrid (April 2005), http://maude.sip.ucm.es/itp/
  26. 26.
    Clavel, M., Santa-Cruz, J.: ASIP+ITP: A verification tool based on algebraic semantics. To appear in Proc. PROLE 2005 (2005), http://maude.sip.ucm.es/~clavel/pubs/
  27. 27.
    d’Amorim, M., Roşu, G.: An Equational Specification for the Scheme Language. In: Proceedings of the 9th Brazilian Symposium on Programming Languages, SBLP 2005 (2005) (to appear), Also Technical Report No. UIUCDCS-R-2005-2567(April 2005)Google Scholar
  28. 28.
    Denker, G., Meseguer, J., Talcott, C.: Rewriting semantics of meta-objects and composable distributed services. In: Proc. 3rd. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2000)Google Scholar
  29. 29.
    Denker, G., Meseguer, J., Talcott, C.L.: Protocol specification and analysis in Maude. In: Heintze, N., Wing, J. (eds.) Proceedings of Workshop on Formal Methods and Security Protocols, Indianapolis, Indiana, June 25 (1998), http://www.cs.bell-labs.com/who/nch/fmsp/index.html
  30. 30.
    Denker, G., Meseguer, J., Talcott, C.L.: Formal specification and analysis of active networks and communication protocols: The Maude experience. In: Maughan, D., Koob, G., Saydjari, S. (eds.) Proceedings DARPA Information Survivability Conference and Exposition, DISCEX 2000, Hilton Head Island, South Carolina, January 25–27, pp. 251–265. IEEE Computer Society Press, Los Alamitos (2000), http://schafercorp-ballston.com/discex/ Google Scholar
  31. 31.
    Denker, G., Millen, J.: CAPSL and CIL language design: A common authentication protocol specification language and its intermediate language. Technical Report SRI-CSL-99-02, Computer Science Laboratory, SRI International (1999), http://www.csl.sri.com/~denker/pub_99.html
  32. 32.
    Denker, G., Millen, J.: CAPSL intermediate language. In: Heintze, N., Clarke, E. (eds.) Proceedings of Workshop on Formal Methods and Security Protocols, FMSP 1999, Trento, Italy (July 1999), http://www.cs.bell-labs.com/who/nch/fmsp99/program.html
  33. 33.
    Denker, G., Millen, J.: CAPSL integrated protocol environment. In: Maughan, D., Koob, G., Saydjari, S. (eds.) Proceedings DARPA Information Survivability Conference and Exposition, DISCEX 2000, Hilton Head Island, South Carolina, January 25-27, pp. 207–222. IEEE Computer Society Press, Los Alamitos (2000), http://schafercorp-ballston.com/discex/ Google Scholar
  34. 34.
    Denker, G., Millen, J.: The CAPSL integrated protocol environment. Technical Report SRI-CSL-2000-02, Computer Science Laboratory, SRI International (2000), http://www.csl.sri.com/~denker/pub_99.html
  35. 35.
    Durán, F.: A reflective module algebra with applications to the Maude language. Ph.D. Thesis, University of Málaga (1999)Google Scholar
  36. 36.
    Durán, F.: Coherence checker and completion tools for Maude specifications. Manuscript, Computer Science Laboratory, SRI International (2000), http://maude.cs.uiuc.edu/papers
  37. 37.
    Durán, F.: The extensibility of Maude’s module algebra. In: Rus, T. (ed.) AMAST 2000. LNCS, vol. 1816, pp. 422–437. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  38. 38.
    Durán, F.: Termination checker and Knuth-Bendix completion tools for Maude equational specifications. Manuscript, Computer Science Laboratory, SRI International (2000), http://maude.cs.uiuc.edu/papers
  39. 39.
    Durán, F., Lucas, S., Meseguer, J., Marché, C., Urbain, X.: Proving termination of membership equational programs. In: Sestoft, P., Heintze, N. (eds.) Proc. of ACM SIGPLAN 2004 Symposium on Partial Evaluation and Program Manipulation, PEPM 2004, pp. 147–158. ACM Press, New York (2004)CrossRefGoogle Scholar
  40. 40.
    Durán, F., Meseguer, J.: An extensible module algebra for Maude. In: Kirchner, Kirchner (eds.) [60], pp. 185–206., http://www.elsevier.nl/locate/entcs/volume15.html
  41. 41.
    Durán, F., Meseguer, J.: A Church-Rosser checker tool for Maude equational specifications. Manuscript, Computer Science Laboratory, SRI International (2000), http://maude.cs.uiuc.edu/papers
  42. 42.
    Durán, F., Meseguer, J.: On parameterized theories and views in Full Maude 2.0. In: Futatsugi, K. (ed.) Proc. 3rd. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2000)Google Scholar
  43. 43.
    Eker, S., Knapp, M., Laderoute, K., Lincoln, P., Meseguer, J., Sonmez, K.: Pathway logic: Symbolic analysis of biological signaling. In: Proceedings of the Pacific Symposium on Biocomputing, January 2002, pp. 400–412 (2002)Google Scholar
  44. 44.
    Eker, S., Knapp, M., Laderoute, K., Lincoln, P., Talcott, C.: Pathway Logic: executable models of biological networks. In: Gadducci, F., Montanari, U. (eds.) Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2002)Google Scholar
  45. 45.
    Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. In: Gadducci, F., Montanari, U. (eds.) Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2002)Google Scholar
  46. 46.
    Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker and its implementation. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 230–234. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  47. 47.
    Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL Protocol Analyzer (2005) (submitted for publication)Google Scholar
  48. 48.
    Escobar, S., Meseguer, J., Thati, P.: Natural narrowing for general term rewriting systems. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 279–293. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  49. 49.
    Farzan, A., Cheng, F., Meseguer, J., Roşu, G.: Formal analysis of Java programs in JavaFAN. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 501–505. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  50. 50.
    Farzan, A., Meseguer, J.: Partial order reduction for rewriting semantics of programming languages. Technical Report UIUCDCS-R-2005-2598, CS Dept., University of Illinois at Urbana-Champaign (June 2005)Google Scholar
  51. 51.
    Farzan, A., Meseguer, J., Roşu, G.: Formal JVM code analysis in JavaFAN. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 132–147. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  52. 52.
    Futatsugi, K. (ed.): Proceedings Third International Workshop on Rewriting Logic and its Applications, WRLA 2000, Kanazawa, Japan, September 18–20. Electronic Notes in Theoretical Computer Science, vol. 36. Elsevier, Amsterdam (2000), http://www.elsevier.nl/locate/entcs/volume36.html Google Scholar
  53. 53.
    Futatsugi, K., Diaconescu, R.: CafeOBJ Report. AMAST Series. World Scientific, Singapore (1998)zbMATHGoogle Scholar
  54. 54.
    Glynn, P.: The role of generalized semi-Markov processes in simulation output analysis (1983)Google Scholar
  55. 55.
    Gunter, C., Goodloe, A., Stehr, M.-O.: Formal prototyping in early stages of protocol design. In: Proceedings of the Workshop on Issues in the Theory of Security (WITS 2005), Long Beach, California, January 10-11 (2005), To appear in the ACM Digital Library. Paper available at http://formal.cs.uiuc.edu/stehr/l3a-wits.pdf
  56. 56.
    Gutierrez-Nolasco, S., Venkatasubramanian, N., Stehr, M.-O., Talcott, C.L.: Exploring adaptability of secure group communication using formal prototyping techniques. In: Proceedings of the 3rd Workshop on Reflective and Adaptive Middleware (RM 2004), Toronto, Ontario, Canada, October 19 (2004), To appear in ACM Digital Library. Extended version available at http://formal.cs.uiuc.edu/stehr/spread_eng.html
  57. 57.
    Hendrix, J., Meseguer, J., Clavel, M.: A sufficient completeness reasoning tool for partial specifications. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 165–174. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  58. 58.
    Holzmann, G.: The Spin Model Checker - Primer and Reference Manual. Addison-Wesley, Reading (2003)Google Scholar
  59. 59.
    Johnsen, E.B., Owe, O., Axelsen, E.W.: A runtime environment for concurrent objects with asynchronous method calls. In: Martí-Oliet, N. (ed.) Proc. 5th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2004)Google Scholar
  60. 60.
    Kirchner, C., Kirchner, H. (eds.): Proceedings Second International Workshop on Rewriting Logic and its Applications, WRLA 1998, Pont-à-Mousson, France, September 1–4. Electronic Notes in Theoretical Computer Science, vol. 15. Elsevier, Amsterdam (1998), http://www.elsevier.nl/locate/entcs/volume15.html Google Scholar
  61. 61.
    Kolch, W.: Meaningful relationships: the regulation of the Ras/Raf/MEK/ERK pathway by protein interactions. Biochem. J. 351, 289–305 (2000)CrossRefGoogle Scholar
  62. 62.
    Kosiuczenko, P., Wirsing, M.: Timed rewriting logic with application to object-oriented specification. Technical report, Institut für Informatik, Universität München (1995)Google Scholar
  63. 63.
    Kumar, N., Sen, K., Meseguer, J., Agha, G.: Probabilistic rewrite theories: Unifying models, logics and tools. Technical Report UIUCDCS-R-2003-2347, University of Illinois at Urbana-Champaign (May 2003)Google Scholar
  64. 64.
    Kumar, N., Sen, K., Meseguer, J., Agha, G.: A rewriting based model of probabilistic distributed object systems. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 32–46. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  65. 65.
    Lien, E.: Formal modeling and analysis of the NORM multicast protocol in Real-Time Maude. Master’s thesis, Dept. of Linguistics, University of Oslo (2004), http://wo.uio.no/as/WebObjects/theses.woa/wo/0.3.9
  66. 66.
    Martí-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd edn., pp. 1–87. Kluwer Academic Publishers, Dordrecht (2002); First published as SRI Tech. Report SRI-CSL-93-05 (August 1993)Google Scholar
  67. 67.
    Martí-Oliet, N., Meseguer, J.: Rewriting logic: roadmap and bibliography. Theoretical Computer Science 285, 121–154 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  68. 68.
    Meadows, C.: The NRL protocol analyzer: An overview. Journal of Logic Programming 26(2), 113–131 (1996)zbMATHCrossRefGoogle Scholar
  69. 69.
    Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  70. 70.
    Meseguer, J.: Rewriting logic as a semantic framework for concurrency: a progress report. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 331–372. Springer, Heidelberg (1996)Google Scholar
  71. 71.
    Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)Google Scholar
  72. 72.
    Meseguer, J.: Research directions in rewriting logic. In: Berger, U., Schwichtenberg, H. (eds.) Computational Logic, NATO Advanced Study Institute, Marktoberdorf, Germany, July 29 – August 6. Springer, Heidelberg (1999)Google Scholar
  73. 73.
    Meseguer, J.: Software specification and verification in rewriting logic. In: Broy, M., Pizka, M. (eds.) Models, Algebras, and Logic of Engineering Software, NATO Advanced Study Institute, Marktoberdorf, Germany, July 30 – August 11, pp. 133–193. IOS Press, Amsterdam (2003)Google Scholar
  74. 74.
    Meseguer, J.: Localized fairness: A rewriting semantics. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 250–263. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  75. 75.
    Meseguer, J., Braga, C.: Modular rewriting semantics of programming languages. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 364–378. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  76. 76.
    Meseguer, J., Roşu, G.: Rewriting logic semantics: From language specifications to formal analysis tools. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 1–44. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  77. 77.
    Meseguer, J., Roşu, G.: The rewriting logic semantics project. In: Proc. of SOS 2005. ENTCS, Elsevier, Amsterdam (2005) (to appear)Google Scholar
  78. 78.
    Meseguer, J., Talcott, C.: Semantic models for distributed object reflection. In: Magnusson, B. (ed.) ECOOP 2002. LNCS, vol. 2374, pp. 1–36. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  79. 79.
    Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to the verification of cryptographic protocols. In: Martí-Oliet, N. (ed.) Proc. 5th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2004)Google Scholar
  80. 80.
    Mosses, P.D.: Modular structural operational semantics. J. Log. Algebr. Program 60–61, 195–228 (2004)CrossRefMathSciNetGoogle Scholar
  81. 81.
    Ölveczky, P., Keaton, M., Meseguer, J., Talcott, C., Zabele, S.: Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol. 2029, p. 333. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  82. 82.
    Ölveczky, P., Meseguer, J.: Real-Time Maude 2.0. In: Proc. WRLA 2004. ENTCS (2004)Google Scholar
  83. 83.
    Ölveczky, P.C.: Specification and Analysis of Real-Time and Hybrid Systems in Rewriting Logic. PhD thesis, University of Bergen, Norway (2000), http://maude.csl.sri.com/papers
  84. 84.
    Ölveczky, P.C., Kosiuczenko, P., Wirsing, M.: An object-oriented algebraic steam-boiler control specification. In: Abrial, J.-R., Börger, E., Langmaack, H. (eds.) Dagstuhl Seminar 1995. LNCS, vol. 1165, pp. 379–402. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  85. 85.
    Ölveczky, P.C., Meseguer, J.: Specifying real-time systems in rewriting logic. In: Meseguer, J. (ed.) Proc. First Intl. Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science, vol. 4, Elsevier, Amsterdam (1996), http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm Google Scholar
  86. 86.
    Ölveczky, P.C., Meseguer, J.: Real-Time Maude: a tool for simulating and analyzing real-time and hybrid systems. In: Proc. 3rd. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2000)Google Scholar
  87. 87.
    Ölveczky, P.C., Meseguer, J.: Specification of real-time and hybrid systems in rewriting logic. Theoretical Computer Science 285, 359–405 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  88. 88.
    Palomino, M.: A predicate abstraction tool for maude. Documentation and tool, available at http://maude.sip.ucm.es/~miguelpt/bibliography.html
  89. 89.
    Parzen, E.: Modern Probability Theory and its Applications. Wiley, Chichester (1960)zbMATHGoogle Scholar
  90. 90.
    Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley and Sons, Chichester (1994)zbMATHGoogle Scholar
  91. 91.
    Roşu, G., Venkatesan, R.P., Whittle, J., Leustean, L.: Certifying optimality of state estimation programs. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 301–314. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  92. 92.
    Rodríguez, D.E.: Case studies in the specification and analysis of protocols in Maude. In: Futatsugi, K. (ed.) [52], pp. 257–275, http://www.elsevier.nl/locate/entcs/volume36.html
  93. 93.
    Sasse, R.: Taclets vs. rewriting logic – relating semantics of Java. Master’s thesis, Fakultät für Informatik, Universität Karlsruhe, Germany (May 2005), Technical Report in Computing Science No. 2005-16, http://www.ubka.uni-karlsruhe.de/cgi-bin/psview?document=ira/2005/16
  94. 94.
    Segala, R.: Modelling and Verification of Randomized Distributed Real Time Systems. PhD thesis, Massachusetts Institute of Technology (1995)Google Scholar
  95. 95.
    Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 266–280. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  96. 96.
    Steggles, L., Kosiuczenko, P.: A timed rewriting logic semantics for SDL: a case study of the alternating bit protocol. In: Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications. ENTCS, vol. 15. North Holland, Amsterdam (1998)Google Scholar
  97. 97.
    Stehr, M.-O., Cervesato, I., Reich, S.: An execution environment for the MSR cryptoprotocol specification language, http://formal.cs.uiuc.edu/stehr/msr.html
  98. 98.
    Stehr, M.-O., Talcott, C.: PLAN in Maude: Specifying an active network programming language. In: Gadducci, F., Montanari, U. (eds.) Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2002)Google Scholar
  99. 99.
    Stehr, M.-O., Talcott, C.L.: Practical techniques for language design and prototyping. In: Fiadeiro, J.L., Montanari, U., Wirsing, M. (eds.) Abstracts Collection of the Dagstuhl Seminar 05081 on Foundations of Global Computing, Schloss Dagstuhl, Wadern, Germany, February 20–25 (2005)Google Scholar
  100. 100.
    Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton (1994)Google Scholar
  101. 101.
    Talcott, C., Eker, S., Knapp, M., Lincoln, P., Laderoute, K.: Pathway logic modeling of protein functional domains in signal transduction. In: Proceedings of the Pacific Symposium on Biocomputing (January 2004)Google Scholar
  102. 102.
    Thati, P., Meseguer, J.: Complete symbolic reachability analysis using back-and-forth narrowing. In: Fiadeiro, J.L., Harman, N.A., Roggenbach, M., Rutten, J. (eds.) CALCO 2005. LNCS, vol. 3629, pp. 379–394. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  103. 103.
    Thati, P., Sen, K., Martí-Oliet, N.: An executable specification of asynchronous Pi-Calculus semantics and may testing in Maude 2.0. In: Gadducci, F., Montanari, U. (eds.) Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2002)Google Scholar
  104. 104.
    Thordvalsen, S.: Modeling and analysis of the OGDC wireless sensor network algorithm in Real-Time Maude. Master’s thesis, Dept. of Informatics, University of Oslo (2005), http://heim.ifi.uio.no/~peterol/RealTimeMaude/OGDC/
  105. 105.
    Verdejo, A.: Maude como marco semántico ejecutable. PhD thesis, Facultad de Informática, Universidad Complutense, Madrid, Spain (2003)Google Scholar
  106. 106.
    Verdejo, A., Martí-Oliet, N.: Executable structural operational semantics in Maude. Manuscript, Dto. Sistemas Informáticos y Programación, Universidad Complutense, Madrid (August. 2003)Google Scholar
  107. 107.
    Verdejo, A., Martí-Oliet, N.: Implementing CCS in Maude. In: Proc. FORTE/PSTV 2000. IFIP, vol. 183, pp. 351–366 (2000)Google Scholar
  108. 108.
    Verdejo, A., Martí-Oliet, N.: Implementing CCS in Maude 2. In: Gadducci, F., Montanari, U. (eds.) Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2002)Google Scholar
  109. 109.
    Viry, P.: Equational rules for rewriting logic. Theoretical Computer Science 285, 487–517 (2002)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • José Meseguer
    • 1
  1. 1.University of Illinois at Urbana-ChampaignUSA

Personalised recommendations