Wan Fokkink, Anna Ingolfsdottir and I have recently completed the paper A Cancellation Theorem for BCCSP, which is now available from the web page where Anna and I collect our papers.
The aim of this paper is to prove a cancellation result for the language BCCSP modulo all the classic semantics in van Glabbeek's linear time-branching time spectrum. The statement of this result is as follows.
Theorem. Let t and u be BCCSP terms that do not contain the variable x as a summand. Let <= be a preorder in van Glabbeek's spectrum. If t+x <= u+x then t <= u.
Apart from having some intrinsic interest, this cancellation result plays a crucial role in the study of the cover equations, in the sense of Fokkink and Nain, that characterize the studied semantics.
Fokkink and Nain proved the instance of the above theorem for failures semantics, with the aim to obtain an ω-completeness result for this semantics; their proof is rather delicate. To the best of our knowledge, failures semantics has so far been the only semantics in the spectrum for which the above result has been published. In our paper, we provide a proof of the above-mentioned property for all of the other semantics in the linear time-branching time spectrum. Despite the naturalness of the statement, which appears obvious, these proofs are far from trivial (at least for yours truly), and quite technical. I myself was really surprised by the amount of work we needed to do to prove such an "obvious" statement. (In case you wonder, the "obvious" statement is false in general. Consider, for instance, an algebra with carrier {0,1} and where the sum of any two elements is 1. Then the inequation y+x <= z+x holds, but y <= z obviously does not.)
I hope that some of the readers of this blog will find the paper worth reading. The techniques used in the proof of the cancellation theorem may also have some independent interest.
No comments:
Post a Comment