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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

A New Approach for Showing Termination of Parameterized Transition Systems

  • Roland Herrmann,
  • Philipp Rümmer

摘要

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.