Antti Valmari - All Linear-Time Congruences for Familiar Operators

lmcs:858 - Logical Methods in Computer Science, November 12, 2013, Volume 9, Issue 4 - https://doi.org/10.2168/LMCS-9(4:11)2013
All Linear-Time Congruences for Familiar Operators

Authors: Antti Valmari

    The detailed behaviour of a system is often represented as a labelled transition system (LTS) and the abstract behaviour as a stuttering-insensitive semantic congruence. Numerous congruences have been presented in the literature. On the other hand, there have not been many results proving the absence of more congruences. This publication fully analyses the linear-time (in a well-defined sense) region with respect to action prefix, hiding, relational renaming, and parallel composition. It contains 40 congruences. They are built from the alphabet, two kinds of traces, two kinds of divergence traces, five kinds of failures, and four kinds of infinite traces. In the case of finite LTSs, infinite traces lose their role and the number of congruences drops to 20. The publication concentrates on the hardest and most novel part of the result, that is, proving the absence of more congruences.


    Volume: Volume 9, Issue 4
    Published on: November 12, 2013
    Accepted on: June 25, 2015
    Submitted on: January 15, 2013
    Keywords: Computer Science - Logic in Computer Science

    1 Document citing this article

    Share

    Consultation statistics

    This page has been seen 320 times.
    This article's PDF has been downloaded 240 times.