• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Annual ACM/IEEE Symposium on Logic in Computer Science >First-order logic with reachability for infinite-state systems
【24h】

First-order logic with reachability for infinite-state systems

机译：具有无限状态系统可达性的一阶逻辑

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

First-order logic with the reachability predicate (FO[R]) is an important means of specification in system analysis. Its decidability status is known for some individual types of infinite-state systems such as pushdown (decidable) and vector addition systems (undecidable).This work aims at a general understanding of which types of systems admit decidability. As a unifying model, we employ valence systems over graph monoids, which feature a finite-state control and are parameterized by a monoid to represent their storage mechanism. As special cases, this includes pushdown systems, various types of counter systems (such as vector addition systems) and combinations thereof. Our main result is a characterization of those graph monoids where FO[R] is decidable for the resulting transition systems.
机译：具有可达性谓词（FO [R]）的一阶逻辑是系统分析中进行规范的重要手段。它的可判定性状态对于某些类型的无限状态系统（例如下推式（可判定）和矢量加法系统（不可判定））是已知的。这项工作旨在大致了解哪些类型的系统允许可判定性。作为一个统一模型，我们对图半体使用价系统，该系统具有有限状态控制并由一个半体参数化以表示其存储机制。作为特殊情况，这包括下推系统，各种类型的计数器系统（例如矢量加法系统）及其组合。我们的主要结果是表征那些图元半边形，其中FO [R]对于最终的过渡系统是可确定的。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号