| 講演抄録/キーワード |
| 講演名 |
2026-03-04 09:40
Inclusion problem with single clock timed automaton revisted ○Mizuhito Ogawa(OTN)・Shoji Yuen(Nagoya U.) SS2025-56 |
| 抄録 |
(和) |
This presentation revisits the paper "Decision probelm for the verification of real-time software" (HSCC 2006), which claims the decidablity of the language inclusion between timed pushdown automaton and 1-clock timed automaton as an extension of the paper "On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap" (LICS 2004). Unfortunately, the proof of the decidability in HSCC 2006 paper has a serious glitch on an application of Higman's lemma. We give an alternative proof based on the bisimulation with the system with finite contorol states and P-automaton techniques |
| (英) |
This presentation revisits the paper "Decision probelm for the verification of real-time software" (HSCC 2006), which claims the decidablity of the language inclusion between timed pushdown automaton and 1-clock timed automaton as an extension of the paper "On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap" (LICS 2004). Unfortunately, the proof of the decidability in HSCC 2006 paper has a serious glitch on an application of Higman's lemma. We give an alternative proof based on the bisimulation with the system with finite contorol states and P-automaton techniques. |
| キーワード |
(和) |
/ / / / / / / |
| (英) |
Language inclusion problem / Timed automaton / Timed pushdown automaton / P-automaton / Decidability / / / |
| 文献情報 |
信学技報, vol. 125, no. 376, SS2025-56, pp. 157-162, 2026年3月. |
| 資料番号 |
SS2025-56 |
| 発行日 |
2026-02-23 (SS) |
| ISSN |
Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
| PDFダウンロード |
SS2025-56 |