• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International Symposium on Automated Technology for Verification and Analysis(ATVA 2005); 20051004-07; Taibei(CT) >Algorithmic Algebraic Model Checking II: Decidability of Semi-algebraic Model Checking and Its Applications to Systems Biology
【24h】

Algorithmic Algebraic Model Checking II: Decidability of Semi-algebraic Model Checking and Its Applications to Systems Biology

机译：算法代数模型检查II：半代数模型检查的可确定性及其在系统生物学中的应用

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Motivated by applications to systems biology, and the emergence of semi-algebraic hybrid systems as a natural framework for modeling biochemical networks, we continue exploring the decidability problem for model-checking with TCTL (Timed Computation Tree Logic) over this broad class of semi-algebraic hybrid systems. Previously, we had introduced these models, demonstrated the close connection to the goals of systems biology. However, we had only developed the techniques for bounded reachability, arguing for the adequacy of such an approach in a majority of the biological applications. Here, we present a semi-decidable symbolic algebraic dense-time TCTL model checking algorithm, which satisfies two desirable properties: it can be derived automatically from the symbolic description, and it extends to and generalizes other versions of temporal logics. The main mathematical device at the core of this approach is Tarski-Collins' real quantifier elimination employed at each fixpoint iteration, whose high complexity is the crux of its unfortunate limitation. Along with these results, we prove the undecidability of this problem in the more powerful "real" Turing machine formalism of Blum, Shub and Smale. We then demonstrate a preliminary version of our model-checker Tolque on the Delta-Notch example.
机译：受系统生物学应用的启发以及半代数混合系统作为生化网络建模的自然框架的出现，我们继续探索在TCTL（定时计算树逻辑）上进行模型检查的可判定性问题。代数混合系统。以前，我们已经介绍了这些模型，展示了与系统生物学目标的紧密联系。但是，我们只开发了有限可达性的技术，并认为这种方法在大多数生物学应用中是否足够。在这里，我们提出了一种半可确定的符号代数密集时间TCTL模型检查算法，该算法满足两个理想的属性：它可以从符号描述中自动得出，并且可以扩展和推广时间逻辑的其他版本。该方法核心的主要数学装置是在每个定点迭代中使用的Tarski-Collins的真正量词消除，其高复杂度是其不幸的局限性的症结所在。连同这些结果，我们在Blum，Shub和Smale更强大的“真实”图灵机形式主义中证明了该问题的不确定性。然后，我们在Delta-Notch示例中演示我们的模型检查器Tolque的初步版本。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号