We propose behavioral specification theories for most equivalences in the linear-time--branching-time spectrum. Almost all previous work on specification theories focuses on bisimilarity, but there is a clear interest in specification theories for other preorders and equivalences. We show that specification theories for preorders cannot exist and develop a general scheme which allows us to define behavioral specification theories, based on disjunctive modal transition systems, for most equivalences in the linear-time--branching-time spectrum.
Fahrenberg, U., & Legay, A. (2020). A linear-time–branching-time spectrum for behavioral specification theories. The Journal of Logical and Algebraic Methods in Programming, 110(110), 100499. https://doi.org/10.1016/j.jlamp.2019.100499 (Original work published 2020)