×

zbMATH — the first resource for mathematics

Liveness verification of reversal-bounded multicounter machines with a free counter. (English) Zbl 1053.03021
Hariharan, Ramesh (ed.) et al., FST TCS 2001: Foundations of software technology and theoretical computer science. 21st conference, Bangalore, India, December 13–15, 2001. Proceedings. Berlin: Springer (ISBN 3-540-43002-4). Lect. Notes Comput. Sci. 2245, 132-143 (2001).
Summary: We investigate the Presburger liveness problems for nondeterministic reversal-bounded multicounter machines with a free counter (NCMFs). We show the following:
(i) The \(\exists\)-Presburger-i.o. problem and the \(\exists\)-Presburger-eventual problem are both decidable. So are their duals, the \(\forall\)-Presburger-almost-always problem and the \(\forall\)-Presburger-always problem.
(ii) The \(\forall\)-Presburger-i.o. problem and the \(\forall\)-Presburger-eventual problem are both undecidable. So are their duals, the \(\exists\)-Presburger-almost-always problem and the \(\exists\)-Presburger-always problem.
These results can be used to formulate a weak form of Presburger linear temporal logic and develop its model-checking theories for NCMFs. They can also be combined with the results of Z. Dang, P. San Pietro and R. A. Kemmerer [Lect. Notes Comput. Sci. 2010, 132–143 (2001; Zbl 0981.68715)] to study the same set of liveness problems on an extended form of discrete timed automata containing, besides clocks, a number of reversal-bounded counters and a free counter.
For the entire collection see [Zbl 0977.00041].

MSC:
03D05 Automata and formal grammars in connection with logical questions
03B25 Decidability of theories and sets of sentences
68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
03B44 Temporal logic
PDF BibTeX XML Cite
Full Text: Link