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

Authors: Thomas A. Henzinger Xavier Nicollin Joseph Sifakis Sergio Yovine

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 = 	 {Thomas A. Henzinger and Xavier Nicollin and Joseph Sifakis and Sergio Yovine},
    title = 	 {Symbolic model checking for real-time systems},
    booktitle =  {Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science (LICS 1992)},
    year =	 {1992},
    month =	 {June}, 
    pages =      {394--406},
    location =   {Santa Cruz, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }