Decidable properties for monadic Abstract State Machines (ASMs)
<P>          Beauquier Daniele (Univ. Paris XII)
          
<P>
We consider a class of  Gurevich Abstract State Machines (ASM)
that work over a finite parametric domain and make assignments
only to unary predicates. We are interested in the decidability of
timed properties of such machines with inputs. We prove that if
the inputs are without parameters, i e. nullary dynamic
predicates, the properties expressed in a  two-sorted first-order
logic  (like safety, liveness with bounded waiting and others) are
decidable.