Automated Verification of Infinite State Concurrent Systems

  • Piotr Dembiński
  • Wojciech Penczek
  • Agata Pólrola
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2328)


The paper shows how to use partitioning techniques to generate abstract state spaces (models) preserving similarity and injectivity. Since these relations are weaker than bisimilarity and surjectivity, our algorithms generate smaller models. This method can be applied for improving several existing partitioning algorithms used for generating finite models of concurrent programs, Time Petri Nets and Timed Automata.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [ACD+92a]_R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi, An implementation of three algorithms for timing verification based on automata emptiness, Proc. of the 13th IEEE Real-Time Systems Symposium (RTSS’92), IEEE Soc. Press, 1992, pp. 157–166.Google Scholar
  2. [ACD+92b]_R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi, Minimization of timed transition systems, Proc. of CONCUR’92, LNCS, vol. 630, Springer-Verlag, 1992, pp. 340–354.Google Scholar
  3. [BCG88]
    M. C. Browne, E. M. Clarke, and O. Grumberg, Characterizing finite Kripke structures in propositional temporal logic, Theoretical Computer Science 59(1/2) (1988), 115–131.MathSciNetzbMATHCrossRefGoogle Scholar
  4. [BFH+92]_A. Bouajjani, J-C. Fernandez, N. Halbwachs, P. Raymond, and C. Ratel, Minimal state graph generation, Science of Computer Programming 18 (1992), 247–269.MathSciNetzbMATHCrossRefGoogle Scholar
  5. [BG00]
    D. Bustan and O. Grumberg, Simulation based minimization, Proc. of the 17th Int. Conf. on Automated Deduction (ICAD’2000) (Pittsburgh), 2000, pp. 255–270.Google Scholar
  6. [Dil89]
    D. Dill, Timing assumptions and verification of finite state concurrent systems, Automatic Verification Methods for Finite-State Systems, LNCS, vol. 407, Springer-Verlag, 1989, pp. 197–212.CrossRefGoogle Scholar
  7. [GKP92]
    U. Goltz, R. Kuiper, and W. Penczek, Propositional temporal logics and equivalences, Proc. of CONCUR’92, LNCS, vol. 630, Springer-Verlag, 1992, pp. 222–236.Google Scholar
  8. [GL91]
    O. Grumberg and D. E. Long, Model checking and modular verification, Proc. of CONCUR’91, LNCS, vol. 527, Springer-Verlag, 1991, pp. 250–265.Google Scholar
  9. [HHK95]
    M. Henzinger, T. Henzinger, and P. Kopke, Computing simulations on finite and infinite graphs, Proc. of the 36th Annual IEEE Symposium on Foundations of Computer Science (FOCS’95), 1995, pp. 453–462.Google Scholar
  10. [PP01]
    W. Penczek and A. Półrola, Abstractions and partial order reductions for checking branching properties of Time Petri Nets, Proc. of the Int. Conf. on Applications and Theory of Petri Nets (ICATPN’01), LNCS, vol. 2075, Springer-Verlag, 2001, pp. 323–342.Google Scholar
  11. [TY96]
    S. Tripakis and S. Yovine, Analysis of timed systems based on time-abstracting bisimulations, Proc. of CAV’96, LNCS, vol. 1102, Springer-Verlag, 1996, pp. 232–243.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Piotr Dembiński
    • 1
  • Wojciech Penczek
    • 1
  • Agata Pólrola
    • 2
  1. 1.Institute of Computer Science, PASWarsawPoland
  2. 2.Faculty of MathematicsUniversity of LodzLodzPoland

Personalised recommendations