Robotic systems have applications in many real-life scenarios, ranging from household cleaning to critical operations. RoboChart is a graphical language for describing robotic controllers designed specifically for autonomous and mobile robots, providing architectural constructs to identify the requirements for a robotic platform. It also provides a formal semantics in CSP. RoboChart has a probabilistic operator (P) but no associated probabilistic CSP semantics. When (P) is used, currently a non-deterministic choice (Π) is used as semantics; this is a conservative semantics but it does not allow the analysis of stochastic properties. In this paper we define the semantics of the operator in terms of the probabilistic CSP operator ⊞. We also show how this augmented CSP semantics for RoboChart can be translated into the PRISM probabilistic language to be able to check stochastic properties.
CITATION STYLE
Conserva Filho, M. S., Marinho, R., Mota, A., & Woodcock, J. (2018). Analysing RoboChart with probabilities. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11254 LNCS, pp. 198–214). Springer Verlag. https://doi.org/10.1007/978-3-030-03044-5_13
Mendeley helps you to discover research relevant for your work.