A New Approach for Showing Termination of Parameterized Transition Systems
摘要
We investigate the termination problem of regular transition systems, i.e., of transition systems whose transition relations can be represented by finite-state automata. Leveraging this automata-theoretical perspective, we propose a new, efficient approach to termination analysis. Our method encodes termination arguments, called statements, as words in an auxiliary language, enabling the verification of whether configurations satisfy those termination arguments via an interpretation automaton. The choice of a fixed interpretation automaton enables the synthesis of new automata dedicated to searching for statements and verifying properties within any given regular transition system. The central contribution of this work is the construction of a specialized finite-state automaton that recognizes statements ensuring the system’s termination according to predefined conditions. Depending on the fragment of regular transitions considered, we define two sets of sufficient conditions for termination and provide an automata-based method to verify them within a given regular transition system.