Please use this identifier to cite or link to this item:
Title: The complexity of identifying characteristic formulae
Authors: Aceto, Luca
Achilleos, Antonis
Francalanza, Adrian
Ingólfsdóttir, Anna
Keywords: Modality (Logic)
Recursive functions -- Data processing
Computer logic
Computational complexity
Characteristic functions
Issue Date: 2020
Publisher: Elsevier
Citation: Aceto, L., Achilleos, A., Francalanza, A., & Ingólfsdóttir, A. (2020). The complexity of identifying characteristic formulae. Journal of Logical and Algebraic Methods in Programming, 112, 100529.
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.
Appears in Collections:Scholarly Works - FacICTCS

Files in This Item:
File Description SizeFormat 
The complexity of identifying characteristic formulae.pdf
  Restricted Access
608.48 kBAdobe PDFView/Open Request a copy

Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.