On Reachability for Hybrid Automata over Bounded Time

被引:0
作者
Brihaye, Thomas [1 ]
Doyen, Laurent [2 ,3 ]
Geeraerts, Gilles [4 ]
Ouaknine, Joel [5 ]
Raskin, Jean-Francois [4 ]
Worrell, James [5 ]
机构
[1] Univ Mons, B-7000 Mons, Belgium
[2] ENS Cachan, LSV, Cachan, France
[3] CNRS, F-75700 Paris, France
[4] Univ Libre Bruxelles, Brussels, Belgium
[5] Univ Oxford, Comp Lab, Oxford OX1 2JD, England
来源
AUTOMATA, LANGUAGES AND PROGRAMMING, ICALP, PT II | 2011年 / 6756卷
基金
英国工程与自然科学研究理事会;
关键词
D O I
暂无
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
This paper investigates the time-bounded version of the reachability problem for hybrid automata. This problem asks whether a given hybrid automaton can reach a given target location within T time units, where T is a constant rational value. We show that, in contrast to the classical (unbounded) reachability problem, the timed-bounded version is decidable for rectangular hybrid automata provided only non-negative rates are allowed. This class of systems is of practical interest and subsumes, among others, the class of stopwatch automata. We also show that the problem becomes undecidable if either diagonal constraints or both negative and positive rates are allowed.
引用
收藏
页码:416 / 427
页数:12
相关论文
共 50 条
[41]   Approximate Parameter Synthesis for Probabilistic Time-Bounded Reachability [J].
Han, Tingting ;
Katoen, Joost-Pieter ;
Mereacre, Alexandru .
RTSS: 2008 REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS, 2008, :173-182
[42]   Approximate Time Bounded Reachability for CTMCs and CTMDPs: A Lyapunov Approach [J].
Salamati, Mahmoud ;
Soudjani, Sadegh ;
Majumdar, Rupak .
QUANTITATIVE EVALUATION OF SYSTEMS, QEST 2018, 2018, 11024 :389-406
[43]   Optimal Time-Bounded Reachability Analysis for Concurrent Systems [J].
Butkova, Yuliya ;
Fox, Gereon .
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT II, 2019, 11428 :191-208
[44]   Parameter Synthesis for Bounded Cost Reachability in Time Petri Nets [J].
Lime, Didier ;
Roux, Olivier H. ;
Seidner, Charlotte .
APPLICATION AND THEORY OF PETRI NETS AND CONCURRENCY, PETRI NETS 2019, 2019, 11522 :406-425
[45]   Efficient choice of parameters on delta-reachability bounded hybrid systems [J].
Alexandre Rocha, Eugenio Miguel ;
Murillo, Kelly Patricia .
ARCHIVES OF CONTROL SCIENCES, 2021, 31 (04) :781-794
[46]   On the complexity of bounded time and precision reachability for piecewise affine systems [J].
Bazille, Hugo ;
Bournez, Olivier ;
Gomaa, Walid ;
Pouly, Amaury .
THEORETICAL COMPUTER SCIENCE, 2018, 735 :132-146
[47]   A Lyapunov Approach for Time-Bounded Reachability of CTMCs and CTMDPs [J].
Salamati, Mahmoud ;
Soudjani, Sadegh ;
Majumdar, Rupak .
ACM TRANSACTIONS ON MODELING AND PERFORMANCE EVALUATION OF COMPUTING SYSTEMS, 2020, 5 (01)
[48]   BACH 2: Bounded ReachAbility CHecker for Compositional Linear Hybrid Systems [J].
Bu, Lei ;
Li, You ;
Wang, Linzhang ;
Chen, Xin ;
Li, Xuandong .
2010 DESIGN, AUTOMATION & TEST IN EUROPE (DATE 2010), 2010, :1512-1517
[49]   Revisiting Reachability in Timed Automata [J].
Quaas, Karin ;
Shirmohammadi, Mahsa ;
Worrell, James .
2017 32ND ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2017,
[50]   Reachability in Pushdown Register Automata [J].
Murawski, Andrzej S. ;
Ramsay, Steven J. ;
Tzevelekos, Nikos .
MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 2014, PT I, 2014, 8634 :464-+