Minimizing fuzzy Kripke models to simplify logical reasoning tasks
Minimizing fuzzy Kripke models over residuated lattices
Data Structures and Algorithms
Summary
Smaller models can make complex logical reasoning easier, but shrinking them without losing important details is hard. This paper studies how to reduce fuzzy Kripke models—mathematical structures used in fuzzy logic—while keeping key properties intact. The authors show that under certain conditions, the smallest equivalent model can be found using a specific type of bisimulation. They also provide the first algorithm to create minimal models preserving local information in some fuzzy logic cases.
What this means in practice
- •For formal verification engineers: Produce smaller fuzzy models that keep essential logical properties for faster automated verification of complex systems.
- •For software architects: Design optimized fuzzy logic models in dynamic systems modeling to reduce computational resources while maintaining accuracy.
A theory result. No direct application yet.
Authors
Linh Anh Nguyen
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.