Skip to main content
SpringerLink
Log in
Book cover

ModelAge Workshop on Formal Models of Agents

ModelAge 1997: Formal Models of Agents pp 123–142Cite as

Towards a Proof-Theoretic Foundation for Actor Specification and Verification

  • Conference paper
  • First Online:

  • 168 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1760))

Abstract

Actors has been regarded as a promising model for open distributed systems. Although the operational semantics of actor programs has already been studied in some recent work, means of reasoning about the behaviour of communities of interconnected actors at a high abstraction level are still lacking. In this paper we argue that a proof-theoretic semantics would be better suited to this purpose. We present an abstract data type like axiomatisation of the kernel primitives of Actors, showing how to reason from specifications of actor communities and how to compose them within the framework of temporal logics of objects.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Gul Agha. Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, 1986.

    Google Scholar 

  2. Gul Agha, Ian A. Mason, Scott Smith, and Carolyn Talcott. A foundation for actor computation. Journal of Functional Programming, 7(1), 1997.

    Google Scholar 

  3. Pierre America and Frank de Boer. A proof system for process creation. In Manfred Broy and Cliff B. Jones, editors, Programming Concepts and Methods, pages 303–332. North Holland, 1990.

    Google Scholar 

  4. Nuno Barreiro, José Fiadeiro, and Tom Maibaum. Politeness in object societies. In Roel Wieringa and Remco Feenstra, editors, Proc. Information Systems: Correctness and Reusability, pages 119–134. World Scientific, 1995.

    Google Scholar 

  5. Carlos H. C. Duarte. Acidity yields another notion for modularity in formal object-oriented specifications (Extended Abstract). In Max Mühlhäuser, editor, Special Issues in Object-Oriented Programming. Dpunkt Verlag, 1996. Workshop Reader of the 10th European Conference on Object-Oriented Programming (ECOOP’96), Linz, Austria.

    Google Scholar 

  6. Hans-Dieter Ehrich, Amilcar Sernadas, and Cristina Sernadas. Objects, object types and object identity. In Hartmut Ehrig, editor, Categorical Methods in Computer Science with Aspects from Topology, volume 334 of Lecture Notes in Computer Science. Springer Verlag, 1988.

    Google Scholar 

  7. Hartmut Ehrig and Bernd Mahr. Fudamentals of Algebraic Specification 1: Equations and Initial Semantics. Springer Verlag, 1985.

    Google Scholar 

  8. E. Allen Emerson. Temporal and modal logic. In J. Van Leeuwen, editor, Hand book of Theoretical Computer Science, pages 996–1072. North Holland, 1990.

    Google Scholar 

  9. José Fiadeiro and Tom Maibaum. Towards object calculi. Technical report, De partment of Computing, Imperial College, London, 1990.

    Google Scholar 

  10. José Fiadeiro and Tom Maibaum. Temporal theories as modularisation units for concurrent systems specification. Formal Aspects of Computing, 4(3):239–272, 1992.

    Article  MATH  Google Scholar 

  11. Joseph A. Goguen and Rod M. Burstall. Institutions: Abstract model theory for specification and programming. Journal of the ACM, 39(1):95–146, January 1992.

    Article  MATH  MathSciNet  Google Scholar 

  12. Carl Hewitt and Henry Baker. Laws for communicating parallel processes. In IFIP Congress, pages 987–992, August 1977.

    Google Scholar 

  13. Bengt Jonsson. Compositional specification and verification of distributed systems. ACM Transactions on Programming Languages and Systems, 16(2):259–303, March 1994.

    Article  MathSciNet  Google Scholar 

  14. Leslie Lamport. What good is temporal logic? In R. E. A. Mason, editor, Proc. Information Processing 83: IFIP 9th World Congress, pages 657–668. North Holland, September 1983.

    Google Scholar 

  15. Tom Maibaum and Wladyslaw Tursky. On what exactly is going on when software is developed step-by-step. In Proc. 7th International Conference on Software Engineering (ICSE’84), pages 525–533. IEEE Computer Society Press, March 1984.

    Google Scholar 

  16. Michel Raynal and Masaaki Mizzymo. How to find his way in this jungle of consistency criteria for distributed shared memories. In Proc. 4th Workshop on Future Trends of Distributed Computing Systems, pages 340–346. IEEE Computer Society Press, September 1993.

    Google Scholar 

  17. Amílcar Sernadas, Cristina Sernadas, and Jose Felix Costa. Object specification logic. Journal of Logic and Computation, 5(5):603–630, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  18. A. Prashad Sistla, Emerson M. Clarke, Nissim Francez, and Albert R. Meyer. Can message buffers be axiomatized in linear temporal logic? Lnformation and Computation, 63:88–112, 1984.

    MATH  MathSciNet  Google Scholar 

  19. Carolyn Talcott. Interaction semantics for components of distributed systems. In Elie Najm and Jean-Bernard Stefani, editors, Proc. 1st IFIP Workshop on Formal Methods for Open Object-Based Distributed Systems (FMOODS’96). Chapman and Hall, 1996.

    Google Scholar 

  20. Roel Wieringa, Wiebren de Jonge, and Paul Spruit. Roles and dynamic subclasses: a modal logic approach. In Mario Tokoro and Remo Pareschi, editors, Proc. Object Oriented Programming, 8th European Conference (ECOOP’94), volume 821 of Lecture Notes in Computer Science, pages 32–59, 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing, Imperial College, 180 Queen’s Gate, London, SW7 2BZ, UK

    Carlos H. C. Duarte

Authors
  1. Carlos H. C. Duarte
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Utrecht University, Padualaan 14, De Uithof, 3508 TB, Utrecht, The Netherlands

    John-Jules Ch. Meyer

  2. Institut d’Informatique, Rue Grandgagnage 21, 5000, Namur, Belgium

    Pierre-Yves Schobbens

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Duarte, C.H.C. (1999). Towards a Proof-Theoretic Foundation for Actor Specification and Verification. In: Meyer, JJ.C., Schobbens, PY. (eds) Formal Models of Agents. ModelAge 1997. Lecture Notes in Computer Science(), vol 1760. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46581-2_9

Download citation

  • DOI: https://doi.org/10.1007/3-540-46581-2_9

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67027-8

  • Online ISBN: 978-3-540-46581-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation