Published online by Cambridge University Press: 08 January 2010
BISIMULATION AND TRACE SEMANTICS
So far, we only considered models having the property of containing a submodel which is isomorphic to the initial algebra of the current theory (for instance see 2.7.35). In other words we may say that if two finite processes in a model are equal, this equality must be derivable from the theory.
Models that with respect to finite processes correspond to the graph model or the term model are said to be models in bisimulation semantics. Because for every one of our theories, its initial model is a model in bisimulation semantics, our axiom systems are said to be a complete axiomatization of bisimulation semantics. In this chapter we will consider other semantics than bisimulation semantics, and we will present complete axiomatizations of these alternative semantics as well.
Because all operators except for + and · can be eliminated from closed terms, we will mainly restrict ourselves to the theory BPA, with special constant 8. The addition of the special constant τ leads to many interesting observations, and a vastly increased complexity. We do not include it here, in order to focus on a few key issues.
We will discuss semantics that identify more processes than bisimulation semantics does. The advantage of this is clear: calculations become easier, and more simplifications can be made. On the other hand, some differences between processes are disregarded, and as a consequence, in some cases some operators cannot be defined any more.
We start with the repetition of an earlier result.
To save this book to your Kindle, first ensure [email protected] is added to your Approved Personal Document E-mail List under your Personal Document Settings on the Manage Your Content and Devices page of your Amazon account. Then enter the ‘name’ part of your Kindle email address below. Find out more about saving to your Kindle.
Note you can select to save to either the @free.kindle.com or @kindle.com variations. ‘@free.kindle.com’ emails are free but can only be saved to your device when it is connected to wi-fi. ‘@kindle.com’ emails can be delivered even when you are not connected to wi-fi, but note that service fees apply.
Find out more about the Kindle Personal Document Service.
To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Dropbox.
To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Google Drive.