Coalgebraic reasoning with global assumptions in arithmetic modal logics
Kupke, Clemens and Pattinson, Dirk and Schröder, Lutz (2022) Coalgebraic reasoning with global assumptions in arithmetic modal logics. ACM Transactions on Computational Logic, 23 (2). pp. 1-34. 11. ISSN 1557-945X (https://doi.org/10.1145/3501300)
Preview |
Text.
Filename: Kupke_etal_ACM_TCL_2022_Coalgebraic_reasoning_with_global_assumptions.pdf
Accepted Author Manuscript License: Strathprints license 1.0 Download (1MB)| Preview |
Abstract
We establish a generic upper bound ExpTime for reasoning with global assumptions (also known as TBoxes) in coalgebraic modal logics. Unlike earlier results of this kind, our bound does not require a tractable set of tableau rules for the instance logics, so that the result applies to wider classes of logics. Examples are Presburger modal logic, which extends graded modal logic with linear inequalities over numbers of successors, and probabilistic modal logic with polynomial inequalities over probabilities. We establish the theoretical upper bound using a type elimination algorithm. We also provide a global caching algorithm that potentially avoids building the entire exponential-sized space of candidate states, and thus offers a basis for practical reasoning. This algorithm still involves frequent fixpoint computations; we show how these can be handled efficiently in a concrete algorithm modelled on Liu and Smolka’s linear-time fixpoint algorithm. Finally, we show that the upper complexity bound is preserved under adding nominals to the logic, i.e., in coalgebraic hybrid logic.
-
-
Item type: Article ID code: 81211 Dates: DateEvent30 April 2022Published14 January 2022Published Online1 November 2021AcceptedSubjects: Science > Mathematics > Electronic computers. Computer science Department: Faculty of Science > Computer and Information Sciences Depositing user: Pure Administrator Date deposited: 21 Jun 2022 10:45 Last modified: 25 Sep 2024 00:47 Related URLs: URI: https://strathprints.strath.ac.uk/id/eprint/81211