A Two Step Perspective for Kripke Structure Reduction

2012/10/01 by Arpit Sharma, Sharma, Arpit
Computer Science · Engineering · #Advanced Memory and Neural Computing #Cellular Automata and Applications #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Logic in Computer Science (cs.LO) #Quantum-Dot Cellular Automata

paper · pdf · doi:10.48550/arxiv.1210.0408

openalex publication_date 2012/10/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

This paper presents a novel theoretical framework for the state space reduction of Kripke structures. We define two equivalence relations, Kripke minimization equivalence (KME) and weak Kripke minimization equivalence (WKME). We define the quotient system under these relations and show that these relations are strictly coarser than strong (bi)simulation and divergence-sensitive stutter (bi)simulation, respectively. We prove that the quotient system obtained under KME and WKME preserves linear-time and stutter-insensitive linear-time properties. Finally, we show that KME is compositional w.r.t. synchronous parallel composition.

Related

• An Efficient Simulation Algorithm on Kripke Structures
• Results on Embeddings Between State-Based and Event-Based Systems
• Generalizing the Paige-Tarjan Algorithm by Abstract Interpretation
• An O(m log n) Algorithm for Stuttering Equivalence and Branching\n Bisimulation
• An n log n Alogrithm for Deterministic Kripke Structure Minimization