微信服务号

微信订阅号

2025年4月3日 8:08 星期四
首页 > 过刊浏览>2016年第27卷第3期 >682-690. DOI:10.13328/j.cnki.jos.004989
PDF HTML阅读 XML下载 导出引用 引用提醒
面向无穷数据的形式模型综述
作者:
基金项目:

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


Survey on Formal Models to Reason about Infinite Data Values
Author:
Fund Project:

National Natural Science Foundation of China (61402179, 61100062, 61272135, 61472474, 61572478); Shanghai Pujiang Program (14PJ1403200); Shanghai ChenGuang Program (13CG21)

  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [79]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

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

    Abstract:

    Infinite data exists extensively in computer programs and database systems.Driven by the need from the applications of formal verification and database management, formal models over infinite alphabets are becoming a research focus of theoretical computer science.The main purpose of this article is to do a relatively complete and detailed survey on this topic.The article is organized according to the different mechanisms of automata models to deal with the infinite data values.The main focus is on the decidability and complexity of the related decision problems, that is, the nonemptiness and language inclusion problem of automata, and the satisfiability problem of logics.

    参考文献
    [1] van Leeuwen J, ed. Handbook of Theoretical Computer Science, Vol.B:Formal Models and Semantics. Elsevier and MIT Press, 1990.
    [2] Wolper P, Vardi M, Sistla A. Reasoning about infinite computation paths. In:Proc. of the FOCS 1983. 1983. 185-194.[doi:10. 1109/SFCS.1983.51]
    [3] Varidi M, Wolper P. An automata-theoretic approach to automatic program verification. In:Proc. of the LICS 1986. 1986. 332-344.
    [4] Hopcroft J, Ullman J. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, 1979.
    [5] Büchi J. Weak second-order arithmetic and finite automata. Mathematical Logik Quarterly Mlq, 1960,6:66-92.[doi:10.1002/malq. 19600060105]
    [6] Elgot C. Decision problems of finite automata design and related arithmetic. IEEE Trans. on American Mathematical Society, 1961, 98:21-52.[doi:10.2307/1993511]
    [7] Thatcher JW, Wright JB. Generalized finite automata theory with an application to a decision problem of second-order logic. Theory of Computing Systems, 1968,2(1):57-81.[doi:10.1007/BF01691346]
    [8] Buchi J. On a decision method in restricted second-order arithmetic. In:Proc. of the Int'l Congress for Logic, Methodology and Philosophy of Science. Standford University Press, 1962. 1-11.[doi:10.1007/978-1-4613-8928-6_23]
    [9] Schutzenberger MP. On finite monoids having only trivial subgroups. Information and Computation, 1965,8:190-194.[doi:10. 1016/S0019-9958(65)90108-7]
    [10] McNaughton R, Papert S. Counter-Free Automata. MIT Press, 1971.
    [11] Segoufin L. Automata and logics for words and trees over an infinite alphabet. In:Proc. of the CSL 2006. 2006. 41-57.[doi:10. 1007/11874683_3]
    [12] Balaban I, Pnueli A, Zuck L. Shape analysis by predicate abstraction. In:Proc. of the VMCAI 2005. 2005. 164-180.[doi:10. 1007/978-3-540-30579-8_12]
    [13] Gopan D, Reps T, Sagiv M. A framework for numeric analysis of array operations. In:Proc. of the POPL 2008. 2008. 338-350.[doi:10.1145/1040305.1040333]
    [14] Gulwani S, McCloskey B, Tiwari A. Lifting abstract interpreters to quantified logical domains. In:Proc. of the POPL 2008. 2008. 235-246.[doi:10.1145/1328438.1328468]
    [15] Alur R, Cerny P, Weinstein S. Algorithmic analysis of array-accessing programs. In:Proc. of the CSL 2009. LNCS 5771, 2009. 86-101.[doi:10.1007/978-3-642-04027-6_9]
    [16] Alur R, Cerny P. Streaming transducers for algorithmic verification of single-pass list-processing programs. In:Proc. of the POPL 2011. 2011. 599-610.[doi:10.1145/1926385.1926454]
    [17] Neven F. Automata, logic, and XML. In:Proc. of the CSL 2002. 2002. 2-26.
    [18] Vianu V. A Web odyssey:From codd to XML. In:Proc. of the PODS 2001. 2001. 1-15.[doi:10.1145/776985.776999]
    [19] Alon N, Milo T, Neven F, Suciu D, Vianu V. XML with data values:Typechecking revisited. Journal of Computer and System Sciences, 2003,66(4):688-727.[doi:10.1016/S0022-0000(03)00032-1]
    [20] Fan W, Libkin L. On XML integrity constraints in the presence of DTDs. Journal of ACM, 2002,49(3):368-406.[doi:10.1145/567112.567117]
    [21] Schwentick Th. XPath query containment. SIGMOD Record, 2004,33(1):101-109.[doi:10.1145/974121.974140]
    [22] Libkin L, Vrgoc D. Regular path queries on graphs with data. In:Proc. of the ICDT 2012. 2012. 74-85.[doi:10.1145/2274576.2274585]
    [23] Libkin L, Martens W, Vrgoc D. Querying graph databases with XPath. In:Proc. of the ICDT 2013. 2013. 129-140.[doi:10.1145/2448496.2448513]
    [24] Kaminski M, Francez N. Finite memory automata. Theoretical Computer Science, 1994,134(2):329-363.[doi:10.1016/0304-3975(94)90242-9]
    [25] Kaminski M, Tan T. Tree Automata Over Infinite Alphabets. Pillars of Computer Science, 2008.[doi:10.1007/978-3-540-78127-1_21]
    [26] Demri S, Lazic R. LTL with the freeze quantifer and register automata. In:Proc. of the LICS 2006. 2006. 17-26.[doi:10.1109/LICS.2006.31]
    [27] Demri S, Lazic R, Nowak D. On the freeze quantifier in constraint LTL. In:Proc. of the TIMES 2005. 2005. 113-121.[doi:10. 1109/TIME.2005.28]
    [28] Jurdzinski M, Lazic R. Alternating automata on data trees and XPath satisfiability. ACM Trans. on Computational Logic, 2011, 12(3):19.[doi:10.1145/1929954.1929956]
    [29] Figueira D. Forward-XPath and extended register automata on data-trees. In:Proc. of the ICDT 2010. 2010. 231-241.[doi:0.1145/1804669.1804699]
    [30] Figueira D, Segoufin L. Bottom-Up automata on data trees and vertical XPath. In:Proc. of the STACS 2011. 2011. 93-104.[doi:10.4230/LIPIcs.STACS.2011.93]
    [31] Figueira D, Hofman P, Lasota S. Relating timed and register automata. In:Proc. of the EXPRESS 2010, Vol.41. EPTCS, 2010. 61-75.[doi:10.1017/S0960129514000322]
    [32] Lasota S, Walukiewicz I. Alternating timed automata. In:Proc. of the FSTTCS 2005, Vol.3441. 2005. 250-265.[doi:10.1007/978-3-540-31982-5_16]
    [33] Kaminski M, Tan T. Regular expressions for languages over infinite alphabets. Fundamenta Informaticae, 2006,69(3):301-318.[doi:10.1007/978-3-540-27798-9_20]
    [34] Libkin L, Vrgoc D. Regular expressions for data words. In:Proc. of the LPAR 2012. 2012. 274-288.[doi:10.1007/978-3-642-28717-6_22]
    [35] Libkin L, Tan T, Vrgoc D. Regular expressions with binding over data words for querying graph databases. In:Proc. of the DLT 2013. 2013. 325-337.[doi:10.1007/978-3-642-38771-5_29]
    [36] Bojanczyk M, Muscholl A, Schwentick T, Segoufin L, David C. Two-Variable logic on words with data. In:Proc. of the LICS 2006. 2006. 7-16.[doi:10.1109/LICS.2006.51]
    [37] Bojańczyk M, David C, Muscholl A, Schwentick T, Segoufin L. Two-Variable logic on data trees and XML reasoning. In:Proc. of the PODS 2006. 2006. 10-19.[doi:10.1145/1142351.1142354]
    [38] Bojanczyk M, Lasota S. An extension of data automata that captures XPath. In:Proc. of the LICS 2010. 2010. 243-252.[doi:10. 1109/LICS.2010.33]
    [39] David C, Libkin L, Tan T. On the satisfiability of two-variable logic over data words. In:Proc. of the LPAR 2010. 2010. 248-262.[doi:10.1007/978-3-642-16242-8_18]
    [40] Wu ZL. A decidable extension of data automata. In:Proc. of the GandALF 2011. 2011. 116-130.[doi:10.4204/EPTCS.54.9]
    [41] Wu ZL. Commutative data automata. In:Proc. of the CSL 2012. 2012. 528-542.[doi:10.4230/LIPIcs.CSL.2012.528]
    [42] Schwentick T, Zeume T. Two-Variable logic with two order relations. In:Proc. of the CSL 2010. 2010. 499-513.[doi:10.1007/978-3-642-15205-4_38]
    [43] Tan T. An automata model for trees with ordered data values. In:Proc. of the LICS 2012. 2012. 586-595.[doi:10.1109/LICS. 2012.69]
    [44] Kara A, Schwentick T, Zeume T. Temporal logics on words with multiple data values. In:Proc. of the FSTTCS 2010. 2010. 481-492.[doi:10.4230/LIPIcs.FSTTCS.2010.481]
    [45] Decker N, Habermehl P, Leucker M, Thoma D. Ordered navigation on multi-attributed data words. In:Proc. of the CONCUR 2014. 2014. 497-511.[doi:10.1007/978-3-662-44584-6_34]
    [46] Neven F, Schwentick T, Vianu V. Finite state machines for strings over infinite alphabets. ACM Trans. on Computational Logic, 2004, 15(3):403-435.[doi:10.1145/1013560.1013562]
    [47] Tan T. On pebble automata for data languages with decidable emptiness problem. Journal of Computer and System Sciences, 2010, 76(8):778-791.[doi:10.1016/j.jcss.2010.03.004]
    [48] Grumberg O, Kupferman O, Sheinvald S. Variable automata over infinite alphabets. In:Proc. of the LATA 2010. 2010. 561-572.[doi:10.1007/978-3-642-13089-2_47]
    [49] Grumberg O, Kupferman O, Sheinvald S. Model checking systems and specifications with parameterized atomic propositions. In:Proc. of the ATVA 2012. 2012. 122-136.[doi:10.1007/978-3-642-33386-6_11]
    [50] Grumberg O, Kupferman O, Sheinvald S. An automata-theoretic approach to reasoning about parameterized systems and specifications. In:Proc. of the ATVA 2013. 2013. 397-411.[doi:10.1007/978-3-319-02444-8_28]
    [51] Fu Song, Zhilin Wu. Extending temporal logics with data variable quantifications. In:Proc. of the FSTTCS 2013. 2013. 253-265.[doi:10.4230/LIPIcs.FSTTCS.2014.253]
    [52] Chen T, Fu S, Wu ZL. On the satisfiability of indexed linear temporal logics. In:Proc. of the CONCUR 2015. 2015. 254-267.[doi:10.4230/LIPIcs.CONCUR.2015.254]
    [53] David C. Complexity of data tree patterns over XML documents. In:Proc. of the MFCS 2008. 2008. 278-289.[doi:10.1007/978-3-540-85238-4_22]
    [54] Bjorklund H, Martens W, Schwentick T. Optimizing conjunctive queries over trees using schema information. In:Proc. of the MFCS 2008. 2008. 132-143.[doi:10.1007/978-3-540-85238-4_10]
    [55] Abiteboul S, Segoufin L, Vianu V. Static analysis of active XML systems. In:Proc. of the PODS 2008. 2008. 221-230.[doi:10. 1145/1620585.1620590]
    [56] Genest B, Muscholl A, Wu ZL. Verifying recursive active documents with positive data tree rewriting. In:Proc. of the FSTTCS 2010. 2010. 469-480.[doi:10.4230/LIPIcs.FSTTCS.2010.469]
    [57] Bruce W. Watson:Implementing and using finite automata toolkits. Natural Language Engineering, 1996,2(4):295-302.[doi:10. 1017/S135132499700154X]
    [58] van Noord G, Gerdemann D. Finite state transducers with predicates and identities. Grammars, 2001,4(3):263-286.[doi:10.1023/A:1012291501330]
    [59] Pill I. Requirements engineering and efficient verification of PSL properties[Ph.D. Thesis]. Graz Univeristy of Technology, 2008.
    [60] Cimatti A, Mover S, Roveri M, Tonetta S. From sequential extended regular expressions to NFA with symbolic labels. In:Proc. of the CIAA 2010. 2010. 87-94.[doi:10.1007/978-3-642-18098-9_10]
    [61] Veanes M, Grigorenko P, de Halleux P, Tillmann N. Rex:Symbolic regular expression explorer. In:Proc. of the ICST 2010. 2010. 498-507.[doi:10.1109/ICST.2010.15]
    [62] Veanes M, Bjørner N, de Moura LM. Symbolic automata constraint solving. In:Proc. of the LPAR 2010. 2010. 640-654.[doi:10. 1007/978-3-642-16242-8_45]
    [63] Hooimeijer P, Livshits B, Molnar D, Saxena P, Veanes M. Fast and precise sanitizer analysis with BEK. In:Proc. of the USENIX Security Symp. 2011.
    [64] Veanes M, Bjørner N. Symbolic automata:The toolkit. In:Proc. of the TACAS 2012. 2012. 472-477.[doi:10.1007/978-3-642-28756-5_33]
    [65] Veanes M, Hooimeijer P, Livshits B, Molnar D, Bjørner N. Symbolic finite state transducers:Algorithms and applications. In:Proc. of the POPL 2012. 2012. 137-150.[doi:10.1145/2103656.2103674]
    [66] D'Antoni L, Veanes M. Static analysis of string encoders and decoders. In:Proc. of the VMCAI 2013. 2013. 209-228.
    [67] D'Antoni L, Alur R. Symbolic visibly pushdown automata. In:Proc. of the CAV 2014. 2014. 209-225.[doi:10. 1007/978-3-642-35873-9_14]
    [68] Veanes M, Bjørner N. Symbolic tree transducers. In:Proc. of the Ershov Memorial Conf. 2011. 377-393.[doi:10. 1007/978-3-642-29709-0_32]
    [69] D'Antoni L, Veanes M, Livshits B, Molnar D. Fast:A transducer-based language for tree manipulation. In:Proc. of the PLDI 2014. 2014. 40.[doi:10.1145/2594291.2594309]
    [70] Veanes M, Bjørner N. Symbolic tree automata. Information Processing Letters, 2015,115(3):418-424.[doi:10.1016/j.ipl.2014. 11. 005]
    [71] Ishtiaq S, O'Hearn P. BI as an assertion language for mutable data structures. In:Proc. of the Principles of Programming Languages (POPL 2001). 2014. 14-26.[doi:10.1145/360204.375719]
    [72] Yang H. Local reasoning for stateful programs. Technical Report, UIUCDCS-R-2001-2227, University of Illinois at Urbana-Champaign, 2001.
    [73] Reynolds JC. Separation logic:A logic for shared mutable data structures. In:Proc. of the LICS 2002. 2002. 55-74.[doi:10.1109/LICS.2002.1029817]
    [74] Bansal K, Brochenin R, Lozes É, Shapes B. Lists with ordered data. In:Proc. of the FOSSACS 2009. 2009. 425-439.[doi:10. 1007/978-3-642-00596-1_30]
    [75] Chin WN, David C, Nguyen HH, Qin SC. Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Science of Computer Programming, 2012,77(9):1006-1036.[doi:10.1016/j.scico.2010.07.004]
    [76] Chu DH, Jaffar J, Trinh MT. Automatic induction proofs of data-structures in imperative programs. In:Proc. of the PLDI 2015. 2015. 457-466.[doi:10.1145/2737924.2737984]
    [77] Enea C, Sighireanu M, Wu ZL. On automated lemma generation for separation logic with inductive definitions. In:Proc. of the ATVA 20152015. 80-96.[doi:10.1007/978-3-319-24953-7_7]
    [78] Habermehl P, Holík L, Rogalewicz A, Simácek J, Vojnar T. Forest automata for verification of heap manipulation. Formal Methods in System Design, 2012,41(1):83-106.[doi:10.1007/s10703-012-0150-8]
    [79] Abdulla PA, Holík L, Jonsson B, Lengál O, Trinh CQ, Vojnar T. Verification of heap manipulating programs with ordered data by extended forest automata. In:Proc. of the ATVA 2013. 2013. 224-239.[doi:10.1007/s00236-015-0235-0]
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

宋富,吴志林.面向无穷数据的形式模型综述.软件学报,2016,27(3):682-690

复制
分享
文章指标
  • 点击次数:5263
  • 下载次数: 6394
  • HTML阅读次数: 2924
  • 引用次数: 0
历史
  • 收稿日期:2015-07-30
  • 最后修改日期:2015-10-20
  • 在线发布日期: 2016-01-06
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19778452位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号