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

Graeme Gange; Pierre Ganty; Peter J. Stuckey

doi:10.1007/978-3-319-68167-2_5

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

Graeme Gange, Pierre Ganty, Peter J. Stuckey

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

6 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 language	English
Title of host publication	Automated Technology for Verification and Analysis
Subtitle of host publication	15th International Symposium, ATVA 2017 Pune, India, October 3–6, 2017 Proceedings
Editors	Deepak D’Souza, K. Narayan Kumar
Place of Publication	Cham Switzerland
Publisher	Springer
Pages	67-83
Number of pages	17
ISBN (Electronic)	9783319681672
ISBN (Print)	9783319681665
DOIs	https://doi.org/10.1007/978-3-319-68167-2_5
Publication status	Published - 2017
Externally published	Yes
Event	International Symposium on Automated Technology for Verification and Analysis 2017 - Pune, India Duration: 3 Oct 2017 → 6 Oct 2017 Conference number: 15th https://www.iarcs.org.in/atva2017/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	10482
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	International Symposium on Automated Technology for Verification and Analysis 2017
Abbreviated title	ATVA 2017
Country/Territory	India
City	Pune
Period	3/10/17 → 6/10/17
Internet address	https://www.iarcs.org.in/atva2017/

Access to Document

10.1007/978-3-319-68167-2_5

Cite this

Gange, G., Ganty, P., & Stuckey, P. J. (2017). Fixing the state budget: approximation of regular languages with small DFAs. In D. D’Souza, & K. Narayan Kumar (Eds.), Automated Technology for Verification and Analysis: 15th International Symposium, ATVA 2017 Pune, India, October 3–6, 2017 Proceedings (pp. 67-83). (Lecture Notes in Computer Science ; Vol. 10482 ). Springer. https://doi.org/10.1007/978-3-319-68167-2_5

Gange, Graeme ; Ganty, Pierre ; Stuckey, Peter J. / Fixing the state budget : approximation of regular languages with small DFAs. Automated Technology for Verification and Analysis: 15th International Symposium, ATVA 2017 Pune, India, October 3–6, 2017 Proceedings. editor / Deepak D’Souza ; K. Narayan Kumar . Cham Switzerland : Springer, 2017. pp. 67-83 (Lecture Notes in Computer Science ).

@inproceedings{98713e569055478ebb92194de599fa58,

title = "Fixing the state budget: approximation of regular languages with small DFAs",

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.",

author = "Graeme Gange and Pierre Ganty and Stuckey, \{Peter J.\}",

year = "2017",

doi = "10.1007/978-3-319-68167-2\_5",

language = "English",

isbn = "9783319681665",

series = "Lecture Notes in Computer Science ",

publisher = "Springer",

pages = "67--83",

editor = "Deepak D{\textquoteright}Souza and \{Narayan Kumar \}, K.",

booktitle = "Automated Technology for Verification and Analysis",

address = "Switzerland",

note = "International Symposium on Automated Technology for Verification and Analysis 2017, ATVA 2017 ; Conference date: 03-10-2017 Through 06-10-2017",

url = "https://www.iarcs.org.in/atva2017/",

}

Gange, G, Ganty, P & Stuckey, PJ 2017, Fixing the state budget: approximation of regular languages with small DFAs. in D D’Souza & K Narayan Kumar (eds), Automated Technology for Verification and Analysis: 15th International Symposium, ATVA 2017 Pune, India, October 3–6, 2017 Proceedings. Lecture Notes in Computer Science , vol. 10482 , Springer, Cham Switzerland, pp. 67-83, International Symposium on Automated Technology for Verification and Analysis 2017, Pune, India, 3/10/17. https://doi.org/10.1007/978-3-319-68167-2_5

Fixing the state budget: approximation of regular languages with small DFAs. / Gange, Graeme; Ganty, Pierre; Stuckey, Peter J.
Automated Technology for Verification and Analysis: 15th International Symposium, ATVA 2017 Pune, India, October 3–6, 2017 Proceedings. ed. / Deepak D’Souza; K. Narayan Kumar . Cham Switzerland: Springer, 2017. p. 67-83 (Lecture Notes in Computer Science ; Vol. 10482 ).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

TY - GEN

T1 - Fixing the state budget

T2 - International Symposium on Automated Technology for Verification and Analysis 2017

AU - Gange, Graeme

AU - Ganty, Pierre

AU - Stuckey, Peter J.

N1 - Conference code: 15th

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/85031397531

U2 - 10.1007/978-3-319-68167-2_5

DO - 10.1007/978-3-319-68167-2_5

M3 - Conference Paper

AN - SCOPUS:85031397531

SN - 9783319681665

T3 - Lecture Notes in Computer Science

SP - 67

EP - 83

BT - Automated Technology for Verification and Analysis

A2 - D’Souza, Deepak

A2 - Narayan Kumar , K.

PB - Springer

CY - Cham Switzerland

Y2 - 3 October 2017 through 6 October 2017

ER -

Gange G, Ganty P, Stuckey PJ. Fixing the state budget: approximation of regular languages with small DFAs. In D’Souza D, Narayan Kumar K, editors, Automated Technology for Verification and Analysis: 15th International Symposium, ATVA 2017 Pune, India, October 3–6, 2017 Proceedings. Cham Switzerland: Springer. 2017. p. 67-83. (Lecture Notes in Computer Science ). doi: 10.1007/978-3-319-68167-2_5

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

Abstract

Publication series

Conference

Access to Document

Other files and links

Towards reliability in combinatorial optimisation

Cite this

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

Abstract

Publication series

Conference

Access to Document

Other files and links

Projects

Towards reliability in combinatorial optimisation

Cite this