Relations and Its Applications

Title: Relations and Its Applications

Main Research Question: Can we find an efficient method to verify the liveness properties of generalized timed automata?

Methodology: The researchers used a unified framework to study liveness verification problems for generalized timed automata. They focused on mixed linear liveness problems and Presburger liveness problems.

Results: They proved that the mixed linear liveness problem for a timed automaton with dense clocks, reversal-bounded counters, and a free counter is decidable. They also showed that the Presburger liveness problem for a timed automaton with discrete clocks, reversal-bounded counters, and a pushdown stack is decidable.

Implications: These results open up new possibilities for automatic verification of real-time systems against complex timing requirements. They provide a more comprehensive approach to liveness verification problems, which can be applied to various real-world scenarios.

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