MODELING COMMUNICATION PROTOCOLS FOR CLIENT-SERVER NETWORKS: MODEL CHECKING DYNAMICAL SYSTEMS

摘要

Certain class of communication protocols is well modeled by dynamical systems on torus-like spaces. If m agents/processes communicate/cooperate in a system then it can be modeled by a dynamical system on m-dimensional torus-like space. No mathematical machinery is known for analysis of these models for m>3. In this paper we suggest a method of investigation of certain properties of these systems using their symbolic dynamics. We construct a marked graph such that all symbolic trajectories of dynamical system under consideration are runs on the marked graph. Therefore, we show that some properties of a dynamic system can be proved as follows: formulate a property in a language of temporal logic (or program logic); model check this formula in the constructed marked graph using it as a Kripke structure.