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.

doi.org/10.1007/978-3-031-19759-8_22
Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence
Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning. ISoLA 2022
Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands

Lion, B., Arbab, F., & Talcott, C. (2022). A rewriting framework for interacting cyber-physical agents. In International Symposium on Leveraging Applications of Formal Methods (pp. 356–372). doi:10.1007/978-3-031-19759-8_22