scholarly journals A spatio-temporal specification language and its completeness & decidability

2020 ◽  
Vol 9 (1) ◽  
Author(s):  
Tengfei Li ◽  
Jing Liu ◽  
Haiying Sun ◽  
Xiang Chen ◽  
Lipeng Zhang ◽  
...  
Keyword(s):  
Intelligent Transportation System ◽  
Cyber Physical Systems ◽  
Specification Language ◽  
Finite Model ◽  
Critical Systems ◽  
Physical Systems ◽  
Spatial Objects ◽  
Temporal Properties ◽  
Spatio Temporal ◽  
Temporal Specification

AbstractIn the past few years, significant progress has been made on spatio-temporal cyber-physical systems in achieving spatio-temporal properties on several long-standing tasks. With the broader specification of spatio-temporal properties on various applications, the concerns over their spatio-temporal logics have been raised in public, especially after the widely reported safety-critical systems involving self-driving cars, intelligent transportation system, image processing. In this paper, we present a spatio-temporal specification language, STSL PC, by combining Signal Temporal Logic (STL) with a spatial logic S4 u, to characterize spatio-temporal dynamic behaviors of cyber-physical systems. This language is highly expressive: it allows the description of quantitative signals, by expressing spatio-temporal traces over real valued signals in dense time, and Boolean signals, by constraining values of spatial objects across threshold predicates. STSL PC combines the power of temporal modalities and spatial operators, and enjoys important properties such as finite model property. We provide a Hilbert-style axiomatization for the proposed STSL PC and prove the soundness and completeness by the spatio-temporal extension of maximal consistent set and canonical model. Further, we demonstrate the decidability of STSL PC and analyze the complexity of STSL PC. Besides, we generalize STSL to the evolution of spatial objects over time, called STSL OC, and provide the proof of its axiomatization system and decidability.

scholarly journals A Logic for Monitoring Dynamic Networks of Spatially-distributed Cyber-Physical Systems

2022 ◽  
Vol Volume 18, Issue 1 ◽  
Author(s):  
L. Nenzi ◽  
E. Bartocci ◽  
L. Bortolussi ◽  
M. Loreti
Keyword(s):  
Ad Hoc ◽  
Dynamic Networks ◽  
Physical Space ◽  
Weighted Graph ◽  
Cyber Physical Systems ◽  
Dynamic Interactions ◽  
Physical Systems ◽  
Temporal Properties ◽  
Spatially Distributed ◽  
Spatio Temporal

Cyber-Physical Systems (CPS) consist of inter-wined computational (cyber) and physical components interacting through sensors and/or actuators. Computational elements are networked at every scale and can communicate with each other and with humans. Nodes can join and leave the network at any time or they can move to different spatial locations. In this scenario, monitoring spatial and temporal properties plays a key role in the understanding of how complex behaviors can emerge from local and dynamic interactions. We revisit here the Spatio-Temporal Reach and Escape Logic (STREL), a logic-based formal language designed to express and monitor spatio-temporal requirements over the execution of mobile and spatially distributed CPS. STREL considers the physical space in which CPS entities (nodes of the graph) are arranged as a weighted graph representing their dynamic topological configuration. Both nodes and edges include attributes modeling physical and logical quantities that can evolve over time. STREL combines the Signal Temporal Logic with two spatial modalities reach and escape that operate over the weighted graph. From these basic operators, we can derive other important spatial modalities such as everywhere, somewhere and surround. We propose both qualitative and quantitative semantics based on constraint semiring algebraic structure. We provide an offline monitoring algorithm for STREL and we show the feasibility of our approach with the application to two case studies: monitoring spatio-temporal requirements over a simulated mobile ad-hoc sensor network and a simulated epidemic spreading model for COVID19.

scholarly journals Deriving Specifications of Control Programs for Cyber Physical Systems

2019 ◽  
Vol 63 (5) ◽  
pp. 774-790
Author(s):  
Alan Burns ◽  
Ian J Hayes ◽  
Cliff B Jones
Keyword(s):  
Physical Environment ◽  
Control Program ◽  
Cyber Physical Systems ◽  
Physical Systems ◽  
Control Programs ◽  
Use Of Time ◽  
Temporal Properties ◽  
Physical Components

Abstract Cyber physical systems (CPS) exist in a physical environment and comprise both physical components and a control program. Physical components are inherently liable to failure and yet an overall CPS is required to operate safely, reliably and cost effectively. This paper proposes a framework for deriving the specification of the software control component of a CPS from an understanding of the behaviour required of the overall system in its physical environment. The two key elements of this framework are (i) an extension to the use of rely/guarantee conditions to allow specifications to be obtained systematically from requirements (as expressed in terms of the required behaviour in the environment) and nested assumptions (about the physical components of the CPS); and (ii) the use of time bands to record the temporal properties required of the CPS at a number of different granularities. The key contribution is in combining these ideas; using time bands overcomes a significant drawback in earlier work. The paper also addresses the means by which the reliability of a CPS can be addressed by challenging each rely condition in the derived specification and, where appropriate, improve robustness and/or define weaker guarantees that can be delivered with respect to the corresponding weaker rely conditions.

scholarly journals Interfacing the Skin

2016 ◽  
Author(s):  
Frank Melendez ◽  
◽  
Nancy Diniz ◽  
Keyword(s):  
Biological Systems ◽  
Cyber Physical Systems ◽  
Autonomous Robotics ◽  
Physical Systems ◽  
Ubiquitous Sensing ◽  
Temporal Relationships ◽  
Spatio Temporal ◽  
Complex Methods

Several technologies are converging to drastically change local and global spatio temporal relationships, including autonomous robotics, cyber-physical systems, ubiquitous sensing networks, and synthetic biological systems. These technologies provide architects and designers with opportunities to redefine models of human-machine-environment interactions that encompass more complex methods of simulated intelligence and nuanced response across a range of scales from the micro to the macro.

Reliability Method of Cyber-Physical Systems Based on Events Polling and Interrupt Control

2012 ◽  
Vol 562-564 ◽  
pp. 1562-1566
Author(s):  
Zhong Zheng ◽  
Gang Xie ◽  
Jing Wang
Keyword(s):  
Cyber Physical Systems ◽  
Reliability Problem ◽  
Physical Systems ◽  
Reliability Method ◽  
Event Model ◽  
Spatio Temporal

This paper proposed the reliability method of cyber-physical systems(CPS) based on events polling and interrupt control, discussed the reliability problem of CPS. According to the characteristic of polling principle and the CPS events model, proposed the polling principle of the CPS based on events. combined the method of the interrupt control, according to the spatio-temporal attributes of different events, set the different interrupt priority to solve the reliability problem of the CPS event model.

Sign in / Sign up

Export Citation Format

Share Document