By the same authors

Analysing RoboChart with probabilities

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Full text download(s)

Published copy (DOI)



Publication details

Title of host publicationFormal Methods
DateAccepted/In press - 28 Aug 2018
DateE-pub ahead of print (current) - 24 Oct 2018
Number of pages17
EditorsTiago Massoni, Mohammad Reza Mousavi
Original languageEnglish
ISBN (Print)9783030030438

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11254 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


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.

Bibliographical note

© Springer Nature Switzerland AG 2018

    Research areas

  • CSP, PRISM, Probabilistic analysis, Robotic systems



Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations