Probabilistic semantics for RoboChart. A weakest completion approach

DOI10.1007/978-3-030-31038-7_5MaRDI QIDQ2296286zbMATH OpenOpenAlexFDO

Authors Ana Cavalcanti, Simon Foster, Alexandre Mota, Kangfeng Ye, Jim Woodcock

Publication date 18 February 2020

Full work available at URL https://doi.org/10.1007/978-3-030-31038-7_5

zbMATH Keywords

relational calculusprobabilistic semanticsstatechartsrobotic controllersRoboChart languageUnifying Theories of Programming (UTP)weakest completion semantics

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Semantics of probabilistic programs: a weak limit approach
• scientific article; zbMATH DE number 1324652
• Probabilistic models for the guarded command language
• Symbolic semantics for probabilistic programs
• Metric Semantics and Full Abstractness for Action Refinement and Probabilistic Choice

Cited in

(5)

• Formally verified animation for RoboChart using interaction trees
• Automated reasoning for probabilistic sequential programs with theorem proving
• UTP, \textsf{\textit{Circus}}, and Isabelle
• A Unary Semigroup Trace Algebra
• Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving

This page was built for publication: Probabilistic semantics for RoboChart. A weakest completion approach

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2296286)