Benjamin Lion | arXiv Science

arXiv2022

A Formal Framework for Distributed Cyber-Physical Systems

Composition is an important feature of a specification language, as it enables the design of a complex system in terms of a product of its parts. Decomposition is equally important in order to reason about structural properties of a system. Usually, however, a system can be decomposed in more than one way, each optimizing for a different set of criteria. We extend an algebraic component-based model for cyber-physical systems to reason about decomposition. In this model, components compose using a family of algebraic products, and decompose, under some conditions, given a corresponding family of division operators. We use division to specify invariant of a system of components, and to model desirable updates. We apply our framework to design a cyber-physical system consisting of robots moving on a shared field, and identify desirable updates using our division operator.

cs.LO↗

arXiv2022

A Rewriting Framework for Interacting Cyber-Physical Agents

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.

cs.LO↗

arXiv2022

Runtime Composition Of Systems of Interacting Cyber-Physical Components

We introduce a transition system based specification of cyber-physical systems whose semantics is compositional with respect to a family of algebraic products. We give sufficient conditions for execution of a product to be correctly implemented by a lazy expansion of the product construction. The transition system algebra is implemented in the Maude rewriting logic system, and we report a simple case study illustrating compositional specification.

cs.LO↗

arXiv2021

A Semantic Model for Interacting Cyber-Physical Systems

We propose a component-based semantic model for Cyber-Physical Systems (CPSs) wherein the notion of a component abstracts the internal details of both cyber and physical processes, to expose a uniform semantic model of their externally observable behaviors expressed as sets of sequences of observations. We introduce algebraic operations on such sequences to model different kinds of component composition. These composition operators yield the externally observable behavior of their resulting composite components through specifications of interactions of the behaviors of their constituent components, as they, e.g., synchronize with or mutually exclude each other's alternative behaviors. Our framework is expressive enough to allow articulation of properties that coordinate desired interactions among composed components within the framework, also as component behavior. We demonstrate the usefulness of our formalism through examples of coordination properties in a CPS consisting of two robots interacting through shared physical resources.

cs.SE↗

arXiv2021

A Semantic Model for Interacting Cyber-Physical Systems

We propose a component-based semantic model for Cyber-Physical Systems (CPSs) wherein the notion of a component abstracts the internal details of both cyber and physical processes, to expose a uniform semantic model of their externally observable behaviors expressed as sets of sequences of observations. We introduce algebraic operations on such sequences to model different kinds of component composition. These composition operators yield the externally observable behavior of their resulting composite components through specifications of interactions of the behaviors of their constituent components, as they, e.g., synchronize with or mutually exclude each other's alternative behaviors. Our framework is expressive enough to allow articulation of properties that coordinate desired interactions among composed components within the framework, also as component behavior. We demonstrate the usefulness of our formalism through examples of coordination properties in a CPS consisting of two robots interacting through shared physical resources.

eess.SY↗

arXiv2016

Central loops in random planar graphs

Random planar graphs appear in a variety of context and it is important for many different applications to be able to characterize their structure. Local quantities fail to give interesting information and it seems that path-related measures are able to convey relevant information about the organization of these structures. In particular, nodes with a large betweenness centrality (BC) display non-trivial patterns, such as central loops. We first discuss empirical results for different random planar graphs and we then propose a toy model which allows us to discuss the condition for the emergence of non-trivial patterns such as central loops. This toy model is made of a star network with $N_b$ branches of size $n$ and links of weight $1$, superimposed to a loop at distance $\ell$ from the center and with links of weight $w$. We estimate for this model the BC at the center and on the loop and we show that the loop can be more central than the origin if $w<w_c$ where the threshold of this transition scales as $w_c\sim n/N_b$. In this regime, there is an optimal position of the loop that scales as $\ell_{opt}\sim N_b w/4$. This simple model sheds some light on the organization of these random structures and allows us to discuss the effect of randomness on the centrality of loops. In particular, it suggests that the number and the spatial extension of radial branches are the crucial ingredients that control the existence of central loops.

physics.soc-ph↗