Decidable Properties for Monadic Abstract State Machines
by
Daniele Beauquier
University Paris 12, FRANCE

We are interested in the problem of verification of time properties for distributed systems.There are a lot of different tools to be used for modeling distributed systems, and among them are Abstract State Machines (ASMs). They provide a formal method for clear design and specification of distributed dynamic systems. On the other hand, the specification of time properties to verify implies also the choice of an appropriate logic. In previous works, we exhibited a first order timed logic (FOTL) and a class of formulas of this logic for which the validity problem is decidable. Formulas of this class have the form f ® g, where f represents the set of runs of the system under consideration and g is a time property to be verified by the system. Moreover f and g are submited to respective semantical restrictions. These restrictions when they are satisfied imply that if the formula f ® g admits a counter-model, then it admits a counter-model of a finite fixed "complexity", and this last property is proved to be decidable.

In this paper, our goal is to provide syntactical sufficient conditions for ASMs on one hand and syntactical sufficient conditions for formulas which express the time property to verify on the other hand, to get a decidable class of verification problems. We give an example of application of our result to the well-known problem of verification "the Watchdog Timer".

Date received: March 31, 2003