Visualisation of large Labelled Transition Systems
Creators: name: Van Ieperen, Geert
Publisher: name: Zenodo
Year: 2021
Subjects: Labelled Transition Systems
State space visualisation
Graph rendering

description: A formal model describes the behaviour of a program, protocol or other system.<br> The properties of this model can be verified, such that we can prove these properties with absolute certainty. Visualising the state space of a formal model is an important tool for their development<br> This thesis focuses on visualising such a state space as a graph. We present a layout technique that provides efficient graph layouts for graphs with over 10000 nodes, <br> discuss the effectiveness of different edge shapes,<br> and present multiple ways of highlighting the structure of the graph.<br> We present a rendering procedure capable of rendering graphs larger than 10000 nodes while supporting these techniques.<br> We implemented these techniques in a tool and use it to measure the performance of the techniques.<br> The effectiveness of these techniques is analysed using a survey on the tool in a few practical applications. We conclude that these techniques can effectively be used in one visualisation to assist in formal model development.
description: {"references": ["Laura Bahiense, Gordana Manic, Breno Piva, and Cid C. de Souza. The maximum common edge subgraph problem: A polyhedral investigation. Discrete Applied Mathematics, 160(18):2523-2541, 2012.", "Gianluca Barbon, Vincent Leroy, and Gwen Sala\u00fcn. Debugging of behavioural models with clear. In Tools and Algorithms for the Construction and Analysis of Systems, pages 386-392, Cham, 2019. Springer International Publishing", "J. Barnes and P. Hut. A hierarchical o(n log n) force-calculation algorithm. page 446-449. Nature, 1986", "Olav Bunte, Jan Friso Groote, Jeroen J. A. Keiren, Maurice Laveaux, Thomas Neele, Erik P. de Vink, Wieger Wesselink, Anton Wijs, and Tim A. C. Willemse. The mcrl2 toolset for analysing concurrent systems. In Tomas Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 21-39, Cham, 2019. Springer International Publishing", "Roberto Gorrieri. Labeled Transition Systems, pages 15-34. Springer International Publishing, Cham, 2017", "Jan Friso Groote and Jaco van de Pol. State space reduction using partial tau-confluence. In Mathematical Foundations of Computer Science 2000, pages 383-393. Springer, 2000.", "David Harel and Yehuda Koren. Graph drawing by high-dimensional embedding. In International symposium on graph drawing, pages 207-219. Springer, 2002", "Nathalie Henry and Jean-Daniel Fekete. Matlink: Enhanced matrix visualization for analyzing social networks. page 288-302. Springer, 2007", "Bas Ploeger and Carst Tankink. Improving an interactive visualization of transition systems. SoftVis '08, page 115-124, New York, NY, USA, 2008. Association for Computing Machinery.", "A. J. Pretorius and J. J. Van Wijk. Visual analysis of multivariate state transition graphs. IEEE Transactions on Visualization and Computer Graphics, 12(5):685-692, 2006.", "Claudia M. Eckert Ren\u00e9 Keller and P. John Clarkson. Matrices or node-link diagrams: which visual representation is better for visualising connectivity models? volume Information Visualization, page 5(1):62-76, 2006", "Zeqian Sheny and Kwan-Liu Maz. Path visualization for adjacency matrices. volume VGTC conference on Visualization, page 83-90. Eurographics Association, 2007"]}