Symbolic Reachability Analysis of Probabilistic Linear Hybrid Automata(<Special Section>Concurrent/Hybrid Systems : Theory and Applications)

金沢大学理工研究域電子情報学系We can model embedded systems as hybrid systems. Moreover, they are distributed and real-time systems. Therefore, it is important to specify and verify randomness and soft real-time properties. For the purpose of system verification, we formally define probabilistic linear hybrid automaton and its symbolic reachability analysis method. It can describe uncertainties and soft real-time characteristics. Copyright © 2005 The Institute of Electronics, Information and Communication Engineer