合成用于时间序列约束的参数化线性与非线性不变式数据库
人工智能
2019-01-29 v1
摘要
许多限制整数序列上某些计算结果约束，可由寄存器自动机紧凑表示。我们利用其寄存器自动机表示合成线性与非线性不变式数据库，从而改进同一序列上此类约束合取的传播。所得不变式是由序列长度函数参数化的公式，且被证明对任意足够长的序列成立。为评估此类线性不变式的质量，我们开发了一种方法以验证生成的线性不变式是否为可行点凸包的刻面。该方法以及非线性不变式的证明，均基于系统生成接受所有满足某简单条件的整数序列的常数大小确定性有限自动机。我们将该方法应用于一组44个时间序列约束，获得1400个线性不变式（其中70%为刻面定义）和600个非线性不变式，并在短期电力生产问题上进行了测试。
引用
@article{arxiv.1901.09793,
title = {Synthesising a Database of Parameterised Linear and Non-Linear Invariants for Time-Series Constraints},
author = {Ekaterina Arafailova and Nicolas Beldiceanu and Helmut Simonis},
journal= {arXiv preprint arXiv:1901.09793},
year = {2019}
}
备注
42 pages, 14 figures