Observational logics and true concurrency

We introduce two observational logics lor reasoning about Distributed Transition Systems (DTS). These logics characterize different classes of properties of DTS computations. The first logic, L?D, is a straightforward generalization of Hennessy-Milner Logic obtained by allowing modalities indexed by partial ordering observations; it is in full agreement with a computationally defined observational equivalence for true concurrency. The second logic, L?p, has as a distinctive feature a past operator which appears co be crucial for adequately describing the interplay of concurrency and nondeterminism. A deeper understanding of L?p is gained by showing that it induces on DTS the same identification of another observational semantics.