I am interested in simulations between labelled transition systems (LTS).

LTS are basically relational systems, in particular they can be viewed as structures for a purely binary relational signature (i.e. a signature having only binary relation symbols).

In my understanding simulations between LTS should be regarded as some form of morphisms between these structures.

So why do we use simulations as congruence relations (that is relations compatible with the transition relations) instead of homomorphisms of the relational structures?

Is there any theoretical reason that makes relations more suited than functions for the purposes of similarity-bisimilarity?

  • 1
    $\begingroup$ Don't have time for a full comment: simulations that are computationally relevant tend to be quite complicated (e.g. weak rather than strong, respecting/ignoring termination, security levels etc, see eg. R. van Glabbeek, The Linear Time - Branching Time Spectrum for a small overview from the 1990s), and it has been rather difficult to phrase them as homomorphisms. The naive relational definition is simple and does the job, unless you are interested in maximum abstractness. See also V. Sassone et al, Models for concurrency: Towards a classification for some early attempts at abstraction. $\endgroup$ May 12, 2018 at 10:54


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.