Abstract
We show how to convert alternating Büechi automata to symbolic structures, using a variant of Miyano and Hayashi’s construction. We avoid building the nondeterministic equivalent of the alternating automaton, thus save an exponential factor in space.
For one-weak automata, Miyano and Hayashi’s approach produces automata that are larger than needed. We show a hybrid approach that produces a smaller nondeterministic automaton if part of the alternating automaton is one weak.
We perform a thorough experimental analysis and conclude that the symbolic approach outperforms the explicit one.
Supported by the European Commission under contract 507219 (PROSYD).
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
IEEE-Commission: IEEE standard for Property Specification Language (PSL) (2005) IEEE Std (1850-2005)
Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Singerman, E., Tiemeyer, A., Vardi, M.Y., Zbar, Y.: The forSpec temporal logic: A new temporal property-specification language. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 296–311. Springer, Heidelberg (2002)
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. Logic in Computer Science, pp. 322–331 (1986)
Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 248–263. Springer, Heidelberg (2000)
Gastin, P., Oddoux, D.: Fast LTL to büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001)
Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. Formal Methods in System Design 1, 47–71 (1997)
Ben-David, S., Bloem, R., Fisman, D., Griesmayer, A., Pill, I., Ruah, S.: Automata construction algorithms optimized for PSL, Prosyd D 3.2/4 (2005), http://www.prosyd.org
Miyano, S., Hayashi, T.: Alternating finite automata on ω-words. Theoretical Computer Science 32, 321–330 (1984)
Leucker, M.: Logics for mazurkiewicz traces. Technical Report AIB-2002-10, RWTH, Aachen, Germany (2002)
Jehle, M., Johannsen, J., Lange, M., Rachinsky, N.: Bounded model checking for all regular properties. In: 3rd Workshop on Bounded Model Checking (BMC 2005). Electronic Notes in Theoretical Computer Science, vol. 144.1, pp. 3–18 (2005)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems, Specification. Springer, New York (1992)
Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Transactions on Computational Logic 2(3), 408–429 (2001)
Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NUSMV: A new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)
Heljanko, K., Junttila, T.A., Latvala, T.: Incremental and complete bounded model checking for full PLTL. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 98–111. Springer, Heidelberg (2005)
Eén, N., Sörensson, N.: MiniSAT (2005), http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/Main.html
David, S.B., Orni, A.: Property-by-Example guide: a handbook of PSL/Sugar examples - PROSYD deliverable d1.1/3 (2005), http://www.prosyd.org
Fritz, C.: Constructing büchi automata from linear temporal logic using simulation relations for alternating büchi automata. In: Ibarra, O., Dang, Z. (eds.) CIAA 2003. LNCS, vol. 2759, pp. 35–48. Springer, Heidelberg (2003)
Fritz, C., Wilke, T.: Simulation relations for alternating Büchi automata. Theoretical Computer Science 338, 275–314 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bloem, R., Cimatti, A., Pill, I., Roveri, M., Semprini, S. (2006). Symbolic Implementation of Alternating Automata. In: Ibarra, O.H., Yen, HC. (eds) Implementation and Application of Automata. CIAA 2006. Lecture Notes in Computer Science, vol 4094. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11812128_20
Download citation
DOI: https://doi.org/10.1007/11812128_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37213-4
Online ISBN: 978-3-540-37214-1
eBook Packages: Computer ScienceComputer Science (R0)