Infinite State Systems: Verification and Automatic Checking

Title: Infinite State Systems: Verification and Automatic Checking

Abstract: This research focuses on the automatic verification of infinite state systems, a common feature in software systems that handle data from infinite domains or have unbounded control structures. The study examines various formalisms, including Context Free Processes, Pushdown Automata, Petri Nets, and Process Algebras. It explores decidability results for certain classes of properties about infinite derivations, particularly those related to linear time logic. The research introduces an automaton-based formalism that allows for both recursion and multi-threading, providing a meaningful example of the results. The main implication of this work is that it offers a framework for automatic checking of certain classes of infinite state systems, potentially simplifying the verification process for complex software systems.

Main Research Question: How can we automatically verify and check properties of infinite state systems, particularly those involving recursion and multi-threading?

Methodology: The research employs the framework of Process Rewrite Systems (PRSs), a formal setting that subsumes many common infinite state models. It focuses on a meaningful automaton-based formalism that allows for both recursion and multi-threading, which can be encoded into PRSs. The study investigates decidability results for certain classes of properties about infinite derivations, particularly those related to linear time logic.

Results: The research establishes decidability results for a class of properties about infinite derivations in a meaningful automaton-based formalism. This allows for automatic checking of certain classes of infinite state systems, particularly those involving recursion and multi-threading.

Implications: The main implication of this work is that it offers a framework for automatic checking of certain classes of infinite state systems, potentially simplifying the verification process for complex software systems. Additionally, the research contributes to the ongoing development of formal methods for verifying and checking properties of infinite state systems.

Link to Article: https://arxiv.org/abs/0312019v1 Authors: arXiv ID: 0312019v1