Skip to main content
Top
Published in: Acta Informatica 5/2016

01-08-2016 | Original Article

A linear-time algorithm for the orbit problem over cyclic groups

Authors: Anthony W. Lin, Sanming Zhou

Published in: Acta Informatica | Issue 5/2016

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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 strings 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 by permuting indices. It is known that the problem is in general as hard as the graph isomorphism problem, whose precise complexity (whether it is solvable in polynomial-time) is a long-standing open problem. 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 problem. It is known that this subproblem is solvable in polynomial-time. Our main result is a linear-time algorithm for this subproblem.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Appendix
Available only for authorised users
Footnotes
1
For, if it were NP-hard, then the coset intersection problem (for permutation groups) would be NP-hard, owing to its polynomial-time equivalence to the orbit problem [9]. By the well-known results of [2, 16] (also see [17, Sect. 6.5, Chapter 27]), which essentially shows that the coset intersection problem is in the complexity class \(\text {coAM}\) (contained in the second level of the polynomial hierarchy), this would mean that the polynomial hierarchy collapses to the second level.
 
2
Some examples in [28] (even with a small number of processes) require a model checker to invoke an algorithm for the orbit problem hundreds to thousands of times for one transition system.
 
3
This means that the bound does not depend on any number-theoretic assumptions.
 
Literature
1.
go back to reference Babai, L., Luks, E.M.: Canonical labeling of graphs. In: STOC, pp. 171–183 (1983) Babai, L., Luks, E.M.: Canonical labeling of graphs. In: STOC, pp. 171–183 (1983)
3.
go back to reference Bach, E., Shallit, J.: Algorithmic Number Theory, Foundations of Computing, vol. 1. The MIT Press, Cambridge (1996)MATH Bach, E., Shallit, J.: Algorithmic Number Theory, Foundations of Computing, vol. 1. The MIT Press, Cambridge (1996)MATH
5.
go back to reference 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)MathSciNetCrossRefMATH 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)MathSciNetCrossRefMATH
6.
go back to reference Brualdi, R.A.: Combinatorial Matrix Classes. Encyclopedia of Mathematics and Its Applications, vol. 108. Cambridge University Press, Cambridge (2006)CrossRef Brualdi, R.A.: Combinatorial Matrix Classes. Encyclopedia of Mathematics and Its Applications, vol. 108. Cambridge University Press, Cambridge (2006)CrossRef
7.
go back to reference Cameron, P.J.: Permutation Groups. London Mathematical Society Student Texts. Cambridge University Press, Cambridge (1999)CrossRef Cameron, P.J.: Permutation Groups. London Mathematical Society Student Texts. Cambridge University Press, Cambridge (1999)CrossRef
8.
go back to reference Clarke, E.M.: The birth of model checking. In: 25 Years of Model Checking (2008) Clarke, E.M.: The birth of model checking. In: 25 Years of Model Checking (2008)
9.
go back to reference Clarke, E.M., Emerson, E.A., Jha, S., Sistla, A.P.: Symmetry reductions in model checking. In: CAV, pp. 147–158 (1998) Clarke, E.M., Emerson, E.A., Jha, S., Sistla, A.P.: Symmetry reductions in model checking. In: CAV, pp. 147–158 (1998)
10.
go back to reference Clarke, E.M., Jha, S., Enders, R., Filkorn, T.: Exploiting symmetry in temporal logic model checking. Formal Methods Syst. Des. 9(1/2), 77–104 (1996)CrossRef Clarke, E.M., Jha, S., Enders, R., Filkorn, T.: Exploiting symmetry in temporal logic model checking. Formal Methods Syst. Des. 9(1/2), 77–104 (1996)CrossRef
12.
go back to reference Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. The MIT Press, Cambridge (2009)MATH Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. The MIT Press, Cambridge (2009)MATH
13.
go back to reference Costa, E., Harvey, D.: Faster deterministic integer factorization. CoRR abs/1201.2116 (2012) Costa, E., Harvey, D.: Faster deterministic integer factorization. CoRR abs/1201.2116 (2012)
15.
go back to reference Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Formal Methods Syst. Des. 9(1/2), 105–131 (1996)CrossRef Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Formal Methods Syst. Des. 9(1/2), 105–131 (1996)CrossRef
16.
go back to reference Goldreich, O., Micali, S., Wigderson, A.: Proofs that yield nothing but their validity and a methodology of cryptographic protocol design (extended abstract). FOCS, 174–187 (1986). doi:10.1109/SFCS.1986.47 Goldreich, O., Micali, S., Wigderson, A.: Proofs that yield nothing but their validity and a methodology of cryptographic protocol design (extended abstract). FOCS, 174–187 (1986). doi:10.​1109/​SFCS.​1986.​47
17.
go back to reference Graham, R.L., Grötschel, M., Lovász, L. (eds.): Handbook of Combinatorics, vol. 2. MIT Press, Cambridge, MA (1995)MATH Graham, R.L., Grötschel, M., Lovász, L. (eds.): Handbook of Combinatorics, vol. 2. MIT Press, Cambridge, MA (1995)MATH
18.
go back to reference Hardy, G.H., Wright, E.M.: An Introduction to The Theory of Numbers, 6th edn. OUP Oxford, Oxford (2008)MATH Hardy, G.H., Wright, E.M.: An Introduction to The Theory of Numbers, 6th edn. OUP Oxford, Oxford (2008)MATH
19.
go back to reference Ip, C.N., Dill, D.L.: Better verification through symmetry. Formal Methods Syst. Des. 9(1/2), 41–75 (1996) Ip, C.N., Dill, D.L.: Better verification through symmetry. Formal Methods Syst. Des. 9(1/2), 41–75 (1996)
20.
go back to reference Israeli, A., Jalfon, M.: Token management schemes and random walks yield self-stabilizing mutual exclusion. In: PoDC, pp. 119–131 (1990). doi:10.1145/93385.93409 Israeli, A., Jalfon, M.: Token management schemes and random walks yield self-stabilizing mutual exclusion. In: PoDC, pp. 119–131 (1990). doi:10.​1145/​93385.​93409
22.
go back to reference Luks, E.M.: Permutation groups and polynomial-time computation. DIMACS Ser. Discrete Math. Theor. Comput. Sci. 11, 139–175 (1993)MathSciNetMATH Luks, E.M.: Permutation groups and polynomial-time computation. DIMACS Ser. Discrete Math. Theor. Comput. Sci. 11, 139–175 (1993)MathSciNetMATH
23.
go back to reference Norman, G.: Analysing randomized distributed algorithms. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 384–418. Springer, Berlin (2004) Norman, G.: Analysing randomized distributed algorithms. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 384–418. Springer, Berlin (2004)
25.
go back to reference Sedgewick, R., Flajolet, P.: An Introduction to the Analysis of Algorithms, 2nd edn. Addison-Wesley Professional, Boston (2013)MATH Sedgewick, R., Flajolet, P.: An Introduction to the Analysis of Algorithms, 2nd edn. Addison-Wesley Professional, Boston (2013)MATH
26.
go back to reference Shoup, V.: A Computational Introduction to Number Theory and Algebra, 2nd edn. Cambridge University Press, Cambridge (2005)CrossRefMATH Shoup, V.: A Computational Introduction to Number Theory and Algebra, 2nd edn. Cambridge University Press, Cambridge (2005)CrossRefMATH
27.
go back to reference Wahl, T., Donaldson, A.F.: Replication and abstraction: symmetry in automated formal verification. Symmetry 2, 799–847 (2010)MathSciNetCrossRef Wahl, T., Donaldson, A.F.: Replication and abstraction: symmetry in automated formal verification. Symmetry 2, 799–847 (2010)MathSciNetCrossRef
28.
go back to reference Zhang, S.J., Sun, J., Sun, C., Liu, Y., Ma, J., Dong, J.S.: Constraint-based automatic symmetry detection. In: ASE, pp. 15–25 (2013) Zhang, S.J., Sun, J., Sun, C., Liu, Y., Ma, J., Dong, J.S.: Constraint-based automatic symmetry detection. In: ASE, pp. 15–25 (2013)
Metadata
Title
A linear-time algorithm for the orbit problem over cyclic groups
Authors
Anthony W. Lin
Sanming Zhou
Publication date
01-08-2016
Publisher
Springer Berlin Heidelberg
Published in
Acta Informatica / Issue 5/2016
Print ISSN: 0001-5903
Electronic ISSN: 1432-0525
DOI
https://doi.org/10.1007/s00236-015-0251-0

Premium Partner