Timed Automata And The Theory Of Real Numbers
CONCUR '99: Proceedings of the 10th International Conference on Concurrency Theory(1999)
摘要
A configuration of a timed automaton is given by a control state and finitely many clock (real) values. We show here that the binary reachability relation between configurations of a timed automaton is definable in an additive theory of real numbers, which is decidable. This result implies the decidability of model checking for some properties which cannot be expressed in timed temporal logics and provide with alternative proofs of some known decidable properties. Our proof relies on two intermediate results: 1. Every timed automaton can be effectively emulated by a timed automaton which does not contain nested. loops. 2. The binary reachability relation for counter automata without nested loops (called here flat automata) is expressible in the additive theory of integers (resp. real numbers). The second result carl be derived from [10].
更多查看译文
关键词
Model Check, Real Time System, Temporal Logic, Transition Sequence, Nest Loop
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络