Abstract
The orbit problem is at the heart of symmetry reduction methods for model checking concurrent systems. It asks whether two given configurations in a concurrent system (represented as finite sequences over some finite alphabet) are in the same orbit with respect to a given finite permutation group (represented by their generators) acting on this set of configurations. It is known that the problem is in general as hard as the graph isomorphism problem, which is widely believed to be not solvable in polynomial time. In this paper, we consider the restriction of the orbit problem when the permutation group is cyclic (i.e. generated by a single permutation), an important restriction of the orbit problem. Our main result is a linear-time algorithm for this subproblem.
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.
Similar content being viewed by others
References
Primorial Numbers (The On-Line Encyclopedia of Integer Sequences), http://oeis.org/A002110
Babai, L., Beals, R., Cai, J.-Y., Ivanyos, G., Luks, E.M.: Multiplicative equations over commuting matrices. In: SODA, pp. 498–507 (1996)
Babai, L., Luks, E.M.: Canonical labeling of graphs. In: STOC, pp. 171–183 (1983)
Bach, E., Shallit, J.: Algorithmic Number Theory. Foundations of Computing, vol. 1. MIT Press (1996)
Bostan, A., Gaudry, P., Schost, É.: Linear Recurrences with Polynomial Coefficients and Application to Integer Factorization and Cartier-Manin Operator. SIAM J. Comput. 36(6), 1777–1806 (2007)
Brualdi, R.A.: Combinatorial matrix classes. Encyclopedia of Mathematics and Its Applications, vol. 108. Cambridge University Press (2006)
Cameron, P.J.: Permutation Groups. London Mathematical Society Student Texts. Cambridge University Press (1999)
Chrobak, M.: Finite automata and unary languages. Theor. Comput. Sci. 47(3), 149–158 (1986)
Clarke, E.M., Emerson, E.A., Jha, S., Sistla, A.P.: Symmetry reductions in model checking. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 147–158. Springer, Heidelberg (1998)
Clarke, E.M., Jha, S., Enders, R., Filkorn, T.: Exploiting symmetry in temporal logic model checking. Formal Methods in System Design 9(1/2), 77–104 (1996)
Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. The MIT Press (2009)
Costa, E., Harvey, D.: Faster deterministic integer factorization. CoRR, abs/1201.2116 (2012)
Donaldson, A.F., Miller, A.: On the constructive orbit problem. Ann. Math. Artif. Intell. 57(1), 1–35 (2009)
Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Formal Methods in System Design 9(1/2), 105–131 (1996)
Erdös, P., Graham, R.L.: On a linear diophantine problem of Frobenius. Acta Arithm. 21, 399–408 (1972)
Göller, S., Mayr, R., To, A.W.: On the computational complexity of verifying one-counter processes. In: LICS, pp. 235–244 (2009)
Hardy, G.H., Wright, E.M.: An Introduction to The Theory of Numbers, 6th edn. OUP Oxford (2008)
Ip, C.N., Dill, D.L.: Better verification through symmetry. Formal Methods in System Design 9(1/2), 41–75 (1996)
Kannan, R., Lipton, R.J.: Polynomial-time algorithm for the orbit problem. J. ACM 33(4), 808–821 (1986)
Sedgewick, R., Flajolet, P.: An Introduction to the Analysis of Algorithms, 2nd edn. Addison-Wesley Professional (2013)
Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time: Preliminary report. In: STOC, pp. 1–9 (1973)
To, A.W.: Unary finite automata vs. arithmetic progressions. Inf. Process. Lett. 109(17), 1010–1014 (2009)
Wahl, T., Donaldson, A.F.: Replication and abstraction: Symmetry in automated formal verification. Symmetry 2, 799–847 (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lin, A.W., Zhou, S. (2014). A Linear-Time Algorithm for the Orbit Problem over Cyclic Groups. In: Baldan, P., Gorla, D. (eds) CONCUR 2014 – Concurrency Theory. CONCUR 2014. Lecture Notes in Computer Science, vol 8704. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44584-6_23
Download citation
DOI: https://doi.org/10.1007/978-3-662-44584-6_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-44583-9
Online ISBN: 978-3-662-44584-6
eBook Packages: Computer ScienceComputer Science (R0)