##
Modular Semantics for Open Transition Rules with Negative Premises

### Martin Churchill

Transition rules with negative premises are needed in the structural
operational semantics of programming and specification constructs
such as priority and interrupt, as well as in timed extensions of
specification languages. The well-known proof-theoretic semantics
for transition system specifications involving such rules is
based on well-supported proofs for closed transitions. Dealing with
open formulae by considering all closed instances is inherently
non-modular -- proofs are not necessarily preserved by disjoint
extensions of the transition system specification.

Here, we conservatively extend the notion of well-supported proof to
open transition rules. We prove that the resulting semantics is
modular, consistent, and closed under instantiation. Our results
provide the foundations for modular notions of bisimulation such
that equivalence can be proved with reference only to the relevant
rules, without appealing to all existing closed instantiations of
terms.