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.
2018
Proceedings of the 19th Italian Conference on Theoretical Computer Science
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11577/3275243
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact