Observations on the Decidability of Transitions

10 years 1 months ago
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. 1 Motivating example Consider the following simplified model of a file system (a real world file system that the authors were exposed to). Basic information about a file is collected in the File class. For simplicity, we include in the model only very basic fil...
Yuri Gurevich, Rostislav Yavorskiy
Added 30 Jun 2010
Updated 30 Jun 2010
Type Conference
Year 2004
Where ASM
Authors Yuri Gurevich, Rostislav Yavorskiy
Comments (0)