Refinement Checking for Multirate Hybrid ZIA
Logic in Computer Science
2014-10-15 v1 Formal Languages and Automata Theory
Abstract
A hybrid system is a dynamical system with both discrete and continuous components. In order to study the modeling and verification aspects of hybrid system, in this paper we first introduce a specification approach combining interface automata, initialized multirate hybrid automata and Z language, which is named MZIA. Meanwhile we propose a refinement relation on MZIAs. Then we give an algorithm for checking refinement relation between MZIAs with finite domain and demonstrate the correctness of the algorithm.
Cite
@article{arxiv.1410.3773,
title = {Refinement Checking for Multirate Hybrid ZIA},
author = {Guozheng Li and Zining Cao and Zheng Gao},
journal= {arXiv preprint arXiv:1410.3773},
year = {2014}
}
Comments
11pages, 3figures