Positive loop-closed automata: A decidable class of hybrid systems

Xuandong Li, Jianhua Zhao, Yu Pei, Yong Li, Tao Zheng, Guoliang Zheng

Research output: Journal article publicationJournal articleAcademic researchpeer-review

7 Citations (Scopus)

Abstract

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.
Original languageEnglish
Pages (from-to)79-108
Number of pages30
JournalJournal of Logic and Algebraic Programming
Volume52-53
DOIs
Publication statusPublished - 1 Jul 2002
Externally publishedYes

Keywords

  • Hybrid automata
  • Linear duration properties
  • Model checking
  • Real-time and hybrid systems

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Logic
  • Computational Theory and Mathematics

Cite this