A Process Algebra With Qualitative Calculus for Modeling Spatio-Temporal Behaviour

Distributive real-time autonomous systems like cyber-physical systems (CPS) and biology systems have become a hot topic nowadays. The high-level design of these systems shares a common characteristic that the behavior of agents is always space-related: i.e., agents are involved in an environment where the space relations between agents count. Agents are always sensitive to the discrete change of space relations among them at explicit time. We call such behavior the spatio-temporal behavior, which has become a critical research point recently. In this paper, we propose a process algebra called Communicating Sequential Process with Qualitative calculus (QCSP) as a formal language for modeling the spatio-temporal behavior. The key feature of our algebra is that it can reason about the space relations between agents by a finite set of binary relations that obey certain mathematical conditions - a qualitative calculus. In QCSP, each agent is confined in a space region. The space region (with an agent in it) can move as a whole and interact with other space regions. The topological structure of space regions forms the outer environment of agents, and the agents react timely according to their environment from time to time. We built our calculi by conservatively extending Timed CSP with qualitative calculus embedded in it, and illustrate how QCSP can be used to model the spatio-temporal behavior by analyzing three examples. We propose a special process algebra as a formal model for behavior that is sensitive to qualitative changing space and time. The key feature of our algebra is that it can reason about the relative location between agents by using qualitative calculus. Each agent is confined in a space region. The space region can move as a whole along with the agent confined in it and interact with other space regions. The behavior of agent depends on the interaction of space regions at an explicit time, shown by that certain actions can be triggered (or allowed) under certain space region relations and time condition. Such spatio-temporal behavior is a critical research point in nowadays distributive real-time autonomous systems like CPS or intelligent transportation systems (ITS). We propose our calculi by conservatively extending Timed CSP with qualitative calculus embedded in it to capture space region relations among agents.