Abstract
We present ACME, a tool implementing algebraic techniques to solve decision problems from automata theory. The core generic algorithm takes as input an automaton and computes its stabilization monoid, which is a generalization of its transition monoid.
Using the stabilization monoid, one can solve many problems: determine whether a B-automaton (which is a special kind of automata with counters) is limited, whether two B-automata are equivalent, and whether a probabilistic leaktight automaton has value 1.
The research leading to these results has received funding from the French ANR project 2010 BLAN 0202 02 FREC, the European Union’s Seventh Framework Programme (FP7/2007-2013) under grant agreement 259454 (GALE) and 239850 (SOSNA).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Colcombet, T., Kuperberg, D., Lombardy, S.: Regular temporal cost functions. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010, Part II. LNCS, vol. 6199, pp. 563–574. Springer, Heidelberg (2010)
Colcombet, T.: The theory of stabilisation monoids and regular cost functions. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009, Part II. LNCS, vol. 5556, pp. 139–150. Springer, Heidelberg (2009)
Colcombet, T.: Regular cost-functions, part I: Logic and algebra over words. Logical Methods in Computer Science 9(3) (2013)
Fijalkow, N., Gimbert, H., Kelmendi, E., Oualhadj, Y.: Deciding the value 1 problem for probabilistic leaktight automata (2014)
Fijalkow, N., Gimbert, H., Oualhadj, Y.: Deciding the value 1 problem for probabilistic leaktight automata. In: LICS, pp. 295–304 (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Fijalkow, N., Kuperberg, D. (2014). ACME: Automata with Counters, Monoids and Equivalence. In: Cassez, F., Raskin, JF. (eds) Automated Technology for Verification and Analysis. ATVA 2014. Lecture Notes in Computer Science, vol 8837. Springer, Cham. https://doi.org/10.1007/978-3-319-11936-6_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-11936-6_12
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11935-9
Online ISBN: 978-3-319-11936-6
eBook Packages: Computer ScienceComputer Science (R0)