  The high availability and scalability of weakly-consistent systems attracts
system designers. Yet, writing correct application code for this type of
systems is difficult; even how to specify the intended behavior of such systems
is still an open question. There has not been established any standard method
to specify the intended dynamic behavior of a weakly consistent system. There
exist specifications of various consistency models for distributed and
concurrent systems; and the semantics of replicated datatypes like CRDTs have
been specified in axiomatic and operational models based on visibility
relations.
  In this paper, we present a temporal logic, EPTL, that is tailored to specify
properties of weakly consistent systems. In contrast to LTL and CTL, EPTL takes
into account that operations of weakly consistent systems are in many cases not
serializable and have to be treated respectively to capture the behavior. We
embed our temporal logic in Isabelle/HOL and can thereby leverage strong
semi-automatic proving capabilities.
