Abstract Interpretation from Buchi Automata

被引:9
作者
Hofmann, Martin [1 ]
Chen, Wei [2 ]
机构
[1] Ludwig Maximilians Univ Munchen, Munich, Germany
[2] Univ Edinburgh, Edinburgh, Midlothian, Scotland
来源
PROCEEDINGS OF THE JOINT MEETING OF THE TWENTY-THIRD EACSL ANNUAL CONFERENCE ON COMPUTER SCIENCE LOGIC (CSL) AND THE TWENTY-NINTH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS) | 2014年
关键词
Type Systems; Type-and-Effect Systems; Temporal Properties; Liveness; MODAL MU-CALCULUS; MODEL CHECKING; SYSTEM; TREES;
D O I
10.1145/2603088.2603127
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We describe the construction of an abstract lattice from a given Buchi automata. The abstract lattice is finite and has the following key properties. (i) There is a Galois connection between it and the (infinite) lattice of languages of finite and infinite words over a given alphabet. (ii) The abstraction is faithful with respect to acceptance by the automaton. (iii) Least fixpoints and omega-iterations (but not in general greatest fixpoints) can be computed on the level of the abstract lattice. This allows one to develop an abstract interpretation capable of checking whether finite and infinite traces of a (recursive) program are accepted by a policy automaton. It is also possible to cast this analysis in form of a type and effect system with the effects being elements of the abstract lattice. While the resulting decidability and complexity results are known (regular model checking for pushdown systems) the abstract lattice provides a new point of view and enables smooth integration with data types, objects, higher-order functions which are best handled with abstract interpretation or type systems. We demonstrate this by generalising our type-and-effect systems to object-oriented programs and higher-order functions.
引用
收藏
页数:10
相关论文
共 50 条
[31]   Kleene and Buchi Theorems for Weighted Automata and Multi-valued Logics over Arbitrary Bounded Lattices [J].
Droste, Manfred ;
Vogler, Heiko .
DEVELOPMENTS IN LANGUAGE THEORY, 2010, 6224 :160-+
[32]   Theories, Solvers and Static Analysis by Abstract Interpretation [J].
Cousot, Patrick ;
Cousot, Radhia ;
Mauborgne, Laurent .
JOURNAL OF THE ACM, 2012, 59 (06)
[33]   Abstract Interpretation of Dynamics of Biological Regulatory Networks [J].
Pauleve, Loic ;
Magnin, Morgan ;
Roux, Olivier .
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2011, 272 :43-56
[34]   Automatic Construction of Complete Abstraction by Abstract Interpretation [J].
Qian, Junyan ;
Zhao, Lingzhong ;
Cai, Guoyong ;
Gu, Tianlong .
PROCEEDINGS OF THE 8TH IEEE/ACIS INTERNATIONAL CONFERENCE ON COMPUTER AND INFORMATION SCIENCE, 2009, :927-+
[35]   Strongly preserving abstraction by complete abstract interpretation [J].
Qian, Jun-Yan ;
Zhao, Ling-Zhong ;
Cai, Guo-Yong .
Jisuanji Xuebao/Chinese Journal of Computers, 2014, 37 (08) :1754-1767
[36]   An efficient simulation algorithm based on abstract interpretation [J].
Ranzato, Francesco ;
Tapparo, Francesco .
INFORMATION AND COMPUTATION, 2010, 208 (01) :1-22
[37]   Calculational Design of a Regular Model Checker by Abstract Interpretation [J].
Cousot, Patrick .
THEORETICAL ASPECTS OF COMPUTING - ICTAC 2019, 2019, 11884 :3-21
[38]   Abstract Interpretation of Symbolic Execution with Explicit State Updates [J].
Bubel, Richard ;
Hahnle, Reiner ;
Weiss, Benjamin .
FORMAL METHODS FOR COMPONENTS AND OBJECTS, 2009, 5751 :247-+
[39]   Abstract interpretation based verification of temporal properties for BioAmbients [J].
Gori, Roberta ;
Levi, Francesca .
INFORMATION AND COMPUTATION, 2010, 208 (08) :869-921
[40]   Calculational design of a regular model checker by abstract interpretation [J].
Cousot, Patrick .
THEORETICAL COMPUTER SCIENCE, 2021, 869 :62-84