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-01-01
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.| File | Dimensione | Formato | |
|---|---|---|---|
|
2020_JLogAlgebraicMethodsProgram_112_Aceto.pdf
non disponibili
Tipologia:
Versione Editoriale (PDF)
Licenza:
Non pubblico
Dimensione
608.48 kB
Formato
Adobe PDF
|
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.
