Description and Reasoning about Hybrid System Based on Nonstandard Model

• NAKAMURA Katsunori

  Ritsumeikan University Heian Jogakuin (St.Agnes') School

• FUSAOKA Akira

  Ritsumeikan University

Bibliographic Information

Other Title

• 非標準モデルに基づくハイブリッドシステムの記述と推論について
• ヒヒョウジュン モデル ニ モトズク ハイブリッド システム ノ キジュツ ト スイロン ニ ツイテ

Abstract

In this paper, we introduce a nonstandard analysis into a logical modeling of continuous dynamics and present a new framework called hyper-finite hybrid automaton (HHA). HHA is a nonstandard interpretation of hybrid automata in the domain of *R. We also enlarge the linear temporal logic LTL to *LTL to describe the system specification. In this framework, we examine the validation of the system consistency of the hybrid system based on model checking, especially the existence and reachability of Zeno point.

Journal

• Transactions of the Institute of Systems, Control and Information Engineers

  Transactions of the Institute of Systems, Control and Information Engineers 21 (6), 176-184, 2008

  THE INSTITUTE OF SYSTEMS, CONTROL AND INFORMATION ENGINEERS (ISCIE)

Keywords

• linear temporal logic
• nonstandard analysis
• hybrid system

Details

• CRID: 1390282680142999808
• NII Article ID: 10021064575
• NII Book ID: AN1013280X
• DOI: 10.5687/iscie.21.176
• ISSN: 2185811X
• ISSN: 13425668
• NDL BIB ID: 9526257
• Web Site: https://ndlsearch.ndl.go.jp/books/R000000004-I9526257
• Text Lang: ja
• Data Source:
  • JaLC
  • NDL
  • Crossref
  • CiNii Articles
• Abstract License Flag: Disallowed