面向无穷数据的形式模型综述

来源：软件学报杂志2016年第3期北京时间：

作者：宋富,吴志林

单位：宋富，上海市高可信计算重点实验室(华东师范大学), 上海 20006211,吴志林，计算机科学国家重点实验室(中国科学院软件研究所), 北京 10019002

摘要：无穷数据广泛存在于计算机程序和数据库系统中.受到形式验证与数据库两方面应用需求的推动,面向无穷数据的形式模型已经成为理论计算机科学的研究热点之一.对面向无穷数据的形式模型(逻辑与自动机)进行了相对全面而详细的总结.主要按照不同自动机模型对无穷数据的处理方式加以组织,并关注相关判定问题,即:自动机的非空性问题、语言包含问题以及逻辑的可满足性问题的可判定性与复杂性.

关键词：无穷数据;自动机;逻辑;非空性;语言包含;可满足性;可判定性;复杂性

基金资助：国家自然科学基金(61402179,61100062,61272135,61472474,61572478);上海浦江人才计划(14PJ1403200);上海晨光人才计划(13CG21)