A Rewriting Framework for Interacting Cyber-Physical Agents

TL;DR

This paper introduces a rewrite-based framework for modeling and analyzing cyber-physical systems, enabling modular, executable specifications that support compositional reasoning about interactions and emergent behaviors.

Contribution

It presents a novel rewrite system approach for specifying CPS components, ensuring semantics are compositional and demonstrating practical application with robot coordination in Maude.

Findings

Framework effectively models robot coordination protocols

Semantic compositionality is maintained in the rewrite system

Practical implementation in Maude validates the approach

Abstract

The analysis of cyber-physical systems (CPS) is challenging due to the large state space and the continuous changes occurring in their constituent parts. Design practices favor modularity to help reducing this complexity. In a previous work, we proposed a discrete semantic model for CPS that captures both cyber and physical aspects as streams of discrete observations, which ultimately form the behavior of a component. This semantic model is denotational and compositional, where each composition operator algebraically models an interaction between a pair of components. In this paper, we propose a specification of components as rewrite systems. The specification is operational and executable, and we study conditions for its semantics as components to be compositional. We demonstrate our framework by modeling a coordination of robots moving on a shared field. We show that our system of robots can be coordinated by a protocol in order to exhibit a desired emerging behavior. We use an implementation of our framework in Maude to give practical results.