Probabilistic semantics for RoboChart. A weakest completion approach

DOI10.1007/978-3-030-31038-7_5OpenAlexW2973326731MaRDI QIDQ2296286FDOQ2296286

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

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

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)

Cited In (5)

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

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)