LDPChecker - A model checking tool for real-time and hybrid system

Yu Pei, Xuandong Li, Guoliang Zheng

Research output: Journal article publicationJournal articleAcademic researchpeer-review


Hybrid systems are real-time systems that allow both continuous state changes over time periods of positive durations and discrete state changes in zero time. Being an important subclass of hybrid systems, linear hybrid systems are usually modeled using linear hybrid automata. Linear hybrid automata are undecidable in general, but for a subclass of linear hybrid automata called positive loop-closed automata, the satisfaction problem for linear duration properties can be solved by linear programming. To support automatic checking of linear hybrid automata for linear duration properties, a tool named LDPChecker implementing the checking algorithm has been developed. The tool LDPChecker can identify positive loop-closed automaton and perform checking on it. Its key features include its ability to check real-time and hybrid system for many real-time properties including reachability property, and to generate diagnostic information automatically.
Original languageEnglish
Pages (from-to)38-46
Number of pages9
JournalJisuanji Yanjiu yu Fazhan/Computer Research and Development
Issue number1
Publication statusPublished - 1 Jan 2005
Externally publishedYes


  • Hybrid automata
  • Linear duration property
  • Model checking
  • Real-time and hybrid system

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture
  • Computer Networks and Communications


Dive into the research topics of 'LDPChecker - A model checking tool for real-time and hybrid system'. Together they form a unique fingerprint.

Cite this