Constraint-based and automata-based representations for the modeling of hybrid systems
-
- HATA Kunihiro
- Waseda University
-
- UEDA Kazunori
- Waseda University
Bibliographic Information
- Other Title
-
- ハイブリッドシステムのモデリングにおける制約表現とオートマトン表現
Abstract
<p>Hybrid systems are systems that involve both continuous and discrete changes,which can express dynamical systems, circuits, control systems, and so on. Hybrid automata (HA)are mainly used for modeling hybrid systems, and model checking methods based on themhave been well-studied. However, there are some non-trivial points in expressing hybridsystems as hybrid automata precisely.HydLa is a hybrid systems modeling language that enables us to write systems' specificationsconcisely using constraint programming and constraint hierarchy. A declarative semantics is given for HydLa, and bounded model checking is featured by its implementation. On the other hand, in order to check properties that hold after an unbounded number of discrete changes, it is necessary to extend the existing definition of HydLa's hybrid trajectories.In this paper, we defined HydLa HA in order to verify models written in a subset of HydLa in an existing framework of hybrid automata. In the definition, open intervals are adoptedfor time structure in hybrid trajectory, whereas closed intervals are adopted in generalhybrid automata. We examined the definition by some examples.</p>
Journal
-
- Proceedings of the Annual Conference of JSAI
-
Proceedings of the Annual Conference of JSAI JSAI2023 (0), 2I5OS9b05-2I5OS9b05, 2023
The Japanese Society for Artificial Intelligence
- Tweet
Details 詳細情報について
-
- CRID
- 1390296808221192960
-
- ISSN
- 27587347
-
- Text Lang
- ja
-
- Data Source
-
- JaLC
-
- Abstract License Flag
- Disallowed