Event Identifier Logic

摘要

In this paper we introduce Event Identifier Logic (EIL), which extends Hennessy–Milnerrnlogic by the addition of:rn(1) reverse as well as forward modalities; andrn(2) identifiers to keep track of events.rnWe show that this logic corresponds to hereditary history-preserving (HH) bisimulationrnequivalence within a particular true-concurrency model, namely, stable configurationrnstructures. We also show how natural sublogics of EIL correspond to coarser equivalences.rnIn particular, we provide logical characterisations of weak-history- preserving (WH) andrnhistory-preserving (H) bisimulation. Logics corresponding to HH and H bisimulation havernbeen given previously, but none, as far as we are aware, corresponding to WH bisimulationrn(when autoconcurrency is allowed). We also present characteristic formulas that characterisernindividual structures with respect to history-preserving equivalences.