Formal modeling and performance evaluation for hybrid systems:a probabilistic hybrid process algebra-based approach

2020/12/23 by Fujun Wang, Wang, Fujun, Zining Cao +5
Computer Science · #F.4.3 #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Logic in Computer Science (cs.LO) #cs.FL #cs.LO

paper · pdf · doi:10.48550/arxiv.2012.12716

arxiv created 2020/12/23 · arxiv updated 2021/01/04

Abstract

Probabilistic behavior is omnipresent in computer controlled systems, in particular, so-called safety-critical hybrid systems, because of various reasons, like uncertain environments, or fundamental properties of nature. In this paper, we extend existing hybrid process algebra ACP_hs^srt with probability without replacing nondeterministic choice operator. In view of some shortcomings in existing approximate probabilistic bisimulation, we relax the constrains and propose a novel approximate probabilistic bisimulation relation. After that, we present a performance evaluation language, CTRML, to reason over probabilistic systems, which extend the results to real number. Along with the specification language, we present a set of algorithms for the evaluation of the language. Additionally, we transfer the hybrid process algebra to probabilistic transition system and show experimental results.

Related

• Extending Hybrid CSP with Probability and Stochasticity
• Stochastic Formal Methods for Hybrid Systems
• ProbReach: Verified Probabilistic Delta-Reachability for Stochastic Hybrid Systems
• A Uniform Approach to Random Process Model
• A Probabilistic Calculus of Cyber-Physical Systems