Relations and Its Applications

Title: Relations and Its Applications

Abstract: This research article explores the existence of an ω-chain for transitive mixed linear relations and its implications for various liveness verification problems. It proposes an approach to verify real-time systems against complex timing requirements using a flattening technique and decidable binary reachability characterizations. The study also discusses the application of these techniques to timed automata augmented with discrete counters and pushdown stacks.

Main Research Question: Can we automatically verify the existence of an ω-chain for transitive mixed linear relations?

Methodology: The research uses a combination of mathematical logic, automata theory, and decision procedures. It employs a recent result of [23] to eliminate quantifiers from the relations and express them into mixed linear constraints. The transitivity of the relations is critical, and removing it from the relations makes the existence of an ω-chain undecidable.

Results: The main theorem proves that the existence of an ω-chain for transitive mixed linear relations is decidable. This result is applied to the binary reachability of timed automata and pushdown automata, providing a decidable answer to the liveness verification problems.

Implications: The research has significant implications for the automatic verification of real-time systems. It opens the door for verifying complex timing requirements and provides a decidable characterization for timed automata and their generalizations. The techniques can be applied to various real-time models, such as timed automata with dense and discrete clocks, and pushdown stacks. This can lead to more accurate and efficient verification of real-time systems, ultimately improving their reliability and safety.

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