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.
Relating some logics for true concurrency
Padoan, Tommaso
2018
Abstract
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.Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.