Advertisement

Minimization of timed transition systems

  • R. Alur
  • C. Courcoubetis
  • N. Halbwachs
  • D. Dill
  • H. Wong-Toi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 630)

Keywords

Model Check Minimization Algorithm Atomic Proposition Region Graph Initial Partition 
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. [1]
    R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proceedings of the Fifth IEEE Symposium on Logic in Computer Science, pages 414–425, 1990.Google Scholar
  2. [2]
    R. Alur and D. Dill. Automata for modeling real-time systems. In Automata, Languages and Programming: Proceedings of the 17th ICALP, Lecture Notes in Computer Science 443, pages 322–335. Springer-Verlag, 1990.Google Scholar
  3. [3]
    R. Alur, T. Feder, and T. Henzinger. The benefits of relaxing punctuality. In Proceedings of the Tenth ACM Symposium on Principles of Distributed Computing, pages 139–152, 1991.Google Scholar
  4. [4]
    R. Alur and T. Henzinger. A really temporal logic. In Proceedings of the 30th IEEE Symposium on Foundations of Computer Science, pages 164–169, 1989. Journal version to appear in the Journal of the ACM.Google Scholar
  5. [5]
    A. Bouajjani, J. Fernandez, and N. Halbwachs. Minimal model generation. In Proceedings of the Second Workshop on Computer-Aided Verification, Rutgers University, 1990.Google Scholar
  6. [6]
    A. Bouajjani, J. Fernandez, N. Halbwachs, P. Raymond, and C. Ratel. Minimal state graph generation. Science of Computer Programming, 1992. To appear.Google Scholar
  7. [7]
    M. Browne, E. Clarke, D. Dill, and B. Mishra. Automatic verification of sequential circuits using temporal logic. IEEE Transactions on Computers, C-35(12):1035–1044, 1986.Google Scholar
  8. [8]
    J. Burch, E. Clarke, D. Dill, L. Hwang, and K. L. McMillan. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth IEEE Symposium on Logic in Computer Science, pages 428–439, 1990.Google Scholar
  9. [9]
    K. Cerans. Decidability of bisimulation equivalence for parallel timer processes. In Proceedings of Chalmers Workshop on Concurrency, Goteborg, 1991.Google Scholar
  10. [10]
    E. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal-logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.zbMATHCrossRefGoogle Scholar
  11. [11]
    C. Courcoubetis and M. Yannakakis. Minimum and maximum delay problems in realtime systems. In Proceedings of the Third Workshop on Computer-Aided Verification, Aalborg University, Denmark, 1991.Google Scholar
  12. [12]
    D. Dill. Timing assumptions and verification of finite-state concurrent systems. In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science 407. Springer-Verlag, 1989.Google Scholar
  13. [13]
    E. Emerson and C. Lei. Modalities for model-checking: Branching time logic strikes back. In Proceedings of the 12th ACM Symposium on Principles of Programming Languages, pages 84–96, 1985.Google Scholar
  14. [14]
    E. A. Emerson and E. M. Clarke. Using branching-time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2:241–266, 1982.zbMATHCrossRefGoogle Scholar
  15. [15]
    E. A. Emerson, A. Mok, A. P. Sistla, and J. Srinivasan. Quantitative temporal reasoning. Presented at the First Workshop on Computer-aided Verification, Grenoble, France, 1989.Google Scholar
  16. [16]
    T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model-checking for real-time systems. In Proceedings of the Seventh IEEE Symposium on Logic in Computer Science, 1992. To appear.Google Scholar
  17. [17]
    D. Lee and M. Yannakakis. Online minimization of transition systems. In Proceedings of ACM Symposium of Theory of Computing, 1992. To appear.Google Scholar
  18. [18]
    H. Lewis. A logic of concrete time intervals. In Proceedings of the Fifth IEEE Symposium on Logic in Computer Science, pages 380–389, 1990.Google Scholar
  19. [19]
    X. Nicollin, J. Sifakis, and S. Yovine. From ATP to timed graphs and hybrid systems. In Proceedings of REX workshop “Real-time: theory in practice”, Lecture Notes in Computer Science 600. Springer-Verlag, 1991.Google Scholar
  20. [20]
    H. Wong-Toi and G. Hoffmann. The control of dense real-time discrete event systems. In Proceedings of the 30th IEEE Conference on Decision and Control, pages 1527–1528, 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • R. Alur
    • 1
  • C. Courcoubetis
    • 2
  • N. Halbwachs
    • 3
  • D. Dill
    • 4
  • H. Wong-Toi
    • 4
  1. 1.AT & T Bell LaboratoriesMurray Hill
  2. 2.University of CreteHeraklionGreece
  3. 3.IMAG InstituteGrenobleFrance
  4. 4.Stanford UniversityStanford

Personalised recommendations