• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International Conference on Concurrency Theory(CONCUR 2004); 20040831-20040903; London; GB >Parameterised Boolean Equation Systems
【24h】

Parameterised Boolean Equation Systems

机译：参数化布尔方程组

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

摘要

Boolean equation system are a useful tool for verifying formulas from modal mu-calculus on transition systems (see for an excellent treatment). We are interested in an extension of boolean equation systems with data. This allows to formulate and prove a substantially wider range of properties on much larger and even infinite state systems. In previous works it has been outlined how to transform a modal formula and a process, both containing data, to a so-called parameterised boolean equation system, or equation system for short. In this article we focus on techniques to solve such equation systems. We introduce a new equivalence between equation systems, because existing equivalences are not compositional. We present techniques similar to Gauss elimination as outlined in [9] that allow to solve each equation system provided a single equation can be solved. We give several techniques for solving single equations, such as approximation (known), patterns (new) and invariants (new). Finally, we provide several small but illustrative examples of verifications of modal mu-calculus formulas on concrete processes to show the use of the techniques.
机译：布尔方程组是从过渡系统的模态微积分中验证公式的有用工具（请参阅参考资料以获得出色的处理）。我们对带有数据的布尔方程组的扩展感兴趣。这允许在更大甚至甚至无限状态的系统上制定和证明实质上更广泛的特性范围。在以前的工作中，已经概述了如何将包含数据的模态公式和过程转换为所谓的参数化布尔方程组或简称为方程组。在本文中，我们重点介绍解决此类方程组的技术。由于现有的等价项不是组成部分，因此我们在方程组之间引入了新的等价项。我们提出了类似于[9]中概述的高斯消去的技术，只要可以解决一个方程，就可以求解每个方程组。我们提供了几种解决单个方程式的技术，例如近似（已知），模式（新）和不变式（新）。最后，我们提供了一些小而说明性的示例，这些示例对具体过程中的模态微积分公式进行了验证，以显示该技术的使用。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号