  Transition systems are often used to describe the behaviour of software
systems. If viewed as a graph then, at their most basic level, vertices
correspond to the states of a program and each edge represents a transition
between states via the (atomic) action labelled. In this setting, systems are
thought to be consistent so that at each state formulas are evaluated as either
True or False.
  On the other hand, when a structure of this sort - for example a map where
states represent locations, some local properties are known and labelled
transitions represent information available about different routes - is built
resorting to multiple sources of information, it is common to find inconsistent
or incomplete information regarding what holds at each state, both at the level
of propositional variables and transitions.
  This paper aims at bringing together Belnap's four values, Dynamic Logic and
hybrid machinery such as nominals and the satisfaction operator, so that
reasoning is still possible in face of contradicting evidence. Proof-theory for
this new logic is explored by means of a terminating, sound and complete
tableaux system.
