Structures for Reachability Problems of Multirate Hybrid Systems

Hai Bin Zhang; Li Ya Yang

doi:10.4028/www.scientific.net/AMR.466-467.754

Paper Titles

Optimization Analysis for Radial Support by Finite Elements Method
p.734

Research on Suspension System Based on Radial-Basis Function Algorithm
p.739

Analysis on Static Stiffness of Synchronization Torsion Bar Based on Finite Element Method
p.744

Control System Design and Implementation of a Quadrotor Unmanned Aerial Vehicle
p.749

Structures for Reachability Problems of Multirate Hybrid Systems
p.754

Design of Power Quality Analyzer Based on Labwindows/CVI
p.759

Towards an Accurate Control of Circulating Fluidized Bed Combustor
p.763

Analysis of Force Mechanism and Reinforcement Effect of Leading High Pressure Grouting Ductule Basing on Numerical Simulation
p.768

The System of Spindle Optimization Design Based on GA
p.773

HomeAdvanced Materials ResearchAdvanced Materials Research Vols. 466-467Structures for Reachability Problems of Multirate...

Structures for Reachability Problems of Multirate Hybrid Systems

Abstract:

This paper investigates symbolic reachability issue of multirate hybrid systems. To this end, a constraint system called multirate zone is formalized for the representation and manipulation of multirate automata. To represent multirate zones, a data structure difference bound matrix for multirate zones is defined. In addition, to handle unions of multirate zones and data sharing, a BDD-like data structure multirate hybrid diagram is also defined. These enable us to do symbolic reachability analysis of multirate automata in an efficient way.

You might also be interested in these eBooks

View Preview

Info:

Periodical:

Advanced Materials Research (Volumes 466-467)

Pages:

754-758

DOI:

https://doi.org/10.4028/www.scientific.net/AMR.466-467.754

Citation:

Cite this paper

Online since:

February 2012

Authors:

Hai Bin Zhang, Li Ya Yang

Keywords:

Hybrid System, Multi-Rate Automata, Reachability Analysis

Export:

RIS, BibTeX

Price:

Permissions CCC:

Request Permissions

Permissions PLS:

Request Permissions

Сopyright:

Citation:

References

[1] Haibin Zhang and Zhenhua Duan. Symbolic Algorithmic Analysis of Rectangular Hybrid Systems. Journal of Computer Science and Technology, 24(3): 531-543 (2009).

Google Scholar

[2] Haibin Zhang and Zhenhua Duan. Symbolic Reachability Analysis of Hybrid Systems. Journal of Software, 19(12): 3111-3121 (2008).

DOI: 10.3724/sp.j.1001.2008.03111

Google Scholar

[3] Haibin Zhang, Zhenhua Duan, Bohu Huang, Xiaobing Wang and Long Zhang. Model Checking Rectangular Hybrid Systems With Timed Computation Tree Logic. TASE'10, pp.126-131 (2010).

DOI: 10.1109/tase.2010.18

Google Scholar

[4] R. Alur, T.A. Henzinger, G. Lafferriere and G.J. Pappas. Discrete Abstractions of Hybrid Systems. Proceedings of the IEEE, 88(7): 971-984 (2000).

DOI: 10.1109/5.871304

Google Scholar

[5] T.A. Henzinger, P. -H. Ho and H. Wong-Toi. HyTech: a model checker for hybrid systems. Software Tools for Technology Transfer, 1: 110-122 (1997).

DOI: 10.1007/s100090050008

Google Scholar

[6] D.L. Dill. Timing Assumptions and Verification of Finite-State Concurrent Systems. AVMFSS'1989. LNCS 1990, pp.197-212 (1989).

DOI: 10.1007/3-540-52148-8_17

Google Scholar

[7] F. Wang. Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-Like Data-Structures. CAV'2004, LNCS 3114, pp.295-307 (2004).

DOI: 10.1007/978-3-540-27813-9_23

Google Scholar

[8] G. Behrmann1, K.G. Larsen, J. Pearson, C. Weise and W. Yi. Efficient Timed Reachability Analysis Using Clock Diffierence Diagrams. CAV'99, LNCS 1633, pp.341-353 (1999).

DOI: 10.1007/3-540-48683-6_30

Google Scholar

[9] T.A. Henzinger, P.W. Kopke, Anuj Puri and Pravin Varaiya. What's Decidable About Hybrid Automata? Journal of Computer and System Sciences. 57: 94-124 (1998).

DOI: 10.1006/jcss.1998.1581

Google Scholar