Skip to main content
SpringerLink
Log in

A General Tableau Technique for Verifying Temporal Properties of Concurrent Programs

Extended Abstract

  • Conference paper
Book cover Semantics for Concurrency

Part of the book series: Workshops in Computing ((WORKSHOPS COMP.))

Abstract

Labelled transition systems provide convenient models for many computational systems. Their usefulness is due partly to their natural association with temporal logics which may be used to express interesting properties of systems. It is of course vital to be able not only to express properties of programs but also to determine whether they hold of them. In the case of finite-state systems, much work has been done on automatic model checking [4]. Algorithms are known for a variety of logics, and many have been implemented and used to study systems including communications protocols and digital circuits.

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 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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. H. Barringer, R. Kuiper and A. Pnueli, Now You May Compose Temporal Logic Specifications, in Proc. 16th Symp. Theory of Comp. ACM Press, 1984.

    Google Scholar 

  2. J. Bradfield, Proving Temporal Properties of Petri Nets, to appear in Proc. of 11th International Conference on Applications and Theory of Petri Nets, Paris, June 1990.

    Google Scholar 

  3. J. Bradfield and C. Stirling, Verifying Temporal Properties of Procesees, submitted for publication.

    Google Scholar 

  4. E. Clarke, E. Emerson and A. Sistla Automatic Verification of Finite-State Systems Using Temporal Logic Specifications: a Practical Approachin Proc. 10th Annual ACM Symp. in Principles of Programming Languages, 1983.

    Google Scholar 

  5. E. Clarke and O. Grumberg The Model Checking Problem for Concurrent Systems With Many Simple Processesin Procs. Temporal Logic in Specification, eds. B. Banieqbal, H. Barringer and A. Pnueli, Springer LNCS 398, 1989.

    Google Scholar 

  6. E. Emerson and C.-L. Lei Efficient Model Checking in Fragments of the Propositional Mu-Calculusin Proc. 1st IEEE Symp. on Logic in Computer Science, 1986.

    Google Scholar 

  7. E. Emerson and J. Srinivasan, Branching Time Temporal Logic, in Proc. Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, eds. J. de Bakker, W.-P. de Roever and G. Rozenberg, Springer LNCS 354, 198Q.

    Google Scholar 

  8. D. Knuth, Additional Comments on a Problem in Concurrent Program Control, Comm. ACM, 9/5 1966.

    Google Scholar 

  9. D. Kozen, Results on the Propositional p-calculus, Theoretical Computer Science, 27 1983.

    Google Scholar 

  10. K. Larsen, Proof Systems for Hennessy-Milner Logic with Recursion,to appear in Information and Computation.

    Google Scholar 

  11. Z. Manna and A. Pnueli, The Anchored Version of the Temporal Framework, in Proc. Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, eds. J. de Bakker, W.-P. de Roever and G. Rozenberg, Springer LNCS 354, 1989.

    Google Scholar 

  12. M. Pease, R. Shostak and L. Lamport, Reaching Agreement in the Presence of Faults, Journal ACM, 27 1980.

    Google Scholar 

  13. G. Plotkin, A Structural Approach to Operational Semantics, Technical Report DAIMI FN-19, University of Aarhus 1981.

    Google Scholar 

  14. V. Pratt, A Decidable Mu-Calculus, in Proc. 22nd IEEE Foundations of Computer Science, 1981.

    Google Scholar 

  15. C. Stirling, A Generalization of Owicki-Gries’s Hoare Logic for a Concurrent While Language, Theoretical Computer Science 58 (1988).

    Google Scholar 

  16. C. Stirling, Modal and Temporal Logics, chapter to appear in Handbook of Logic in Computer Science, OUP 1990.

    Google Scholar 

  17. C. Stirling and D. Walker, Local Model Checking in the Modal Mu-Calculus, in Proc. Intl. Joint Conf. on Theory and Practice of Software Development, eds. J. Diaz and F. Orejas, Springer LNCS 351, 1989.

    Google Scholar 

  18. D. Walker, Automated Analysis of Mutual Exclusion Algorithms Using CCS, Formal Aspects of Computing (1989) 1.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Edinburgh, Edinburgh, EH9 3JZ, UK

    Colin Stirling & David Walker

Authors
  1. Colin Stirling
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David Walker
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 1990 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Stirling, C., Walker, D. (1990). A General Tableau Technique for Verifying Temporal Properties of Concurrent Programs. In: Semantics for Concurrency. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3860-0_1

Download citation

  • DOI: https://doi.org/10.1007/978-1-4471-3860-0_1

  • Publisher Name: Springer, London

  • Print ISBN: 978-3-540-19625-9

  • Online ISBN: 978-1-4471-3860-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation