In the setting of the modal logic that characterizes modal refinement over modal transition systems, Boudol and Larsen showed that the formulae for which model checking can be reduced to preorder checking, that is, the characteristic formulae, are exactly the consistent and prime ones. This paper presents general, sufficient conditions guaranteeing that characteristic formulae are exactly the consistent and prime ones. It is shown that the given conditions apply to various behavioural relations in the literature. In particular, characteristic formulae are exactly the prime and consistent ones for all the semantics in van Glabbeek's linear time-branching time spectrum.

When are prime formulae characteristic?

Dario Della Monica;
2019-01-01

Abstract

In the setting of the modal logic that characterizes modal refinement over modal transition systems, Boudol and Larsen showed that the formulae for which model checking can be reduced to preorder checking, that is, the characteristic formulae, are exactly the consistent and prime ones. This paper presents general, sufficient conditions guaranteeing that characteristic formulae are exactly the consistent and prime ones. It is shown that the given conditions apply to various behavioural relations in the literature. In particular, characteristic formulae are exactly the prime and consistent ones for all the semantics in van Glabbeek's linear time-branching time spectrum.
File in questo prodotto:
File Dimensione Formato  
tcs19_editor.pdf

non disponibili

Tipologia: Versione Editoriale (PDF)
Licenza: Non pubblico
Dimensione 825.58 kB
Formato Adobe PDF
825.58 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
tcs19_post.pdf

Open Access dal 20/07/2021

Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 617.09 kB
Formato Adobe PDF
617.09 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/11390/1143313
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 2
social impact