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.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
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)