Compositional and Symbolic Model-Checking of Real-Time Systems


  • Kim G. Larsen
  • Paul Pettersson
  • Wang Yi



Efficient automatic model-checking algorithms for
real-time systems have been obtained in recent years
based on the state-region graph technique of Alur,
Courcoubetis and Dill. However, these algorithms are
faced with two potential types of explosion arising from
parallel composition: explosion in the space of control
nodes, and explosion in the region space over clock variables.
In this paper we attack these explosion problems by
developing and combining compositional and symbolic
model-checking techniques. The presented techniques
provide the foundation for a new automatic verification
tool Uppaal. Experimental results indicate that
Uppaal performs time- and space-wise favorably compared
with other real-time verification tools.




How to Cite

Larsen, K. G., Pettersson, P., & Yi, W. (1996). Compositional and Symbolic Model-Checking of Real-Time Systems. BRICS Report Series, 3(59).