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} }