Decidability and Complexity Issues for OneCounter Machines
Antonin Kucera
Masaryk University Brno
(Visiting Faron Moller for one week.)
Abstract
Onecounter machines can be seen as an idealized model for finitestate
programs operating on a single unbounded variable. We present an overview
of recent results related to the problem of formal verification of reactive
systems defined in the syntax of onecounter machines. More specifically, we
consider the problem of equivalencechecking (wrt bisimilarity and simulation
equivalence) and the modelchecking problem for branchingtime logics (EF,
mucalculus). It turns out that a very important feature of onecounter
systems which often determines the decidability/tractability border for the
mentioned problems is the ability to test the counter for zero. We also
consider `weak' onecounter machines which cannot test for zero explicitly
(this model is computationally equivalent to Petri nets with at most one
unbounded place) and show that this weakening indeed brings more decidability
and tractability.
The presentation is based on several papers which appeared in the last five
years, including some very recent ones. The aim is to present the results
themselves together with some notes on proof techniques, without going into
technicalities.
Place: Information technology, Uppsala University
Room: 1510
Time: 13.1514.00 (+ discussions)
Room 1510 is in Building 1, Floor 5, room 10
(in the southern part of the building).
Help on how to find ASTEC Seminars.
There will be an extended period for discussions after the seminar.
Speakers are encouraged to give an short (5 min) introduction to the subject at the begining of the talk.
Listeners are excused if they have to leave after 14.00.
Everyone is welcome !
Updated 16Feb2001 09:20 by Roland Grönroos
email: info at astec.uu.se
Location: http://www.astec.uu.se/Seminars/01/0227.shtml
