Relating some logics for true concurrency

We study some logics for true concurrency recently defined by several authors to characterise a number of known or meaningful behavioural equivalences, with special interest in history-preserving bisimilarity. All the considered logics are event-based, naturally interpreted over event structures or any formalism which can be given a causal semantics, like Petri nets. Operators of incomparable expressiveness from different logics can be combined into a single logic, more powerful than the original ones. Since the event structure associated with a system is typically infinite (even if the system is finite state), already the known decidability results of model-checking in the original logics are non-trivial. Here we show, using a tableaux-based approach, that the model-checking problem for the new logic is still decidable over a class of event structures satisfying a suitable regularity condition, referred to as strong regularity.