Liveness Verification of Reversal-Bounded Multicounter Machines with a Free Counter
We investigate the Presburger liveness problems for nondeterministic reversal-bounded multicounter machines with a free counter (NCMFs). We show the following: - The ∃-Presburger-i.o. problem and the ∃-Presburger-eventual problem are both decidable. So are their duals, the ∀-Presburger-almost-always problem and the ∀-Presburger-always problem. - The ∀-Presburger-i.o. problem and the ∀-Presburger-eventual problem are both undecidable. So are their duals, the ∃-Presburger-almost-always problem and the ∃-Presburger-always problem.
These results can be used to formulate a weak form of Presburger linear temporal logic and developits model-checking theories for NCMFs. They can also be combined with  to study the same set of liveness problems on an extended form of discrete timed automata containing, besides clocks, a number of reversalbounded counters and a free counter.
KeywordsModel Check Mode Vector Disjunctive Normal Form Reachability Problem Time Automaton
Unable to display preview. Download preview PDF.
- 3.A. Bouajjani, J. Esparza, and O. Maler. “Reachability analysis of pushdown automata: application to model-Checking,” CONCUR’97, LNCS 1243, pp. 135–150Google Scholar
- 4.G. Cece and A. Finkel, “Programs with Quasi-Stable Channels are Effectively Recognizable,” CAV’97, LNCS 1254, pp. 304–315Google Scholar
- 5.H. Comon and Y. Jurski. “Multiple counters automata, safety analysis and Presburger arithmetic,” CAV’98, LNCS 1427, pp. 268–279Google Scholar
- 6.H. Comon and Y. Jurski, “Timed automata and the theory of real numbers,” CONCUR’99, LNCS 1664, pp. 242–257Google Scholar
- 7.Z. Dang, “Binary reachability analysis of timed pushdown automata with dense clocks,” CAV’01, LNCS 2102, pp. 506–517Google Scholar
- 8.Z. Dang, O. H. Ibarra, T. Bultan, R. A. Kemmerer and J. Su, “Binary Reachability Analysis of Discrete Pushdown Timed Automata,” CAV’00, LNCS 1855, pp. 69–84Google Scholar
- 9.Z. Dang, O. H. Ibarra and R. A. Kemmerer, “Decidable Approximations on Generalized and Parameterized Discrete Timed Automata,” COCOON’01, LNCS 2108, pp. 529–539Google Scholar
- 10.Z. Dang and R. A. Kemmerer, “Using the ASTRAL model checker to analyze Mobile IP,” Proceedings of the Twenty-first International Conference on Software Engineering (ICSE’99), pp. 132–141, IEEE Press, 1999Google Scholar
- 11.Z. Dang and R. A. Kemmerer, “Three approximation techniques forASTRALsymbolic model checking of infinite state real-time systems,” Proceedings of the Twenty-second International Conference on Software Engineering (ICSE’00), pp. 345–354, IEEE Press, 2000Google Scholar
- 12.Z. Dang, P. San Pietro, and R. A. Kemmerer, “On Presburger Liveness of Discrete Timed Automata,” STACS’01, LNCS 2010, pp. 132–143Google Scholar
- 13.A. Finkel and G. Sutre. “Decidability of Reachability Problems for Classes of Two Counter Automata,” STACS’00, LNCS 1770, pp. 346–357Google Scholar
- 14.A. Finkel, B. Willems, and P. Wolper. “A direct symbolic approach to model checking pushdown systems,” INFINITY’97 Google Scholar
- 16.O. H. Ibarra, “Reachability and safety in queue systems with counters and pushdown stack,” Proceedings of the International Conference on Implementation and Application of Automata, pp. 120–129, 2000Google Scholar
- 17.O. H. Ibarra, Z. Dang, and P. San Pietro, “Verification in Loosely Synchronous Queue-Connected Discrete Timed Automata,” submitted. 2001Google Scholar
- 18.O. H. Ibarra, J. Su, T. Bultan, Z. Dang, and R. A. Kemmerer, “Counter Machines: Decidable Properties and Applications to Verification Problems,”, MFCS’00, LNCS 1893, pp. 426–435Google Scholar
- 19.G. Kreisel and J. L. Krevine, “Elements of Mathematical Logic,” North-Holland, 1967Google Scholar
- 20.K. L. McMillan. “Symbolic model-checking-an approach to the state explosion problem,” PhD thesis, Department of Computer Science, Carnegie Mellon University, 1992Google Scholar