Model Checking Multirate Hybrid Systems with Dense Timed Interval Temporal Logic

Hai Bin Zhang; Li Ya Yang

doi:10.4028/www.scientific.net/AMM.198-199.889

Paper Titles

Research on Comprehensive Planning and Statistics Index Model of Power Grid
p.871

Empirical Analysis on Regression Model Based on Time Series and Cross Section Data of Hot-Rolled Coil Price
p.876

A New Model of Tourism Space Carrying Capacity
p.880

Contagion Effect Analysis of Financial Crisis in Soybean Futures Markets Based on Copula Functions
p.885

Model Checking Multirate Hybrid Systems with Dense Timed Interval Temporal Logic
p.889

Analytical Solution for the Subsurface Flow Wetland Model
p.894

Research on Semantic Business Process Model in Logistics Distribution Field
p.899

Research on Warship Maintenance Support Simulation System Based on the Method of Equipment Maintenance Support Simulation Experiment
p.905

Application Specific Architecture Template Reuse for SoC Transaction Level Modeling
p.911

HomeApplied Mechanics and MaterialsApplied Mechanics and Materials Vols. 198-199Model Checking Multirate Hybrid Systems with Dense...

Model Checking Multirate Hybrid Systems with Dense Timed Interval Temporal Logic

Abstract:

This paper investigates the model checking issue of multirate hybrid systems. To this end, multirate automata are used to represent the possible behavior of multirate hybrid systems, and a dense timed interval temporal logic (DTITL) is defined to describe the desirable property. To check whether a multirate automaton satisfies a DTITL formula, a corresponding region automaton and a propositional interval temporal logic (PITL) formula are constructed. After each vertex of the region automaton being labeled with propositions appearing in the corresponding PITL formula, the model checking problem for mutirate hybrid systems is reduced to the same issue for PITL, which can be solved readily.

You might also be interested in these eBooks

Applied Mechanics, Mechatronics Automation & System Simulation

View Preview

Info:

Periodical:

Applied Mechanics and Materials (Volumes 198-199)

Pages:

889-893

DOI:

https://doi.org/10.4028/www.scientific.net/AMM.198-199.889

Citation:

Cite this paper

Online since:

September 2012

Authors:

Hai Bin Zhang, Li Ya Yang

Keywords:

Hybrid System, Interval Temporal Logic, Model Checking

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] 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

[3] B. Moskowski. Executing Temporal Logic. Cambridge University Press (1986).

Google Scholar

[4] M. Muller-Olm, D. Schmidt and B. Ateffen. Model-checking: a tutorial introduction, LNCS 1694, pp.330-354 (1999).

Google Scholar

[5] 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

[6] A. Kapur, T. A. Henzinger, Z. Manna and A. Pnueli. Proving safety properties of hybrid systems, FTRTFT' 94, LNCS 863, p.431–454 (1994).

DOI: 10.1007/3-540-58468-4_177

Google Scholar

[7] 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