  Interactive systems with registers and voices (shortly, "rv-systems") are a
model for interactive computing obtained closing register machines with respect
to a space-time duality transformation ("voices" are the time-dual counterparts
of "registers"). In the same vain, AGAPIA v0.1, a structured programming
language for rv-systems, is the space-time dual closure of classical while
programs (over a specific type of data). Typical AGAPIA programs describe open
processes located at various sites and having their temporal windows of
adequate reaction to the environment. The language naturally supports process
migration, structured interaction, and deployment of components on
heterogeneous machines.
  In this paper a sound Hoare-like spatio-temporal logic for the verification
of AGAPIA v0.1 programs is introduced. As a case study, a formal verification
proof of a popular distributed termination detection protocol is presented.

Programming Languages;Logic in Computer Science