This note shows that the trace simulation preorder does not have a finite inequational basis over the language BCCSP. Indeed, no collection of sound inequations of bounded depth is ground-complete with respect to the trace simulation preorder over BCCSP even over a singleton set of actions.

Trace Simulation Semantics is not Finitely Based over BCCSP

Aceto L;
2017

Abstract

This note shows that the trace simulation preorder does not have a finite inequational basis over the language BCCSP. Indeed, no collection of sound inequations of bounded depth is ground-complete with respect to the trace simulation preorder over BCCSP even over a singleton set of actions.
trace simulation preorder; complete axiomatizations; BCCSP
File in questo prodotto:
File Dimensione Formato  
2017_Acta Cybern_23_Aceto.pdf

accesso aperto

Tipologia: Versione Editoriale (PDF)
Licenza: Accesso gratuito
Dimensione 311.27 kB
Formato Adobe PDF
311.27 kB Adobe PDF Visualizza/Apri

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/20.500.12571/509
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact