• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Computer Science Logic >Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars
【24h】

Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars

机译：具有基数界的分数集合和带有星号的混合线性算术

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

摘要

We present decision procedures for logical constraints involving collections such as sets, multisets, and fuzzy sets. Element membership in our collections is given by characteristic functions from a finite universe (of unknown size) to a user-defined subset of rational numbers. Our logic supports standard operators such as union, intersection, difference, or any operation defined pointwise using mixed linear integer-rational arithmetic. Moreover, it supports the notion of cardinality of the collection, defined as the sum of occurrences of all elements. Deciding formulas in such logic has applications in software verification. Our decision procedure reduces satisfiability of formulas with collections to satisfiability of formulas in an extension of mixed linear integer-rational arithmetic with a "star" operator. The star operator computes the integer cone (closure under vector addition) of the solution set of a given formula. We give an algorithm for eliminating the star operator, which reduces the problem to mixed linear integer-rational arithmetic. Star elimination combines naturally with quantifier elimination for mixed integer-rational arithmetic. Our decidability result subsumes previous special cases for sets and multisets. The extension with star is interesting in its own right because it can encode reachability problems for a simple class of transition systems.
机译：我们提出了涉及集合（如集合，多集合和模糊集合）的逻辑约束的决策程序。我们集合中的元素隶属关系由从有限宇宙（大小未知）到用户定义的有理数子集的特征函数给出。我们的逻辑支持标准运算符，例如并集，交集，差或使用混合线性整数有理算术逐点定义的任何运算。此外，它支持集合的基数概念，定义为所有元素出现的总和。此类逻辑中的公式公式在软件验证中具有应用。我们的决策程序在带有“ star”运算符的混合线性整数有理算术扩展中，将具有集合的公式的可满足性降低为公式的可满足性。星形算子计算给定公式的解集的整数锥（向量加法下的闭合）。我们给出了消除星形算子的算法，该算法将问题简化为混合线性整数有理数算法。恒星消除与混合整数理性算术的量词消除自然结合。我们的可判定性结果包含了先前对集合和多集的特殊情况。 star扩展本身很有趣，因为它可以为简单的过渡系统类别编码可达性问题。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号