Satisfiability of Modal Inclusion Logic: Lax and Strict Semantics
Lauri Hella, Antti Kuusisto, Arne Meier, Heribert Vollmer
TL;DR
This paper analyzes the computational complexity of satisfiability in modal inclusion logic, revealing EXPTIME-completeness generally and NEXPTIME-completeness for certain structures under strict semantics.
Contribution
It distinguishes between lax and strict semantics, providing complexity classifications and showing NEXPTIME-completeness for specific structures.
Findings
Both variants are EXPTIME-complete on general structures.
NEXPTIME-completeness achieved for certain structures under strict semantics.
Complexity depends on the class of structures and semantics used.
Abstract
We investigate the computational complexity of the satisfiability problem of modal inclusion logic. We distinguish two variants of the problem: one for the strict and another one for the lax semantics. Both problems turn out to be EXPTIME-complete on general structures. Finally, we show how for a specific class of structures NEXPTIME-completeness for these problems under strict semantics can be achieved.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Formal Methods in Verification · Logic, programming, and type systems