Application Conditions for Reactive Systems with Applications to Bisimulation Theory

Abstract

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