Skip to main content
SpringerLink
Log in

Composition of Temporal Logic Specifications

  • Conference paper
Applications and Theory of Petri Nets 2004 (ICATPN 2004)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 3099))

Included in the following conference series:

  • 672 Accesses

Abstract

The Temporal Logic of Distributed Actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. TLDA supports a modular design of systems: Subsystems can be specified and verified separately and then be integrated into one system. The properties of the subsystems will be preserved in this process. TLDA can be syntactically viewed as an extension of TLA. We propose a different semantical model based on partial order which increases the expressiveness of the logic.

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

Access this chapter

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M.: An axiomatization of Lamport’s Temporal Logic of Actions. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 57–69. Springer, Heidelberg (1990)

    Google Scholar 

  2. Abadi, M., Lamport, L.: Composing specifications. ACM Transactions on Programming Languages and Systems 15(1), 73–132 (1993)

    Article  Google Scholar 

  3. Abadi, M., Lamport, L.: Decomposing specifications of concurrent systems. In: Olderog, E.-R. (ed.) Proc. of the Working Conference on Programming Concepts, Methods and Calculi (PROCOMET 1994). IFIP Transactions, vol. A-56, pp. 327–340. North-Holland, Amsterdam (1994)

    Google Scholar 

  4. Abadi, M., Lamport, L.: Conjoining specifications. ACM Transactions on Programming Languages and Systems 17(3), 507–534 (1995)

    Article  Google Scholar 

  5. Abadi, M., Merz, S.: On TLA as a logic. In: Broy, M. (ed.) Deductive Program Design. NATO ASI series F. Springer, Heidelberg (1996)

    Google Scholar 

  6. Abadi, M., Plotkin, G.D.: A logical view of composition and refinement. In: Proc. of the 18th Ann. ACM Symposium on Principles of Programming Languages, pp. 323–332 (1991)

    Google Scholar 

  7. Abadi, M., Plotkin, G.D.: A logical view of composition. Theoretical Computer Science 114(1), 3–30 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  8. Alexander, A., Reisig, W.: Logic of involved variables - system specification with Temporal Logic of Distributed Actions. In: Proc. of the 3rd International Conference on Aplication of Concurrency to System Design (ACSD 2003), Guimaraes, Portugal, pp. 167–176 (2003)

    Google Scholar 

  9. Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters 21(4), 181–185 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  10. Best, E., Fernandez, C.: Nonsequential processes – a Petri net view. In: Brauer, W., Rozenberg, G., Salomaa, A. (eds.) EATCS Monographs on Theoretical Computer Science, vol. 13. Springer, Heidelberg (1988)

    Google Scholar 

  11. Gomm, D., Kindler, E., Paech, B., Walter, R.: Compositional liveness properties of EN-systems. In: Ajmone Marsan, M. (ed.) ICATPN 1993. LNCS, vol. 691, pp. 262–281. Springer, Heidelberg (1993)

    Google Scholar 

  12. Huth, M., Ryan, M.: Logic in Computer Science: Modelling and reasoning about systems. Cambridge University Press, Cambridge (2000)

    MATH  Google Scholar 

  13. Kindler, E.: A compositional partial order semantics for Petri net components. In: Azéma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 235–252. Springer, Heidelberg (1997)

    Google Scholar 

  14. Kindler, E., Walter, R.: Message passing mutex. In: Desel, J. (ed.) Structures in Concurrency Theory, Workshops in Computing, May 1995, pp. 205–219. Springer, Heidelberg (1995)

    Google Scholar 

  15. Lamport, L.: Sometime is sometimes not never. In: Proc. of the 7th ACM Symposium on Principles of Programming Languages, January 1980, pp. 174–185 (1980)

    Google Scholar 

  16. Lamport, L.: The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems 16(3), 872–923 (1994)

    Article  Google Scholar 

  17. Lamport, L.: Composition: A way to make proofs harder. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 402–423. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  18. Manna, Z., Pnueli, A.: The temporal logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992)

    Google Scholar 

  19. Pnueli, A.: The temporal semantics of concurrent programs. Theoretical Computer Science 13(1), 45–61 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  20. Reisig, W.: Interleaved progress concurrent progress and local progress. In: Peled, D.A., Pratt, V.R., Holzmann, G.J. (eds.) Partial Order Methods in Verification. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 29, pp. 99–115. AMS, Providence (1997)

    Google Scholar 

  21. Reisig, W.: Elements of Distributed Algorithms: Modeling and Analysis with Petri Nets. Springer, Heidelberg (1998)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Humboldt-Universität zu Berlin, Unter den Linden 6, 10099, Berlin, Germany

    Adrianna Alexander

Authors
  1. Adrianna Alexander
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Universitat Politècnica de Catalunya, Spain

    Jordi Cortadella

  2. Institut für Informatik, Humboldt-Universität zu Berlin, Unter den Linden 6, 10099, Berlin, Germany

    Wolfgang Reisig

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Alexander, A. (2004). Composition of Temporal Logic Specifications. In: Cortadella, J., Reisig, W. (eds) Applications and Theory of Petri Nets 2004. ICATPN 2004. Lecture Notes in Computer Science, vol 3099. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27793-4_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-27793-4_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-22236-1

  • Online ISBN: 978-3-540-27793-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation