Please use this identifier to cite or link to this item:
https://www.um.edu.mt/library/oar/handle/123456789/86057| 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. |
| URI: | https://www.um.edu.mt/library/oar/handle/123456789/86057 |
| Appears in Collections: | Scholarly Works - FacICTCS |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| The complexity of identifying characteristic formulae.pdf Restricted Access | 608.48 kB | Adobe PDF | View/Open Request a copy |
Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.