Symbolic Transition Systems: A Framework for Analyzing Infinite-State Systems

Title: Symbolic Transition Systems: A Framework for Analyzing Infinite-State Systems

Research Question: How can we analyze and verify the behavior of infinite-state systems in a finite and symbolic manner?

Methodology: The researchers introduced a framework called Symbolic Transition Systems (STS), which consists of a set of classes of systems with increasingly comprehensive state spaces. These classes are STS1, STS2, STS3, STS4, and STS5, each with specific properties that allow for symbolic analysis.

Results: The researchers provided examples from hybrid systems for four of these classes: STS1, STS2, STS3, and STS4. They showed that these classes can be analyzed symbolically by iterating certain operations and terminating when no new state sets are generated. This enables model checking of various temporal properties, such as linear temporal logic and reachability properties.

Implications: The STS framework provides a powerful tool for analyzing and verifying the behavior of infinite-state systems. It allows for symbolic analysis, which means that the state spaces can be represented and manipulated in a finite and symbolic manner. This makes it possible to check interesting, unbounded temporal properties of the systems, which is a significant advancement in the field of system verification.

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