Decidable Properties for Monadic Abstract State Machines.

The paper describes a decidable class of verification problems expressed in first order timed logic. To specify programs we use Abstract State Machines. It is known that Abstract State Machines and first order timed logic are two very powerful formalisms apt to represent verification problems for timed distributed systems. However, the general verification problem represented in this way is undecidable. Prior, some decidable classes of verification problems were described in semantical properties that are in their turn undecidable. The decidable class of the present paper is described in syntactical terms. Though it admits no functions, only predicates, it is of practical interest and we give an example illustrating possible applications.