@article{oai:kanazawa-u.repo.nii.ac.jp:00007823,
 author = {Mutsuda, Yosuke and Kato, Takaaki and Yamane, Satoshi},
 issue = {11},
 journal = {IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences},
 month = {Nov},
 note = {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 Engineers, 金沢大学理工研究域電子情報学系},
 pages = {2972--2981},
 title = {Symbolic Reachability Analysis of Probabilistic Linear Hybrid Automata(<Special Section>Concurrent/Hybrid Systems : Theory and Applications)},
 volume = {E88-A},
 year = {2005}
}