Logic in Computer Science (LICS 1992)

Paper: Symbolic model checking for real-time systems (at LICS 1992)

Authors: Henzinger, T.A. Nicollin, X. Sifakis, J. Yovine, S.

Abstract

Finite-state programs over real-numbered time in a guarded-command language with real-valued clocks are described. Model checking answers the question of which states of a real-time program satisfy a branching-time specification. An algorithm that computes this set of states symbolically as a fixpoint of a functional on state predicates, without constructing the state space, is given

BibTeX

  @InProceedings{HenzingerNicollinSi-Symbolicmodelchecki,
    author = 	 {Henzinger, T.A. and Nicollin, X. and Sifakis, J. and Yovine, S.},
    title = 	 {Symbolic model checking for real-time systems},
    booktitle =  {Proceedings of the Seventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1992},
    year =	 1992,
    editor =	 {Andre Scedrov},
    month =	 {June}, 
    pages =      {394--406},
    location =   {Santa Cruz, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }