Abstract
We here present an approach to reasoning about actor programs on the basis of temporal logic. Temporal logic is particularly appropriate for the specification of concurrent programs, but most known temporal logic proof systems for concurrent computations rely on imperative language constructs, ignoring, e.g., the creation of processes and the dynamic configuration of communication channels, which are crucial for actor based programming. We will demonstrate our approach by applying it to a detection algorithm for termination of parts of a computation.
This work has been done as a part of my dissertation at the Computational Linguistics Lab, Freiburg University, Germany. Thanks to all of the colleagues and especially to Prof. Hahn!
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Agha, G. Actors: a Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge, MA, 1986.
Agha, G. The structure and semantics of actor languages. In Foundations of Object-Oriented Languages, J. de Bakker, W.-P. de Roever, and G. Rozenberg, Eds., no. 489 in LNCS. Springer, Berlin etc., 1990, pp. 1–59.
Agha, G., Frølund, S., Kim, W. Y., Panwar, R., Patterson, A., and Sturman, D. Abstraction and modularity mechanisms for concurrent computing. In Research Directions in Concurrent Object-Oriented Programming, G. Agha, P. Wegner, and A. Yonezawa, Eds. MIT Press, Cambridge, MA, 1993, pp. 3–21.
Agha, G., Mason, I. A., Smith, S. F., and Talcott, C. L. A foundation for actor computation. Journal of Functional Programming 7 (1997), 1–72.
Barringer, H. The use of temporal logic in the compositional specification of concurrent systems. In Temporal Logics and their Applications, A. Galton, Ed. Academic Press, London etc., 1987, pp. 53–90.
Chandy, K. M., and Misra, J. Parallel Program Design. Addison-Wesley, 1989.
Clarke, E. M., Emerson, E. A., and Sistla, A. P. Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. ACM Transactions on Programming Languages and Systems 8, 2 (April 1986), 244–263.
Clinger, W. D. Foundations of Actor Semantics. PhD thesis, Cambridge, MA: MIT, Dept. of Mathematics, 1981.
Duarte, C. H. C. A proof-theoretic approach to the design of object-based mobility. In Proc. 2nd IFIP Conf. on Formal Methods for Open Object-Based Distributed Systems (London, 1997), H. Bowman and J. Derrick, Eds., Chapman and Hall, pp. 37–56.
Emerson, E., and Halpern, J. ’sometimes’ and ‘not never’ revisited: On branching time versus linear time temporal logic. Journal of the ACM 33, 1 (1986).
Felleisen, M., and Friedman, D. P. Control operators, the SECD-machine, and the ë-calculus. In Formal Descriptions of Programming Concepts III, M. Wirsing, Ed. Elsevier, Amsterdam, NL, 1986, pp. 193–217.
Frølund, S. Inheritance of synchronization constraints in concurrent object oriented programming languages. In ECOOP’92-European Conference on Object-Oriented Programming (1992), O. L. Madsen, Ed., no. 615 in LNCS, Springer, pp. 185–196.
Greif, I. G. Semantics of Communicating Parallel Processes. PhD thesis, MIT, Dept. of Electrical Engineering and Computer Science, 1975.
Hewitt, C., and Baker, H. Actors and continuous functionals. In Proceedings of the IFIPWorking Conference on Formal Description of Programming Concepts (1978), E. Neuhold, Ed., Amsterdam etc.: North-Holland, pp. 367–390.
Hoare, C. Communicating Sequential Processes. Prentice-Hall, 1985.
Kröger, F. Temporal Logic of Programs. Springer, 1987.
Lamport, L. The Temporal Logic of Actions. Transactions on Programming Languages and Systems 16, 3 (May 1994), 872–923.
Manna, Z., and Pnueli, A. The Temporal Logic of Reactive and Concurrent Systems. Springer, Berlin etc., 1992.
Milner, R. Communication and Concurrency. Prentice-Hall, Englewood Cliffs, NJ, 1989.
Milner, R., Parrow, J., and Walker, D. A calculus of mobile processes, I/II. Information and Computation 100, 1 (1992), 1–77.
Nierstrasz, O. Towards an object calculus. In ECOOP’91-Proceedings of the European Workshop on Object-Based Concurrent Computing (Berlin etc., Geneva, Switzerland, July 15–16 1992), M. Tokoro, O. Nierstrasz, P. Wegner, and A. Yonezawa, Eds., Springer.
Owicki, S., and Lamport, L. Proving liveness properties of concurrent programs. ACM Transactions on Programming Languages and Systems 4, 3 (1982), 455–495.
Plotkin, G. Call-by-name, call-by-value and the lambda calculus. Theoretical Computer Science 1 (1975), 125–159.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Schacht, S. (2001). Formal Reasoning about Actor Programs Using Temporal Logic. In: Agha, G.A., De Cindio, F., Rozenberg, G. (eds) Concurrent Object-Oriented Programming and Petri Nets. Lecture Notes in Computer Science, vol 2001. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45397-0_18
Download citation
DOI: https://doi.org/10.1007/3-540-45397-0_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41942-6
Online ISBN: 978-3-540-45397-0
eBook Packages: Springer Book Archive