Abstract Interpretation from Buchi Automata

Martin Hofmann, Wei Chen

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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 ω-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.
Original languageEnglish
Title of host publicationProceedings 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)
Place of PublicationNew York, NY, USA
PublisherACM
Number of pages10
DOIs
Publication statusPublished - 2014

Publication series

NameCSL-LICS '14
PublisherACM

Keywords

  • liveness, temporal properties, type systems, type-and-effect systems

Fingerprint

Dive into the research topics of 'Abstract Interpretation from Buchi Automata'. Together they form a unique fingerprint.

Cite this