Title :
Symbolic model checking for real-time systems
Author :
Henzinger, Thomas A. ; Nicollin, X. ; Sifakis, Joseph ; Yovine, S.
Author_Institution :
Dept. of Comput. Sci., Cornell Univ., Ithaca, NY, USA
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
Keywords :
formal specification; program verification; programming theory; real-time systems; CTL; automatic verification; branching-time specification; finite state programs; guarded-command language; real-numbered time; real-time program; real-time systems; real-valued clocks; state predicates; state space; symbolic model checking; Algorithm design and analysis; Boolean functions; Clocks; Computer science; Data structures; Power system modeling; Real time systems; Safety; State-space methods; Upper bound;
Conference_Titel :
Logic in Computer Science, 1992. LICS '92., Proceedings of the Seventh Annual IEEE Symposium on
Conference_Location :
Santa Cruz, CA
Print_ISBN :
0-8186-2735-2
DOI :
10.1109/LICS.1992.185551
