Submitted: September 2014
Abstract
Labelled transition systems (LTS) are a popular way of modelling the behaviour of reactive systems and processes. Consequently, there are many tools to create, view and analyse such systems. However, many of these tools are hard to set up or use or cannot work with large or infinite transition systems. This unnecessarily complicates the use of such systems, especially for teaching. There, complex set-up cannot be expected from students, and infinite systems are regularly analysed while exploring the limits of LTS and languages having LTS semantics.
For this thesis, a new application handling labelled transition systems was developed – pseuCo.com. Being a JavaScript-based web application, it offers a set-up-free experience, while still keeping many advantages of classic, native applications, like offline use.
In addition, pseuCo.com was designed to work with large or infinite transition systems as well as with small ones, enabling users to view and analyse them just as they would expect. Users can visualize any transition system right in their browser, with the ability to expand and collapse states as they wish. While automatic graph layout keeps the system easily readable even as states appear and disappear, users are free to rearrange states as they wish. Support for (partial) minimization – even of infinite systems – allows to get a faster overview over the behaviour modelled by a system.
PseuCo.com includes a compiler from pseuCo to CCS, and a mechanism to convert CCS terms to labelled transition systems. Both are based on PseuCoCo, and seamlessly integrated into the user interface.
PseuCo.com features an internal file system for supported file types, with extensive import and export capabilities. A link-based file sharing mechanism enables users to easily send pseuCo.com-files to any user, without requiring anything but an internet connection and a modern browser from the receiver.