首页    期刊浏览 2024年09月18日 星期三
登录注册

文章基本信息

  • 标题:Real-Time Model-Checking: Parameters everywhere
  • 本地全文:下载
  • 作者:Véronique Bruyère ; Jean-François Raskin
  • 期刊名称:Logical Methods in Computer Science
  • 印刷版ISSN:1860-5974
  • 电子版ISSN:1860-5974
  • 出版年度:2007
  • 卷号:3
  • 期号:01
  • DOI:10.2168/LMCS-3(1:7)2007
  • 出版社:Technical University of Braunschweig
  • 摘要:

    In this paper, we study the model-checking and parameter synthesis problems of the logic TCTL over discrete-timed automata where parameters are allowed both in the model (timed automaton) and in the property (temporal formula). Our results are as follows. On the negative side, we show that the model-checking problem of TCTL extended with parameters is undecidable over discrete-timed automata with only one parametric clock. The undecidability result needs equality in the logic. On the positive side, we show that the model-checking and the parameter synthesis problems become decidable for a fragment of the logic where equality is not allowed. Our method is based on automata theoretic principles and an extension of our method to express durations of runs in timed automata using Presburger arithmetic.

  • 关键词:Model-Checking;Parameters;Principles
国家哲学社会科学文献中心版权所有