We denote a sequence of identifiers with and . As a convention, we use
for constants
and for variables of an abstract or a concrete machine respectively
and for parameters of an abstract or concrete machine respectively
for axioms
and for the invariants of the abstract machines or concrete machine respectively
and for the guards of the abstract events or concrete event respectively