Symbolic Reachability Analysis of Probabilistic Linear Hybrid Automata

Yosuke MUTSUDA; Takaaki KATO; Satoshi YAMANE

doi:10.1093/ietfec/e88-a.11.2972

Symbolic Reachability Analysis of Probabilistic Linear Hybrid Automata

Yosuke MUTSUDA, Takaaki KATO, Satoshi YAMANE

Full Text Views

0

Share
Cite this

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.

Publication: IEICE TRANSACTIONS on Fundamentals Vol.E88-A No.11 pp.2972-2981

Publication Date: 2005/11/01

Publicized

Online ISSN

DOI: 10.1093/ietfec/e88-a.11.2972

Type of Manuscript: Special Section PAPER (Special Section on Concurrent/Hybrid Systems: Theory and Applications)

Category

Cite this

Copy

Yosuke MUTSUDA, Takaaki KATO, Satoshi YAMANE, "Symbolic Reachability Analysis of Probabilistic Linear Hybrid Automata" in IEICE TRANSACTIONS on Fundamentals, vol. E88-A, no. 11, pp. 2972-2981, November 2005, doi: 10.1093/ietfec/e88-a.11.2972.
Abstract: 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.
URL: https://globals.ieice.org/en_transactions/fundamentals/10.1093/ietfec/e88-a.11.2972/_p

Copy

@ARTICLE{e88-a_11_2972,
author={Yosuke MUTSUDA, Takaaki KATO, Satoshi YAMANE, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Symbolic Reachability Analysis of Probabilistic Linear Hybrid Automata},
year={2005},
volume={E88-A},
number={11},
pages={2972-2981},
abstract={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.},
keywords={},
doi={10.1093/ietfec/e88-a.11.2972},
ISSN={},
month={November},}

Copy

TY - JOUR
TI - Symbolic Reachability Analysis of Probabilistic Linear Hybrid Automata
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 2972
EP - 2981
AU - Yosuke MUTSUDA
AU - Takaaki KATO
AU - Satoshi YAMANE
PY - 2005
DO - 10.1093/ietfec/e88-a.11.2972
JO - IEICE TRANSACTIONS on Fundamentals
SN -
VL - E88-A
IS - 11
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - November 2005
AB - 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.
ER -