All congruences below stability-preserving fair testing or CFFD
Valmari, A. (2020). All congruences below stability-preserving fair testing or CFFD. Acta Informatica, 57(3-5), 353-383. https://doi.org/10.1007/s00236-019-00364-4
Published in
Acta InformaticaAuthors
Date
2020Copyright
© 2020 the Author(s)
In process algebras, a congruence is an equivalence that remains valid when any subsystem is replaced by an equivalent one. Whether or not an equivalence is a congruence depends on the set of operators used in building systems from subsystems. Numerous congruences have been found, differing from each other in fine details, major ideas, or both, and none of them is good for all situations. The world of congruences seems thus chaotic, which is unpleasant, because the notion of congruence is at the heart of process algebras. This study continues attempts to clarify the big picture by proving that in certain sub-areas, there are no other congruences than those that are already known or found in the study. First, the region below stability-preserving fair testing equivalence is surveyed using an exceptionally small set of operators. The region contains few congruences, which is in sharp contrast with an earlier result on the region below Chaos-Free Failures Divergences (CFFD) equivalence, which contains 40 well-known and not well-known congruences. Second, steps are taken towards a general theory of dealing with initial stability, which is a small but popular detail. This theory is applied to the region below CFFD.
...


Publisher
SpringerISSN Search the Publication Forum
0001-5903Keywords
Publication in research information system
https://converis.jyu.fi/converis/portal/detail/Publication/35410861
Metadata
Show full item recordCollections
Additional information about funding
Open access funding provided by University of Jyväskylä (JYU).License
Related items
Showing items with similar title or keywords.
-
Stubborn Sets, Frozen Actions, and Fair Testing
Valmari, Antti; Vogler, Walter (IOS Press, 2021)Many partial order methods use some special condition for ensuring that the analysis is not terminated prematurely. In the case of stubborn set methods for safety properties, implementation of the condition is usually based ... -
The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction
Neele, Thomas; Valmari, Antti; Willemse, Tim A. C (Springer, 2020)In model checking, partial-order reduction (POR) is an effective technique to reduce the size of the state space. Stubborn sets are an established variant of POR and have seen many applications over the past 31 years. One ... -
A Detailed Account of The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction
Neele, Thomas; Valmari, Antti; Willemse, Tim A. C. (Logical Methods in Computer Science e.V., 2021)One of the most popular state-space reduction techniques for model checking is partial-order reduction (POR). Of the many different POR implementations, stubborn sets are a very versatile variant and have thus seen many ... -
Matriisikertolaskun kustannusmalli hajautetun ja jaetun muistin rinnakkaistietokoneille
Moilanen, Marko (2023)Merkittävä rinnakkaisohjelman suorituskykyyn vaikuttava tekijä on laskennan ja viestinnän välinen tasapaino. Tutkielmassa kehitettiin rinnakkaisalgoritmi ja sitä vastaava kustannusmalli matriisikertolaskulle C = AB, missä ... -
GPU-accelerated time integration of Gross-Pitaevskii equation with discrete exterior calculus
Kivioja, Markus; Mönkölä, Sanna; Rossi, Tuomo (Elsevier BV, 2022)The quantized vortices in superfluids are modeled by the Gross-Pitaevskii equation whose numerical time integration is instrumental in the physics studies of such systems. In this paper, we present a reliable numerical ...