Observations on the Decidability of Transitions

Consider a multiple-agent transition system such that, for some basic types T1,…,Tn, the state of any agent can be represented as an element of the Cartesian product T1×…×Tn. The system evolves by means of global steps. During such a step, new agents may be created and some existing agents may be updated or removed, but the total number of created, updated and removed agents is uniformly bounded. We show that, under appropriate conditions, there is an algorithm for deciding assume-guarantee properties of one-step computations. The result can be used for automatic invariant verification as well as for finite state approximation of the system in the context of test-case generation from AsmL specifications.