Advertisement

Formal Methods in System Design

, Volume 26, Issue 1, pp 7–25 | Cite as

Deciding Global Partial-Order Properties

  • Rajeev Alur
  • Ken McMillan
  • Doron Peled
Article

Abstract

Model checking of asynchronous systems is traditionally based on the interleaving model, where an execution is modeled by a total order between atomic events. Recently, the use of partial order semantics, representing the causal order between events, is becoming popular. This paper considers the model checking problem for partial-order temporal logics. Solutions to this problem exist for partial order logics over local states. For the more general global logics that are interpreted over global states, only undecidability results have been proved. In this paper, we present a decision procedure for a partial order temporal logic over global states. We also sharpen the undecidability results by showing that a single until operator is sufficient for undecidability.

model checking temporal logics partial order logics concurrency 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    R. Alur, K. McMillan, and D. Peled, “model-checking of correctness conditions for concurrent objects,” in LICS96, 11th IEEE Symposium on Logic in Computer Science, New Brunswick, NJ, USA, 1996, pp. 219–228.Google Scholar
  2. 2.
    R. Alur, W. Penczek, and D. Peled, “Model-checking of causality properties,” in 10th Symposium on Logic in Computer Science, 1995, pp. 90–100.Google Scholar
  3. 3.
    W. Ebinger, “Logical definability of trace languages,” in V. Diekert and G. Rozenberg (Eds.), The Book of Traces, World Scientific, 1995, pp. 382–390.Google Scholar
  4. 4.
    P. Godefroid and P. Wolper, “A partial approach to model checking,” Information and Computation, Vol. 110, No. 2, pp. 305–326, 1994.Google Scholar
  5. 5.
    G. Holzmann and D. Peled, “The state of SPIN,” in 8th Conference on Computer-Aided Verification, Lecture Notes in Computer Science, Vol. 1102, 1996, pp. 385–389.Google Scholar
  6. 6.
    S. Katz and D. Peled, “Interleaving set temporal logic,” Theoretical Computer Science, Vol. 75, pp. 21–43, 1992.Google Scholar
  7. 7.
    O. Lichtenstein and A. Pnueli, “Checking that finite-state concurrent programs satisfy their linear specification,” in 11th ACM Symposium on Principles of Programming Languages, 1984, pp. 97–107.Google Scholar
  8. 8.
    K. Lodaya, R. Parikh, R. Ramanujam, and P.S. Thiagarajan, “A logical study of distributed transitions systems,” Information and Computation, Vol. 119, pp. 91–118, 1985.Google Scholar
  9. 9.
    A. Mazurkiewicz, “Trace theory,” in W. Brauer, W. Reisig, and G. Rozenberg (Eds.), Advances in Petri Nets 1986, Vol. 255, Lecture Notes in Computer Science, 1987, pp. 279–324.Google Scholar
  10. 10.
    K.L. McMillan, “Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits,” in 4th Conference on Computer-Aided Verification, Lecture Notes in Computer Science, Vol. 663, 1992, pp. 164–177.Google Scholar
  11. 11.
    D. Peled, “Combining partial order reductions with on-the-fly model checking,” in Proc. 6th Conference on Computer Aided Verification, Lecture Notes in Computer Science, Vol. 818, 1994, pp. 377–390.Google Scholar
  12. 12.
    W. Penczek and R. Kuiper, “Traces and logic,” in V. Diekert and G. Rozenberg (Eds.), The Book of Traces, World Scientific, 1995, pp. 307–390.Google Scholar
  13. 13.
    W. Penczek, “On undecidability of propositional temporal logics on trace systems,” Information Processing Letters, Vol. 43, pp. 147–153, 1992.Google Scholar
  14. 14.
    D. Peled and A. Pnueli, “Proving partial order properties,” Theoretical Computer Science, Vol. 126, pp. 143–182, 1994.Google Scholar
  15. 15.
    S. Pinter and P. Wolper, “A temporal logic for reasoning about partially ordered computations,” in 3rd ACM Symposium on Principles of Distributed Computing, 1984, pp. 28–37.Google Scholar
  16. 16.
    V.R. Pratt, “Modeling concurrency with partial orders,” Intl. J. of Parallel Programming, Vol. 15, No. 1, pp. 33–71, 1986.Google Scholar
  17. 17.
    W.J. Savitch, “Relationship between nondeterministic and deterministic tape complexities,” J. on Computer and System Sciences, Vol. 4, pp. 177–192, 1970.Google Scholar
  18. 18.
    P.S. Thiagarajan, “A trace based extension of linear time temporal logic,” in Ninth Symposium on Logic in Computer Science, 1994, pp. 438–447.Google Scholar
  19. 19.
    A. Valmari, “A Stubborn attack on state explosion,” in Proc. 2nd Conference on Computer-Aided Verification, Lecture Notes in Computer Science, Vol. 531, 1990, pp. 156–165.Google Scholar
  20. 20.
    M.Y. Vardi and P. Wolper, “An automata-theoretic approach to automatic program verification,” in First Symposium on Logic in Computer Science, 1986, pp. 332–344.Google Scholar
  21. 21.
    D. Peled and T. Wilke, “Stutter invariant temporal properties are expressible without the next-time operator,” Information Processing Letters, Vol. 63, No. 5, pp. 243–246, 1997.Google Scholar
  22. 22.
    W. Zielonka, “Notes on finite asynchronous automata,” R.A.I.R.O.-Informatique Théorique et. Applications, Vol. 21, pp. 99–135, 1987.Google Scholar

Copyright information

© Springer Science + Business Media, Inc. 2005

Authors and Affiliations

  1. 1.Department of Computer and Information ScienceUniversity of Pennsylvania
  2. 2.Cadence Berkeley LabsUSA
  3. 3.Department of Computer ScienceUniversity of WarwickWarwick

Personalised recommendations