Application Conditions for Reactive Systems with Applications to Bisimulation Theory

摘要

This paper presents generalized application conditions (GACs), a newformalism for nested application conditions. GACs are not only suitable for DPOrewriting, but for rewriting in reactive systems as well. The main theorem states thatit is possible to construct an equivalent reactive system rule with a GAC for a DPOrule with application conditions under very mild conditions. The resulting reactivesystem rules live in the cospan category of the category C, in which the DPO ruleslive.It turns out that these GACs for reactive systems provide a slightly more powerfulway to control the application of a rewriting rule, than it is possible in the originalDPO setting.At the end, we give a short outlook on the applications of this formalism to the fieldof bisimulation theory, sketch our latest results and discuss future work.