@article{Larsen_Pettersson_Yi_1996, title={Compositional and Symbolic Model-Checking of Real-Time Systems}, volume={3}, url={https://tidsskrift.dk/brics/article/view/18770}, DOI={10.7146/brics.v3i59.18770}, abstractNote={Efficient automatic model-checking algorithms for<br />real-time systems have been obtained in recent years<br />based on the state-region graph technique of Alur,<br />Courcoubetis and Dill. However, these algorithms are<br />faced with two potential types of explosion arising from<br />parallel composition: explosion in the space of control<br />nodes, and explosion in the region space over clock variables.<br />In this paper we attack these explosion problems by<br />developing and combining compositional and symbolic<br />model-checking techniques. The presented techniques<br />provide the foundation for a new automatic verification<br />tool Uppaal. Experimental results indicate that<br />Uppaal performs time- and space-wise favorably compared<br />with other real-time verification tools.}, number={59}, journal={BRICS Report Series}, author={Larsen, Kim G. and Pettersson, Paul and Yi, Wang}, year={1996}, month={Jun.} }