Faculty of Information Technology, BUT

Publication Details

Simulation Algorithms for Symbolic Automata

HOLÍK Lukáš, LENGÁL Ondřej, SÍČ Juraj, VEANES Margus and VOJNAR Tomáš. Simulation Algorithms for Symbolic Automata. In: Proc. of 16th International Symposium on Automated Technology for Verification and Analysis. Heidelberg: Springer Verlag, 2018, pp. 109-125. ISBN 978-3-030-01089-8. ISSN 0302-9743. Available from: http://dx.doi.org/10.1007/978-3-030-01090-4_7
Czech title
Symbolické algoritmy pro symbolické automaty
Type
conference paper
Language
english
Authors
Holík Lukáš, Mgr., Ph.D. (DITS FIT BUT)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Síč Juraj, Bc. (RCIT FIT BUT)
Veanes Margus (MSR)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
URL
Keywords
symbolic automata
simulation
finite automata
Abstract
We investigate means of efficient computation of the simulation relation over symbolic finite automata (SFAs), i.e., finite automata with transitions labeled by predicates over alphabet symbols. In one approach, we build on the algorithm by Ilie, Navaro, and Yu proposed originally for classical finite automata, modifying it using the so-called mintermisation of the transition predicates. This solution, however, generates all Boolean combinations of the predicates, which easily causes an exponential blowup in the number of transitions. Therefore, we propose two more advanced solutions. The first one still applies mintermisation but in a local way, mitigating the size of the exponential blowup. The other one focuses on a novel symbolic way of dealing with transitions, for which we need to sacrifice the counting technique of the original algorithm (counting is used to decrease the dependency of the running time on the number of transitions from quadratic to linear). We perform a thorough experimental evaluation of all the algorithms, together with several further alternatives, showing that all of them have their merits in practice, but with the clear indication that in most of the cases, efficient treatment of symbolic transitions is more beneficial than counting.
Published
2018
Pages
109-125
Journal
Lecture Notes in Computer Science, no. 11138, ISSN 0302-9743
Proceedings
Proc. of 16th International Symposium on Automated Technology for Verification and Analysis
Conference
16th International Symposium on Automated Technology for Verification and Analysis, Los Angeles, US
ISBN
978-3-030-01089-8
Publisher
Springer Verlag
Place
Heidelberg, DE
DOI
BibTeX
@INPROCEEDINGS{FITPUB11801,
   author = "Luk\'{a}\v{s} Hol\'{i}k and Ond\v{r}ej Leng\'{a}l and Juraj S\'{i}\v{c} and Margus Veanes and Tom\'{a}\v{s} Vojnar",
   title = "Simulation Algorithms for Symbolic Automata",
   pages = "109--125",
   booktitle = "Proc. of 16th International Symposium on Automated Technology for Verification and Analysis",
   journal = "Lecture Notes in Computer Science",
   number = 11138,
   year = 2018,
   location = "Heidelberg, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-030-01089-8",
   ISSN = "0302-9743",
   doi = "10.1007/978-3-030-01090-4\_7",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11801"
}
Back to top