We introduce the completeness problem for Modal Logic (possibly with fixpoint operators) and examine its complexity. A formula is called complete, if any two satisfying processes are bisimilar. The completeness problem is closely connected to the characterization problem, which asks whether a given formula characterizes a given process up to bisimulation equivalence. We discover that completeness, characterization, and validity have the same complexity — with some exceptions for which there are, in general, no complete formulae. To prove our upper bounds, we present a non-deterministic procedure with an oracle for validity that combines tableaux and a test for bisimilarity, and determines whether a formula is complete.

The complexity of identifying characteristic formulae

Luca Aceto;
2020

Abstract

We introduce the completeness problem for Modal Logic (possibly with fixpoint operators) and examine its complexity. A formula is called complete, if any two satisfying processes are bisimilar. The completeness problem is closely connected to the characterization problem, which asks whether a given formula characterizes a given process up to bisimulation equivalence. We discover that completeness, characterization, and validity have the same complexity — with some exceptions for which there are, in general, no complete formulae. To prove our upper bounds, we present a non-deterministic procedure with an oracle for validity that combines tableaux and a test for bisimilarity, and determines whether a formula is complete.
Modal logic, μ-calculus, Hennessy-Milner logic with recursion, Completeness, Characteristic formulae, Computational complexity
File in questo prodotto:
File Dimensione Formato  
2020_JLogAlgebraicMethodsProgram_112_Aceto.pdf

non disponibili

Licenza: Non pubblico
608.48 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

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: http://hdl.handle.net/20.500.12571/14368
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact