Approximate bisimulation and discretization of hybrid CSP
From MaRDI portal
Publication:2281663
DOI10.1007/978-3-319-48989-6_43zbMATH Open1427.68218arXiv1609.00091OpenAlexW2963576416MaRDI QIDQ2281663FDOQ2281663
Shu-Ling Wang, Naijun Zhan, Li Jiao, Yangjia Li, Gaogao Yan
Publication date: 3 January 2020
Abstract: Hybrid Communicating Sequential Processes (HCSP) is a powerful formal modeling language for hybrid systems, which is an extension of CSP by introducing differential equations for modeling continuous evolution and interrupts for modeling interaction between continuous and discrete dynamics. In this paper, we investigate the semantic foundation for HCSP from an operational point of view by proposing notion of approximate bisimulation, which provides an appropriate criterion to characterize the equivalence between HCSP processes with continuous and discrete behaviour. We give an algorithm to determine whether two HCSP processes are approximately bisimilar. In addition, based on that, we propose an approach on how to discretize HCSP, i.e., given an HCSP process A, we construct another HCSP process B which does not contain any continuous dynamics such that A and B are approximately bisimilar with given precisions. This provides a rigorous way to transform a verified control model to a correct program model, which fills the gap in the design of embedded systems.
Full work available at URL: https://arxiv.org/abs/1609.00091
Hybrid systems of ordinary differential equations (34A38) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Cited In (2)
This page was built for publication: Approximate bisimulation and discretization of hybrid CSP
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2281663)
