IEICE Trans - Symbolic Reachability Analysis of Probabilistic Linear Hybrid Automata

Symbolic Reachability Analysis of Probabilistic Linear Hybrid Automata

Yosuke MUTSUDA
Takaaki KATO
Satoshi YAMANE

Publication
IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E88-A    No.11    pp.2972-2981
Publication Date: 2005/11/01
Online ISSN: 
DOI: 10.1093/ietfec/e88-a.11.2972
Print ISSN: 0916-8508
Type of Manuscript: Special Section PAPER (Special Section on Concurrent/Hybrid Systems: Theory and Applications)
Category: 
Keyword: 
verification,  performance evaluation,  formal specification,  probabilistic hybrid automata,  reachability,  symbolic methods,  

Full Text: PDF(641.7KB)>>
Buy this Article


Summary: 
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.

open access publishing via