Observational logics and true concurrency

We introduce two observational logics for reasoning about Distributed Transition Systems (DTS). These logics characterize different classes of properties of DTS compurations. The first logic, LD, 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, LP, has as a distinctive feature a past operator which appears to be crucial for adequately describing the interplay of concurrency and nondeterminism. A deeper understanding of Lp is gained by showing that it induces On DTS the same identification of another observational semantics.