Partial-Order Reduction

Chapter

Abstract

Partial order reduction methods help reduce the time and space required to automatically verify concurrent asynchronous systems based on commutativity between concurrently executed transitions. We describe partial order reduction for various specification formalisms, such as LTL, CTL, and process algebra.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alur, R., Brayton, R., Henzinger, T., Qadeer, S., Rajamani, S.: Partial order reduction in symbolic state space exploration. In: Grumberg, O. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1254, pp. 340–351. Springer, Heidelberg (1997) CrossRefGoogle Scholar
  2. 2.
    Bosnacki, D., Elkind, E., Genest, B., Peled, D.: On commutativity based edge lean search. In: Arge, L., Cachin, C., Jurdzinski, T., Tarlecki, A. (eds.) Intl. Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol. 4596, pp. 158–170. Springer, Heidelberg (2007) CrossRefGoogle Scholar
  3. 3.
    Browne, M., Clarke, E., Grumberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theor. Comput. Sci. 59(1–2), 115–131 (1988) MathSciNetCrossRefGoogle Scholar
  4. 4.
    Chou, C., Peled, D.: Verifying a model-checking algorithm. In: Margaria, T., Steffen, B. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 1055, pp. 241–257. Springer, Heidelberg (1996) Google Scholar
  5. 5.
    Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000) Google Scholar
  6. 6.
    Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. Form. Methods Syst. Des. 1(2–3), 275–288 (1992) CrossRefGoogle Scholar
  7. 7.
    De Nicola, R., Vaandrager, F.: Three logics for branching bisimulation. In: Symp. on Logic in Computer Science, vol. LICS, pp. 118–129. IEEE, Piscataway (1990) Google Scholar
  8. 8.
    Esparza, J., Heljanko, K.: Unfoldings—a partial-order approach to model checking. EATCS Monographs in Theoretical Computer Science. Springer, Heidelberg (2008) MATHGoogle Scholar
  9. 9.
    Gerth, R., Kuiper, R., Penczek, W., Peled, D.: A partial order approach to branching time logic model checking. In: Israel Symp. on the Theory of Computing and Systems (ISTCS), pp. 130–139. IEEE, Piscataway (1995). Full version in Information and Computation 150(2), 132–152 (1999) Google Scholar
  10. 10.
    Gerth, R., Peled, D., Vardi, M., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembinski, P., Sredniawa, M. (eds.) Intl. Symp. on Protocol Specification, Testing and Verification (PSTV). IFIP Conference Proceedings, vol. 38, pp. 3–18. Chapman & Hall, London (1995) Google Scholar
  11. 11.
    van Glabbeek, R., Weijland, W.: Branching time and abstraction in bisimulation semantics. In: Ritter, G.X. (ed.) Information Processing 89, Proc. of the IFIP World Computer Congress, pp. 613–618. North-Holland/IFIP, Amsterdam (1989) Google Scholar
  12. 12.
    Godefroid, P., Peled, D., Staskauskas, M.: Using partial order methods in the formal validation of industrial concurrent programs. In: Zeil, S.J. (ed.) Intl. Symp. on Software Testing and Analysis (ISSTA). Software Engineering Notes, vol. 21, pp. 261–269. ACM Press, New York (1996) Google Scholar
  13. 13.
    Godefroid, P., Pirottin, D.: Refining dependencies improves partial order verification methods. In: Courcoubetis, C. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 697, pp. 438–449. Springer, Heidelberg (1993) CrossRefGoogle Scholar
  14. 14.
    Godefroid, P., Wolper, P.: Using partial orders for the efficient verification of deadlock freedom and safety properties. In: Larsen, K.G., Skou, A. (eds.) Intl. Workshop on Computer-Aided Verification (CAV). LNCS, vol. 575, pp. 332–342. Springer, Heidelberg (1991) CrossRefGoogle Scholar
  15. 15.
    Godefroid, P., Wolper, P.: Using partial orders for the efficient verification of deadlock freedom and safety properties. Form. Methods Syst. Des. 2(2), 149–164 (1993) CrossRefGoogle Scholar
  16. 16.
    Holzmann, G., Godefroid, P., Pirottin, D.: Coverage preserving reduction strategies for reachability analysis. In: Linn, R.J. Jr., Uyar, M.Ü. (eds.) Intl. Symp. on Protocol Specification, Testing and Verification (PSTV). IFIP Transactions, vol. C-8, pp. 349–363. North-Holland, Amsterdam (1992) CrossRefGoogle Scholar
  17. 17.
    Holzmann, G., Peled, D.: An improvement in formal verification. In: Hogrefe, D., Leue, S. (eds.) Intl. Conf. on Formal Description Techniques (FORTE). IFIP Conference Proceedings, vol. 6, pp. 197–211. Chapman & Hall, London (1994) Google Scholar
  18. 18.
    Holzmann, G.J., Peled, D., Yannakakis, M.: On nested depth first search. In: Grégoire, J.C., Holzmann, G.J., Peled, D.A. (eds.) Workshop on the SPIN Verification System. DIMACS: Series in Discrete Mathematics and Theoretical Computer Science, vol. 32, pp. 23–32. AMS/DIMACS, Providence (1996) CrossRefGoogle Scholar
  19. 19.
    Kahlon, V., Wang, C., Gupta, A.: Monotonic partial order reduction: an optimal symbolic partial order reduction technique. In: Bouajjani, A., Maler, O. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 5643, pp. 398–413. Springer, Heidelberg (2009) CrossRefGoogle Scholar
  20. 20.
    Katz, S., Peled, D.: An efficient verification method for parallel and distributed programs. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds.) REX Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. LNCS, vol. 354, pp. 489–507. Springer, Heidelberg (1988) CrossRefGoogle Scholar
  21. 21.
    Katz, S., Peled, D.: Defining conditional independence using collapses. Theor. Comput. Sci. 101(2), 337–359 (1992) MathSciNetCrossRefGoogle Scholar
  22. 22.
    Kokkarinen, I., Peled, D., Valmari, A.: Relaxed visibility enhances partial order reduction. In: Grumberg, O. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1254, pp. 328–339. Springer, Heidelberg (1997) CrossRefGoogle Scholar
  23. 23.
    Kurshan, R., Levin, V., Minea, M., Peled, D., Yenigün, H.: Static partial order reduction. In: Steffen, B. (ed.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 1384, pp. 345–357. Springer, Heidelberg (1998) Google Scholar
  24. 24.
    Lamport, L.: What good is temporal logic. In: Mason, R. (ed.) Information Processing 83, Proc. of the World Computer Congress, pp. 657–668. North-Holland/IFIP, Amsterdam (1983) Google Scholar
  25. 25.
    Mazurkiewicz, A.: Trace theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) Petri Nets: Central Models and Their Properties, Advances in Petri Nets (APN). LNCS, vol. 255, pp. 279–324. Springer, Heidelberg (1986) Google Scholar
  26. 26.
    McMillan, K.L.: Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: Gregor von Bochmann, D.K.P. (ed.) Intl. Workshop on Computer-Aided Verification (CAV). LNCS, vol. 663, pp. 164–177. Springer, Heidelberg (1992) CrossRefGoogle Scholar
  27. 27.
    Milner, R.: A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980) MATHGoogle Scholar
  28. 28.
    Ochmanski, E.: Languages and automata. In: Diekert, V., Rozenberg, G. (eds.) The Book of Traces, pp. 167–204. World Scientific, Singapore (1995) CrossRefGoogle Scholar
  29. 29.
    Peled, D.: All from one, one for all, on model-checking using representatives. In: Courcoubetis, C. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993) CrossRefGoogle Scholar
  30. 30.
    Peled, D.: Combining partial order reductions with on-the-fly model-checking. Form. Methods Syst. Des. 8(1), 39–64 (1996) CrossRefGoogle Scholar
  31. 31.
    Peled, D., Wilke, T.: Stutter-invariant temporal properties are expressible without the nexttime operator. Inf. Process. Lett. 63(5), 243–246 (1997) CrossRefGoogle Scholar
  32. 32.
    Peled, D., Wilke, T., Wolper, P.: An algorithmic approach for checking closure properties of \(\omega\)-regular languages. In: Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 1119, pp. 596–610. Springer, Heidelberg (1996) CrossRefGoogle Scholar
  33. 33.
    Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) Intl. Conf. on Applications and Theory of Petri Nets (APN). LNCS, vol. 483, pp. 491–515. Springer, Heidelberg (1989) Google Scholar
  34. 34.
    Valmari, A.: On-the-fly verification with stubborn sets. In: Courcoubetis, C. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 697, pp. 397–408. Springer, Heidelberg (1993) CrossRefGoogle Scholar
  35. 35.
    Valmari, A.: Stubborn set methods for process algebras. In: Peled, D.A., Pratt, V.R., Holzmann, G.J. (eds.) DIMACS Workshop on Partial Order Methods in Verification (POMIV). DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 29, pp. 213–231. AMS, Providence (1996) CrossRefGoogle Scholar
  36. 36.
    Vardi, M., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Symp. on Logic in Computer Science (LICS), pp. 322–331. IEEE, Piscataway (1986) Google Scholar
  37. 37.
    Winskel, G.: An introduction to event structures. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds.) REX Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. LNCS, vol. 354, pp. 364–397. Springer, Heidelberg (1988) CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Bar Ilan UniversityRamat GanIsrael

Personalised recommendations