Abstract
Insight into the global structure of a state space is of great help in the analysis of the underlying process. We advocate the use of visualization for this purpose and present a method to visualize the structure of very large state spaces with millions of nodes. The method uses a clustering based on an equivalence relation to obtain a simplified representation, which is used as a backbone for the display of the entire state space. With this visualization we are able to answer questions about the global structure of a state space that cannot easily be answered by conventional methods. We show this by presenting a number of visualizations of real-world protocols .
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Arnold A (1994) Finite transition systems. Prentice Hall, Englewood Cliffs, NJ
Baeten J, Weijland P (1991) Process algebra. In: Cambridge tracts in theoretical computer science, vol 18. Cambridge University Press, Cambridge, UK
Fernandez J-C, Garavel H, Kerbrat A, Mateescu R, Mounier L, Sighireanu M (1996) CADP – A Protocol Validation and Verification Toolbox. In: Proceedings of the 8th International Conference on Computer Aided Verification. LCNS, vol 1102, Springer, pp 437–440
Blom SCC, Fokkink WJ, Groote JF, van Langevelde IA, Lisser B, van de Pol JC (2001) mCRL: A toolset for analysing algebraic specifications. In: Computer-Aided Verification (CAV 2001). Lecture notes in computer science, vol 2102. Springer, Berlin Heidelberg New York, pp 250–254
Carrière J, Kazman R (1995) Research report: interacting with huge hierarchies: beyond cone trees. In: Proceedings of the IEEE conference on information visualization. IEEE Press, New York, pp 74–81
Gansner ER, North SC (2000) An open graph visualization system and its applications to software engineering. Softw Practice Exper 30(11):1203–1233
Garavel H et al. (2003) The VLTS (Very Large Transition System) Benchmark suite. http://www.inrialpes.fr/vasy/cadp/resources/benchmark_bcg.html
Groote JF, Pang J, Wouters AG (2003) Analysis of a distributed system for lifting trucks. The Journal of Logic and Algebraic Programming 55(1–2):21–56
Groote JF, van Ham F (2003) Large state space visualization. In: Proceedings of TACAS 2003, pp 585–590
van Ham F, van de Wetering H, van Wijk JJ (2002) Visualization of state transition graphs. IEEE Trans Visual Comput Graph 8(4):319–329
IEEE Computer Society (1996) IEEE standard for a high performance serial bus, Std 1394-1995 , August 1996
Jéron T, Jard C (1994) 3D layout of reachability graphs of communicating processes. In: Proceedings of the DIMACS international workshop on graph drawing. Springer, Berlin Heidelberg New York, pp 25–32
Koren Y, Carmel L, Harel D (2001) ACE: A fast multiscale eigenvectors computation for drawing huge graphs. Technical Report MCS01-17, Weizmann Institute Of Science. http://www.wisdom.weizmann.ac.il/reports.html
van Langevelde IA (2001) A compact file format for labeled transition systems. Technical report SEN-R0102, CWI, Amsterdam, The Netherlands
Luttik SP (1997) Description and formal specification of the link layer of P1394. Technical report SEN-R9706, CWI, Amsterdam, The Netherlands
Mauw S, Veltink GJ (eds) (1993) Algebraic specifications of communication protocols. Cambridge tracts in theoretical computer science, vol 36. Cambridge University Press, Cambridge, UK
Robertson GG, Mackinlay JD, Card SK (1991) Cone trees: animated 3D visualizations of hierarchical information. In: Proceedings of the conference on human factors in computing systems (CHI ’91), pp 189–194
Tutte W (1963) How to draw a graph. Proc Lond Math Soc 3(13):743–768
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Groote, J., van Ham, F. Interactive visualization of large state spaces. Int J Softw Tools Technol Transfer 8, 77–91 (2006). https://doi.org/10.1007/s10009-005-0198-5
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-005-0198-5