×

zbMATH — the first resource for mathematics

Positive loop-closed automata: A decidable class of hybrid systems. (English) Zbl 1008.68070
Summary: The model-checking problem for real-time and hybrid systems is very difficult, even for a well-formed class of hybrid systems – the class of linear hybrid automata – the problem is still undecidable in general. So an important question for the analysis and design of real-time and hybrid systems is the identification of subclasses of such systems and corresponding restricted classes of analysis problems that can be settled algorithmically. In this paper, we show that for a class of linear hybrid automata called positive loop-closed automata, the satisfaction problem for linear duration properties can be solved by linear programming. We extend the traditional regular expressions with duration constraints and use them as a language to describe the behaviour of this class of linear hybrid automata. The extended notation is called duration-constrained regular expressions. Based on this formalism, we show that the model-checking problem can be reduced formally to linear programs.

MSC:
68Q45 Formal languages and automata
Software:
HyTech
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Chaochen, Zhou; Hoare, C.A.R.; Ravn, A.P., A calculus of durations, Information processing letter, 40, 5, 269-276, (1991) · Zbl 0743.68097
[2] Henzinger, T.A., The theory of hybrid automata, (), 278-292 · Zbl 0959.68073
[3] Alur, R.; Courcoubetis, C.; Halbwachs, N.; Henzinger, T.A.; Ho, P.-H.; Nicollin, X.; Olivero, A.; Sifakis, J.; Yovine, S., The algorithmic analysis of hybrid systems, Theoretical computer science, 138, 3-34, (1995) · Zbl 0874.68206
[4] Chaochen, Zhou; Jinzhong, Zhang; Lu, Yang; Xiaoshan, Li, Linear duration invariants, (), 88-109
[5] Kesten, Y.; Pnueli, A.; Sifakis, J.; Yovine, S., Decidable integration graphs, Information and computation, 150, 2, 209-243, (1999) · Zbl 1045.68566
[6] T.A. Henzinger, P.W. Kopke, Anuj Puri, Pravin Varaiya, What’s decidable about hybrid automata? Journal of Computer and System Sciences 57 (1998) 94-124 · Zbl 0920.68091
[7] Henzinger, T.A.; Majumdar, Rupak, Symbolic model checking for rectangular hybrid systems, () · Zbl 0960.68117
[8] Henzinger, T.A.; Ho, P.-H.; Wong-Toi, H., HYTECH: a model checker for hybrid systems, Software tools for technology transfer, 1, 110-122, (1997) · Zbl 1060.68603
[9] Alur, R.; Courcoubetis, C.; Henzinger, T.A., Computing accumulated delays in real-time systmes, (), 181-193
[10] Alur, R.; David, D., A theory of timed automata, Theoretical computer science, 126, 183-235, (1994) · Zbl 0803.68071
[11] Henzinger, T.A.; Ho, P.-H.; Wong-Toi, H., Algorithmic analysis of nonlinear hybrid systems, IEEE transactions on automatic control, 43, 540-554, (1998) · Zbl 0918.93019
[12] Henzinger, T.A.; Rusu, Vlad, Reachability verification for hybrid automata, (), 190-204
[13] Halbwachs, N.; Proy, Y.-E.; Raymond, P., Verification of linear hybrid systems by means of convex approximations, ()
[14] Avrunin, G.S.; Corbett, J.C.; Dillon, L.K., Analyzing partially-implemented real-time systems, IEEE transactions on software engineering, 24, 8, 602-614, (1998)
[15] Asarin, E.; Caspi, P.; Maler, O., A Kleene theorem for timed automata, (), 160-171
[16] Jianhua, Z.; Hung, D.V., On checking parallel real-time systems for linear duration properties, (), 241-250
[17] Z. Jianhua, D. Van Hung, Checking timed automata for some discretisable duration properties, Research Report 145, UNU/IIST, Macau, 1998
[18] Xuandong, L.; Yu, P.; Jianhua, Z.; Yong, L.; Tao, Z.; Guoliang, Z., Efficient verification of a class of linear hybrid automata using linear programming, (), 465-479 · Zbl 1002.68506
[19] Xuandong, L.; Hung, D.Van; Tao, Z., Checking hybrid automata for linear duration invariants, (), 166-180
[20] Xuandong, L.; Tao, Z.; Jianmin, H.; Jianhua, Z.; Guoliang, Z., Hybrid regular expressions, (), 384-399
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.