In the paper we offer an algorithm for turning an axiomatization for a behavioural preorder in the linear time-branching time spectrum that includes the ready simulation preorder into an axiomatization for the kernel of the preorder. The algorithm preserves finiteness, ground-completeness and omega-completeness of the axiomatization that it receives as input. The proof of its correctness relies on an analysis of the so-called cover equations for the semantics in the spectrum we study in the paper.
I thoroughly enjoyed working on that paper. The development of the technical details in that work reminded me yet again of a few valuable lessons that I tend to forget when I feel that I am short of time and that I badly need to produce some research output to keep my conscience at bay.
- It is easy to make mistakes in proofs unless one is very careful in checking even the seemingly most obvious of claims. (This is what happens to me at least.)
- Haste is never a good advisor.
- When I feel that a paper is done, I should let it rest for a day, and proof read it once more.
Thanks again to Anna and Wan, the coauthors with whom I have written the largest number of papers, for another very instructive and pleasant collaborations. I hope that there will be another one in the near future.