All Linear-Time Congruences for Familiar Operators
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 absenc...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2013-11-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/858/pdf |
| _version_ | 1797268715628134400 |
|---|---|
| author | Antti Valmari |
| author_facet | Antti Valmari |
| author_sort | Antti Valmari |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:36:53Z |
| format | Article |
| id | doaj.art-b073169f528f4083b4616264419048dd |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:53Z |
| publishDate | 2013-11-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-b073169f528f4083b4616264419048dd2024-03-08T09:30:37ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742013-11-01Volume 9, Issue 410.2168/LMCS-9(4:11)2013858All Linear-Time Congruences for Familiar OperatorsAntti ValmariThe 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.https://lmcs.episciences.org/858/pdfcomputer science - logic in computer science |
| spellingShingle | Antti Valmari All Linear-Time Congruences for Familiar Operators Logical Methods in Computer Science computer science - logic in computer science |
| title | All Linear-Time Congruences for Familiar Operators |
| title_full | All Linear-Time Congruences for Familiar Operators |
| title_fullStr | All Linear-Time Congruences for Familiar Operators |
| title_full_unstemmed | All Linear-Time Congruences for Familiar Operators |
| title_short | All Linear-Time Congruences for Familiar Operators |
| title_sort | all linear time congruences for familiar operators |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/858/pdf |
| work_keys_str_mv | AT anttivalmari alllineartimecongruencesforfamiliaroperators |