# Liveness Verification of Reversal-Bounded Multicounter Machines with a Free Counter

## Abstract

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 [12] 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.

## Keywords

Model Check Mode Vector Disjunctive Normal Form Reachability Problem Time Automaton## Preview

Unable to display preview. Download preview PDF.

## References

- 1.R. Alur and D. Dill, “The theory of timed automata,”
*TCS*, 126(2):183–236, 1994zbMATHCrossRefMathSciNetGoogle Scholar - 2.P. Abdulla and B. Jonsson, “Verifying programs with unreliable channels,”
*Information and Computation*, 127(2): 91–101, 1996zbMATHCrossRefMathSciNetGoogle Scholar - 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 - 15.O. H. Ibarra, “Reversal-bounded multicounter machines and their decision problems,”
*J.ACM*,**25**(1978) 116–133zbMATHCrossRefMathSciNetGoogle 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
- 21.W. Peng and S. Purushothaman. “Analysis of a Class of Communicating Finite State Machines,”
*Acta Informatica*, 29(6/7): 499–522, 1992zbMATHCrossRefMathSciNetGoogle Scholar - 22.W. Pugh, “TheOmega test: a fast and practical integer programming algorithm for dependence analysis,”
*Communications of the ACM*, 35(8): 102–114, 1992CrossRefGoogle Scholar