Fixing the state budget: approximation of regular languages with small DFAs

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

3 Citations (Scopus)

Abstract

Strings are pervasive in programming, and arguably even more pervasive in web programming. A natural abstraction for reasoning about strings are finite-automata. They are a well-understood formalism, and operations on them are decidable and well-known. But in practice these operations either blow up in size or in cost of operations. Hence the attractive automata representations become impractical. In this paper we propose reasoning about strings using small automata, by restricting the number of states available. We show how we can construct small automata which over-approximate the language specified by a larger automata, using discrete optimization techniques, both complete approaches and incomplete approaches based on greedy search. Small automata provide a strong basis for reasoning about strings in programming, since operations on small automata do not blow up in cost.

Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis
Subtitle of host publication15th International Symposium, ATVA 2017 Pune, India, October 3–6, 2017 Proceedings
EditorsDeepak D’Souza, K. Narayan Kumar
Place of PublicationCham Switzerland
PublisherSpringer
Pages67-83
Number of pages17
ISBN (Electronic)9783319681672
ISBN (Print)9783319681665
DOIs
Publication statusPublished - 2017
Externally publishedYes
EventInternational Symposium on Automated Technology for Verification and Analysis 2017 - Pune, India
Duration: 3 Oct 20176 Oct 2017
Conference number: 15th
https://www.iarcs.org.in/atva2017/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume10482
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Symposium on Automated Technology for Verification and Analysis 2017
Abbreviated titleATVA 2017
CountryIndia
CityPune
Period3/10/176/10/17
Internet address

Cite this