
handle: 11588/752126 , 11562/989622 , 11383/2079048
Cyber-Physical Systems (CPSs) are integrations of distributed computing systems with physical processes via a networking with actuators and sensors, where feedback loops among the components allow the physical processes to affect the computations and vice versa. Although CPSs can be found in several complex and sometimes critical real-world domains, their verification and validation often relies on simulation-test systems rather then automatic methodologies to formally verify safety requirements. In this work, we prove the decidability of the reachability problem for discrete-time linear CPSs whose physical process in isolation has a periodic behavior, up to an initial transitory phase.
Formal safety verification; Linear cyber-physical systems; Reachability problem; Computer Science Applications1707 Computer Vision and Pattern Recognition; Computer Networks and Communications; Control and Systems Engineering; Electrical and Electronic Engineering, Model checking, Safety verification, Cyber-physical system
Formal safety verification; Linear cyber-physical systems; Reachability problem; Computer Science Applications1707 Computer Vision and Pattern Recognition; Computer Networks and Communications; Control and Systems Engineering; Electrical and Electronic Engineering, Model checking, Safety verification, Cyber-physical system
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 3 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
