arXiv preprint ·
Minimizing fuzzy Kripke models over residuated lattices
- Published
- Source
- arXiv preprint, posted before peer review
- Original
- Read it at arXiv
- Topics
Abstract
Model minimization is a fundamental problem in formal methods, as smaller models can substantially reduce the complexity of model analysis and reasoning while preserving relevant semantic properties. This work studies the minimization of finite fuzzy Kripke models over residuated lattices while preserving global or local assertions in fuzzy modal logics, which are either fuzzy propositional dynamic logic or a restriction thereof, optionally enriched with nominals, converse modalities, and/or the universal program constructor. We prove that, whenever the multiplication operator of the underlying residuated lattice is right-continuous, the quotient model induced by the greatest fuzzy auto-bisimulation is a minimal reduction preserving global assertions. If the underlying fuzzy modal logic includes the universal program constructor, this quotient model is also a minimal reduction preserving local assertions and a minimal fuzzy Kripke model bisimilar to the original model. In the case where the universal program constructor is absent and the multiplication operator is additionally strictly monotone with respect to~1, we present the first algorithm for constructing a minimal reduction preserving local assertions; the resulting model is also a minimal bisimilar model.
The authors’ abstract, as arXiv lists it. arXiv’s listings, abstracts included, are free for anyone to reuse.
Read it on ReadSearch
Each opens after you create an account, and brings you back to this paper.
More in Data Structures & Algorithms
Improved classical optimization of fermionic Hamiltonians beyond Gaussian states
Faster Deterministic Approximation for Counting Knapsack
Conditional Indexing Lower Bounds and Normalization Boundaries for Elastic Subsequence Matching
The Matching Number Characterizes the Query Complexity of Edge Counting and Degree Moment Estimation
Subset Sum and Integer Programming Feasibility Test in Near-Optimal Time
Get the few papers worth your time in Data Structures & Algorithms every morning.
ReadSearch reads the new papers in your field each day and brings you the few worth reading, each with its key finding in a sentence.