Advertisement

Regular automata and model checking

  • Z. Habasiński
Parallelism And Concurrency
  • 110 Downloads
Part of the Lecture Notes in Computer Science book series (LNCS, volume 299)

Abstract

We present a class of the temporal branching time logics designated for the specification of concurrent programs and incorporating all regular temporal operators. A linear time model checking procedure is given due to which an efficient verification of the temporal dependencies in programs is possible.

Keywords

Model Check Concurrent Program Computation Tree Logic Linear Time Temporal Logic Model Check Problem 
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. AC86.
    Arnold A. Crubille P. A linear algorithm to solve fixed-point equations on graphs, Rep. I-8632, Univ. de Bordeaux I.Google Scholar
  2. Bro86.
    Browne M.C. An improved algorithm for the automatic verification of finite state systems using temporal logic, Rep. CMU-CS-86-156, Carnegie-Mellon Univ.Google Scholar
  3. CE81.
    Clarke E.M. Emerson E.A. Design and synthesis of synchronization skeletons using branching time temporal logic, LNCS 131,:52–71.Google Scholar
  4. CES83.
    Clarke E.M. Emerson E.A. Sistla A.P. Automatic verification of finite state concurrent systems using temporal logic specifications, POPL-Symp.,:117–126; see also ACM Tran. on Prog. Lang. and Systems 8(2):244–263, 1986.Google Scholar
  5. CGK87.
    Clarke E.M., Grumberg O., Kurshan R.P. A synthesis of two approaches for verifying finite state concurrent systems, Report of the Carnegie Mellon Univ., 1987.Google Scholar
  6. EC82.
    Emerson E.A. Clarke M. Using branching time temporal logic to synthesize synchronization skeletons, Sci. of Comp. Programming 2,:241–266.Google Scholar
  7. EL85a.
    Emerson E.A. Lei Ch-L. Modalities for model checking: branching time strickes back, POPL-Symp.,:84–96.Google Scholar
  8. EL85b.
    Emerson E.A. Lei Ch-L. Temporal model checking under generalized fairness constraints, Hawaii Int. Conf. System Sci.,1985.Google Scholar
  9. Flo67.
    Floyd R.W. Assigning meaning to programs, Proc. of Symp. in Applied Math.XIX, Am. Math. Soc.Google Scholar
  10. Hai82.
    Hailpern B. T. Verifying concurrent processes using temporal logic, LNCS 129.Google Scholar
  11. Hab84.
    Habasinski Z. Process logics: two decidability results, LNCS 176,:282–290.Google Scholar
  12. Hoa69.
    Hoare C.A.R. The axiomatic basis of computer programming, Comm. of ACM 12,:576–583.Google Scholar
  13. Koz83.
    Kozen D. Results on the propositional Mu-calculus, Th. Comput. Sci. 27,:333–354.Google Scholar
  14. Lam83.
    Lamport L. Specifying concurrent modules, TOPLAS 5(2),:190–222.Google Scholar
  15. Mic84.
    Michel M. Algebre de machines et logique temporelle, LNCS 166, Proc. of STACS.Google Scholar
  16. MP74.
    Manna Z. Pnueli A. Axiomatic approach to total correctness of programs, Acta Informatica 3.Google Scholar
  17. QS81.
    Quielle J.P. Sifakis J. Specification of concurrent systems in CESAR, Proc. of the 5th Int. Symp. in Programming.Google Scholar
  18. SM81.
    Salwicki A. Muldner T. On the algorithmic properties of concurrent programs, LNCS 125,:169–197.Google Scholar
  19. Wol82.
    Wolper P. Synthesis of Communicating Processes from temporal logic specifications, Ph.D.Thesis,Stanford Univ.,California.Google Scholar
  20. Wol86.
    Wolper P. Expressing interesting properties of programs in propositional temporal logic, POPL-Symp.,1986.Google Scholar
  21. WVS83.
    Wolper P. Vardi M.Y. Sistla A.P. Reasoning about infinite computation paths, FOCS-Symp.,:185–194.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1988

Authors and Affiliations

  • Z. Habasiński
    • 1
  1. 1.Computer CentreTechnical Univ. of PoznańPoznańPoland

Personalised recommendations