Abstract Machines Notation (AMN) is the notation of the B method for
specifying systems and it is supported by tools providing editing,
navigating, animating and proving facilities. AMN permits us to state
invariance properties, based on safety conditions, but there are
applications, such as telecom services, where fairness and liveness
properties must also be considered. We define a way to extend the B
method expressivity by defining a semantics over traces, in the same
spirit as the temporal logic of actions does and we provide a
semantical framework for defining a extended B method that can exploit
the B environments facilities.