A Unified Model for Real-Time Systems: Symbolic Techniques and Implementation
arxiv(2023)
摘要
In this paper, we consider a model of generalized timed automata (GTA) with
two kinds of clocks, history and future, that can express many timed features
succinctly, including timed automata, event-clock automata with and without
diagonal constraints, and automata with timers. Our main contribution is a new
simulation-based zone algorithm for checking reachability in this unified
model. While such algorithms are known to exist for timed automata, and have
recently been shown for event-clock automata without diagonal constraints, this
is the first result that can handle event-clock automata with diagonal
constraints and automata with timers. We also provide a prototype
implementation for our model and show experimental results on several
benchmarks. To the best of our knowledge, this is the first effective
implementation not just for our unified model, but even just for automata with
timers or for event-clock automata (with predicting clocks) without going
through a costly translation via timed automata. Last but not least, beyond
being interesting in their own right, generalized timed automata can be used
for model-checking event-clock specifications over timed automata models.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要