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...

• Type: Conference
• Year: 2004
• Where: ASM
• Authors: Yuri Gurevich, Rostislav Yavorskiy
• Keywords: ASM 2004, Automatic Invariant Verification, Basic file Attributes, Microbiology, finite State Approximation