Antti Valmari - All Linear-Time Congruences for Familiar Operators

lmcs:858 - Logical Methods in Computer Science, November 12, 2013, Volume 9, Issue 4 -
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


Consultation statistics

This page has been seen 273 times.
This article's PDF has been downloaded 207 times.